ChainInfClosed

formal source

 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
 175    (fun chain hchain_sub hne_chain hchain_chain => by
 176      obtain ⟨lb, hlb_mem, hlb_bound⟩ := hchain chain.toSet hchain_sub
 177        ⟨hne_chain.some, hne_chain.some.2⟩
 178        (fun a ha b hb hab => hchain_chain ha.2 hb.2 (Subtype.coe_injective.ne hab))
 179      exact ⟨⟨lb, hlb_mem⟩, fun ⟨s, hs⟩ hs_chain => hlb_bound s hs_chain⟩)
 180    hne
 181  exact ⟨m, hmP, fun s hs hle => hm ⟨s, hs⟩ hle⟩
 182
 183/-! ## Section 6: Properties of Maximal Recognizers -/