pith. machine review for the scientific record. sign in
theorem proved term proof

recognizerSetoid_iff

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  43theorem recognizerSetoid_iff {E : Type*} (r : Recognizer C E) (c₁ c₂ : C) :
  44    (recognizerSetoid r).Rel c₁ c₂ ↔ r.R c₁ = r.R c₂ :=

proof body

Term-mode proof.

  45  Iff.rfl
  46
  47/-! ## Section 2: Composition Refines Both Components
  48
  49In Mathlib's ordering on `Setoid C`, we have `s ≤ t` iff `∀ a b, s.Rel a b → t.Rel a b`.
  50This means s ≤ t when s is *at least as fine as* t (s-related implies t-related, so
  51t has at least as many related pairs, i.e., t is coarser). The composite recognizer
  52R₁ ⊗ R₂ is finer than both R₁ and R₂, so its setoid is ≤ both component setoids. -/
  53
  54/-- The composite setoid relates c₁, c₂ iff both components do. -/

depends on (12)

Lean names referenced from this declaration's body.