English
If α is a preorder and S is a subset of α such that every c ⊆ S which is a chain has an upper bound in S, then there exists m ∈ α maximal with respect to membership in S.
Русский
Если есть подмножество S из α такое, что каждая цепь внутри S имеет верхнюю грань в S, то существует m, максимальный по включению в S.
LaTeX
$$$$\forall {\alpha} [\text{Preorder } \alpha], (S:\text{Set }(\text{Set }\alpha)) \to \Big(\forall c \subseteq S, IsChain (\\subseteq) c \\to \exists ub \in S, \forall s \in c, s \subseteq ub\Big) \\to \exists m, \Maximal (\\in S) m.$$$$
Lean4
theorem zorn_le_nonempty₀ (s : Set α) (ih : ∀ c ⊆ s, IsChain (· ≤ ·) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub) (x : α)
(hxs : x ∈ s) : ∃ m, x ≤ m ∧ Maximal (· ∈ s) m :=
by
have H := zorn_le₀ ({y ∈ s | x ≤ y}) fun c hcs hc => ?_
· rcases H with ⟨m, ⟨hms, hxm⟩, hm⟩
exact ⟨m, hxm, hms, fun z hzs hmz => @hm _ ⟨hzs, hxm.trans hmz⟩ hmz⟩
· rcases c.eq_empty_or_nonempty with (rfl | ⟨y, hy⟩)
· exact ⟨x, ⟨hxs, le_rfl⟩, fun z => False.elim⟩
· rcases ih c (fun z hz => (hcs hz).1) hc y hy with ⟨z, hzs, hz⟩
exact ⟨z, ⟨hzs, (hcs hy).2.trans <| hz _ hy⟩, hz⟩
