def definition def or abbrev

`IsRecognizerInduced`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 144def IsRecognizerInduced (s : Setoid C) : Prop :=

proof body

Definition body.

 145  ∃ (E : Type*) (r : Recognizer C E), recognizerSetoid r = s
 146
 147/-- **The Chain Infimum Property**: The intersection (infimum) of a chain of
 148    equivalence relations is an equivalence relation. For setoids, this is
 149    the `sInf` operation in the complete lattice of setoids.
 150
 151    If a family P is closed under chain infima, then for any chain in P,
 152    the infimum is in P. -/

depends on (16)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
Chain in IndisputableMonolith.Chain decl_use
complete in IndisputableMonolith.Complexity.SAT.Backprop decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
E in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
recognizerSetoid in IndisputableMonolith.RecogGeom.ZornRefinement decl_use
Chain in IndisputableMonolith.Recognition decl_use
Chain in IndisputableMonolith.RRF.Core.Recognition decl_use