IsRecognizerInduced

formal source

 141a minimal (finest) element. -/
 142
 143/-- A setoid is *recognizer-induced* if it arises from some recognizer. -/
 144def IsRecognizerInduced (s : Setoid C) : Prop :=
 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. -/
 153def ChainInfClosed (P : Set (Setoid C)) : Prop :=
 154  ∀ (chain : Set (Setoid C)), chain ⊆ P → chain.Nonempty → IsChain (· ≤ ·) chain →
 155    sInf chain ∈ P
 156
 157/-- **Theorem (Zorn for Recognizers)**: Let P be a nonempty family of setoids
 158    on C that is closed under chain infima. Then P contains a minimal element—
 159    a finest recognizer-induced equivalence relation.
 160
 161    Formally: ∃ m ∈ P such that no s ∈ P is strictly finer than m.
 162
 163    This is the dual of Zorn's Lemma (existence of minimal elements):
 164    every chain has a lower bound (the infimum) ⟹ minimal element exists. -/
 165theorem maximal_recognizer_setoid_exists
 166    (P : Set (Setoid C))
 167    (hne : P.Nonempty)
 168    (hchain : ∀ (chain : Set (Setoid C)), chain ⊆ P → chain.Nonempty →
 169      IsChain (· ≤ ·) chain → ∃ lb ∈ P, ∀ s ∈ chain, lb ≤ s) :
 170    ∃ m ∈ P, ∀ s ∈ P, s ≤ m → m ≤ s := by
 171  -- Apply Zorn's Lemma in the ≤ order (where ≤ = "finer")
 172  -- We need: every chain has a lower bound → minimal element exists
 173  -- This is the standard dual Zorn formulation
 174  obtain ⟨m, hmP, hm⟩ := zorn_nonempty_partialOrder₀ P