zorn_le_nonempty_Ici₀ — Mathlib

English

Let a be an element and suppose that every chain in Ici a has an upper bound; then there exists a maximal element above a.

Русский

Пусть имеется элемент a; если каждую цепь внутри Ici a можно ограничить сверху, то существует максимальный элемент выше a.

LaTeX

$$$$\forall {\alpha} [\text{Preorder } \alpha] (a:\alpha) (ih : \forall c \subseteq Ici a, IsChain (\\le) c \to \forall y \in c, \exists ub, \forall z \in c, z \le ub) (x:\alpha) (hax : a \le x) : \exists m, x \le m \land IsMax m.$$$$

Lean4

theorem zorn_le_nonempty_Ici₀ (a : α) (ih : ∀ c ⊆ Ici a, IsChain (· ≤ ·) c → ∀ y ∈ c, ∃ ub, ∀ z ∈ c, z ≤ ub) (x : α)
    (hax : a ≤ x) : ∃ m, x ≤ m ∧ IsMax m :=
  by
  let ⟨m, hxm, ham, hm⟩ := zorn_le_nonempty₀ (Ici a) (fun c hca hc y hy ↦ ?_) x hax
  · exact ⟨m, hxm, fun z hmz => hm (ham.trans hmz) hmz⟩
  · have ⟨ub, hub⟩ := ih c hca hc y hy
    exact ⟨ub, (hca hy).trans (hub y hy), hub⟩

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