English
If a type α is nonempty and every nonempty chain has an upper bound, then there exists a maximal element.
Русский
Если множество α ненулевое и каждая непустая цепь имеет верхнюю грань, то существует максимальный элемент.
LaTeX
$$$$\\forall {\\alpha} [\,\\text{Nonempty } \\alpha\], \\Big(\\forall c, \\IsChain r\\ c \\to c.Nonempty \\to \\exists ub, \\forall a \\in c, r(a,ub)\\Big) \\to \\Big(\\forall {a,b,c}, r(a,b) \\to r(b,c) \\to r(a,c)\\Big) \\to \\exists m, \\forall a, r(m,a) \\to r(a,m).$$$$
Lean4
/-- A variant of Zorn's lemma. If every nonempty chain of a nonempty type has an upper bound, then
there is a maximal element.
-/
theorem exists_maximal_of_nonempty_chains_bounded [Nonempty α]
(h : ∀ c, IsChain r c → c.Nonempty → ∃ ub, ∀ a ∈ c, a ≺ ub) (trans : ∀ {a b c}, a ≺ b → b ≺ c → a ≺ c) :
∃ m, ∀ a, m ≺ a → a ≺ m :=
exists_maximal_of_chains_bounded
(fun c hc =>
(eq_empty_or_nonempty c).elim (fun h => ⟨Classical.arbitrary α, fun x hx => (h ▸ hx : x ∈ (∅ : Set α)).elim⟩)
(h c hc))
trans
