def definition def or abbrev

`recognizerSetoid`

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

formal statement (Lean)

  39def recognizerSetoid {E : Type*} (r : Recognizer C E) : Setoid C :=

Definition body.

  40  indistinguishableSetoid r
  41
  42/-- The setoid relation unfolds to R(c₁) = R(c₂). -/

From the project-wide theorem graph. These declarations reference this one in their body.

composite_setoid_iff in IndisputableMonolith.RecogGeom.ZornRefinement decl_use
composite_setoid_is_inf in IndisputableMonolith.RecogGeom.ZornRefinement decl_use
composite_setoid_le_left in IndisputableMonolith.RecogGeom.ZornRefinement decl_use
composite_setoid_le_right in IndisputableMonolith.RecogGeom.ZornRefinement decl_use
IsRecognizerInduced in IndisputableMonolith.RecogGeom.ZornRefinement decl_use
maximal_unique_setoid in IndisputableMonolith.RecogGeom.ZornRefinement decl_use
recognizer_meet_semilattice in IndisputableMonolith.RecogGeom.ZornRefinement decl_use
recognizerSetoid_iff in IndisputableMonolith.RecogGeom.ZornRefinement decl_use
zorn_refinement_status in IndisputableMonolith.RecogGeom.ZornRefinement decl_use

Lean names referenced from this declaration's body.

setoid in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
setoid in IndisputableMonolith.Foundation.RationalsFromLogic decl_use
E in IndisputableMonolith.Foundation.SpectralEmergence decl_use
indistinguishableSetoid in IndisputableMonolith.RecogGeom.Indistinguishable decl_use