not_bddAbove_isInitial — Mathlib

English

The set of initial ordinals is not bounded above; there is no finite upper bound for initial ordinals.

Русский

Множество начальных ординалов не имеет верхней границы; не существует конечной верхней границы для начальных ординалов.

LaTeX

$$$\neg\mathrm{BddAbove}\{x \mid \mathrm{IsInitial}(x)\}$$$

Lean4

theorem not_bddAbove_isInitial : ¬BddAbove {x | IsInitial x} :=
  by
  rintro ⟨a, ha⟩
  have := ha (isInitial_ord (succ a.card))
  rw [ord_le] at this
  exact (lt_succ _).not_ge this

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