English
If every chain is bounded above, then there exists a maximal element m with respect to the given preorder.
Русский
Если каждая цепь ограничена сверху относительно заданного предorder, существует максимальный элемент m относительно данного порядка.
LaTeX
$$$$\forall {\alpha} [\text{Preorder } \alpha], \Big(\forall c:\, \text{Set }\alpha, \IsChain (\\le) c \to\ BddAbove c\Big) \to \exists m:\alpha, \IsMax m.$$$$
Lean4
theorem zorn_le₀ (s : Set α) (ih : ∀ c ⊆ s, IsChain (· ≤ ·) c → ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub) : ∃ m, Maximal (· ∈ s) m :=
let ⟨⟨m, hms⟩, h⟩ :=
@zorn_le s _ fun c hc =>
let ⟨ub, hubs, hub⟩ :=
ih (Subtype.val '' c) (fun _ ⟨⟨_, hx⟩, _, h⟩ => h ▸ hx)
(by
rintro _ ⟨p, hpc, rfl⟩ _ ⟨q, hqc, rfl⟩ hpq
exact hc hpc hqc fun t => hpq (Subtype.ext_iff.1 t))
⟨⟨ub, hubs⟩, fun ⟨_, _⟩ hc => hub _ ⟨_, hc, rfl⟩⟩
⟨m, hms, fun z hzs hmz => @h ⟨z, hzs⟩ hmz⟩
