iSup_natCast

Mathlib.SetTheory.Ordinal.Family

URI: https://scilib.ai/kg/mathlib#Ordinal.iSup_natCast

English

The supremum of the natural-number embedded ordinals equals ω.

Русский

Наивысшая верхняя граница, полученная из чисел, равна ω.

LaTeX

$$$\\operatorname{iSup} (\\operatorname{Nat.cast}) = \\omega$$$

Lean4

@[simp]
theorem iSup_natCast : iSup Nat.cast = ω :=
  (Ordinal.iSup_le fun n => (nat_lt_omega0 n).le).antisymm <| omega0_le.2 <| Ordinal.le_iSup _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru