English
If S is a set of subsets and a certain chain condition holds, then for any x in S there exists m containing x with m minimal among S.
Русский
Если S — набор подмножеств и выполняется цепное условие, то для любого x ∈ S существует m, содержащий x, минимальный по включению в S.
LaTeX
$$$$\forall {\alpha} (S:\Set(\Set\alpha)), (H : \forall c \subseteq S, IsChain (\\subseteq) c \\to c.Nonempty \\to \exists ub \in S, \forall s \in c, s \\subseteq ub) \\to \forall x \in S, \exists m \ni x, \text{Minimal}(\\in S) m.$$$$
Lean4
theorem zorn_subset_nonempty (S : Set (Set α)) (H : ∀ c ⊆ S, IsChain (· ⊆ ·) c → c.Nonempty → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub)
(x) (hx : x ∈ S) : ∃ m, x ⊆ m ∧ Maximal (· ∈ S) m :=
zorn_le_nonempty₀ _ (fun _ cS hc y yc => H _ cS hc ⟨y, yc⟩) _ hx
