maximal_cells_unsplittable

formal source

 190
 191/-- A maximal recognizer has the property that its resolution cells cannot
 192    be split by any other recognizer in the family. -/
 193theorem maximal_cells_unsplittable {E E' : Type*}
 194    (r : Recognizer C E) (r' : Recognizer C E')
 195    (hmax : IsFinerThan r' r → IsFinerThan r r')
 196    (c₁ c₂ : C) (h : Indistinguishable r c₁ c₂) :
 197    -- If r' is finer than r, then r is also finer than r'
 198    -- meaning r and r' have exactly the same resolution cells
 199    IsFinerThan r' r → Indistinguishable r' c₁ c₂ := by
 200  intro hfiner
 201  exact hfiner c₁ c₂ h
 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. -/