maximal_unique_setoid

formal source

 202
 203/-- If a maximal recognizer exists and another recognizer refines it,
 204    they induce the same equivalence relation. -/
 205theorem maximal_unique_setoid {E₁ E₂ : Type*}
 206    (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂)
 207    (hfiner : IsFinerThan r₂ r₁)
 208    (hmax : IsFinerThan r₂ r₁ → IsFinerThan r₁ r₂) :
 209    recognizerSetoid r₁ = recognizerSetoid r₂ := by
 210  ext c₁ c₂
 211  exact ⟨fun h => hfiner c₁ c₂ h, fun h => hmax hfiner c₁ c₂ h⟩
 212
 213/-! ## Section 7: Connection to the Complete Lattice
 214
 215The setoids on C form a complete lattice in Mathlib. The recognizer-induced
 216setoids form a sub-meet-semilattice (closed under finite meets via ⊗).
 217The Zorn result above shows that with the chain-infimum closure property,
 218this sublattice has a bottom element (finest recognizer). -/
 219
 220/-- Composition provides the meet (infimum) operation for recognizer setoids.
 221    Together with the Zorn result, this establishes that a chain-closed
 222    family of recognizer setoids forms a complete meet-semilattice with
 223    a minimum element. -/
 224theorem recognizer_meet_semilattice {E₁ E₂ : Type*}
 225    (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) :
 226    recognizerSetoid (r₁ ⊗ r₂) = sInf {recognizerSetoid r₁, recognizerSetoid r₂} := by
 227  ext c₁ c₂
 228  simp only [Setoid.sInf, Set.mem_setOf_eq]
 229  constructor
 230  · intro h s hs
 231    simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at hs
 232    cases hs with
 233    | inl h₁ => rw [← h₁]; exact (composite_setoid_le_left r₁ r₂) h
 234    | inr h₂ => rw [← h₂]; exact (composite_setoid_le_right r₁ r₂) h
 235  · intro h