English
If every chain in a poset has an upper bound, then there exists a maximal element.
Русский
Если у частичного порядка каждый цепной набор имеет верхнюю грань, тогда существует максимальный элемент.
LaTeX
$$$$\forall \alpha\, [r:\alpha \to \alpha \to \mathrm{Prop}],\; \Big(\forall c, \IsChain r\ c \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
/-- **Zorn's lemma**
If every chain has an upper bound, then there exists a maximal element. -/
theorem exists_maximal_of_chains_bounded (h : ∀ c, IsChain r c → ∃ ub, ∀ a ∈ c, a ≺ ub)
(trans : ∀ {a b c}, a ≺ b → b ≺ c → a ≺ c) : ∃ m, ∀ a, m ≺ a → a ≺ m :=
have : ∃ ub, ∀ a ∈ maxChain r, a ≺ ub := h _ <| maxChain_spec.left
let ⟨ub, (hub : ∀ a ∈ maxChain r, a ≺ ub)⟩ := this
⟨ub, fun a ha =>
have : IsChain r (insert a <| maxChain r) := maxChain_spec.1.insert fun b hb _ => Or.inr <| trans (hub b hb) ha
hub a <| by
rw [maxChain_spec.right this (subset_insert _ _)]
exact mem_insert _ _⟩
