exists_isMax — Mathlib

English

There exists a maximal partial Hahn embedding under Zorn's lemma.

Русский

Существует максимальное частичное Ган-встраивание по лемме Зорна.

LaTeX

$$$\\exists f : Partial seed, IsMax f$$$

Lean4

theorem exists_isMax [IsOrderedAddMonoid R] : ∃ f : Partial seed, IsMax f :=
  by
  apply zorn_le_nonempty
  intro c hc hnonempty
  exact ⟨sSup hnonempty hc.directedOn, mem_upperBounds.mpr fun _ hf ↦ le_sSupFun hc.directedOn hf⟩

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