zorn_le — Mathlib

English

Let α be a type with a preorder. If every chain c ⊆ α has an upper bound, there exists a maximal element m in α.

Русский

Пусть α — множество с частичным порядком. Если каждая цепь c ⊆ α имеет верхнюю границу, существует максимальный элемент m в α.

LaTeX

$$$$\forall {\alpha} [\text{Preorder } \alpha], \Big(\forall c:\, \text{Set }\alpha, \IsChain (≤) c \to BddAbove c\Big) \to \exists m:\alpha, \IsMax m.$$$$

Lean4

theorem zorn_le (h : ∀ c : Set α, IsChain (· ≤ ·) c → BddAbove c) : ∃ m : α, IsMax m :=
  exists_maximal_of_chains_bounded h le_trans

Похожие утверждения