zorn_le_nonempty — Mathlib

English

If α is nonempty and every chain has an upper bound, there exists a maximal element.

Русский

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

LaTeX

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

Lean4

theorem zorn_le_nonempty [Nonempty α] (h : ∀ c : Set α, IsChain (· ≤ ·) c → c.Nonempty → BddAbove c) :
    ∃ m : α, IsMax m :=
  exists_maximal_of_nonempty_chains_bounded h le_trans

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