English
If S is a family of sets and H holds for chains, then for any x ∈ S there exists m such that m ⊆ x and m is Minimal in S.
Русский
Если S — семейство множеств и выполняется условие H для цепей, тогда для любого x ∈ S существует m, удовлетворяющее m ⊆ x и минимальный в S.
LaTeX
$$$$\forall {\alpha} (S:\Set(\Set\alpha)), (H : \forall c ⊆ S, IsChain (\\subseteq) c \\to c.Nonempty \\to \exists ub \\in S, \forall s \\in c, ub \\subseteq s) \\to \forall x \\in S, \\exists m, m \\subseteq x \\land \ Minimal (\\in S) m.$$$$
Lean4
theorem zorn_superset_nonempty (S : Set (Set α))
(H : ∀ c ⊆ S, IsChain (· ⊆ ·) c → c.Nonempty → ∃ lb ∈ S, ∀ s ∈ c, lb ⊆ s) (x) (hx : x ∈ S) :
∃ m, m ⊆ x ∧ Minimal (· ∈ S) m :=
@zorn_le_nonempty₀ (Set α)ᵒᵈ _ S (fun _ cS hc y yc => H _ cS hc.symm ⟨y, yc⟩) _ hx
