iSup_add_nat

Mathlib.SetTheory.Ordinal.Family

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

English

For any ordinal o, the supremum over natural numbers of o + n equals o + ω.

Русский

Для произвольного ординала o супремум по n∈ℕ от o+n равен o+ω.

LaTeX

$$$\\forall o\\; (\\sup_{n\\in\\mathbb{N}} (o+n)) = o+\\omega$$$

Lean4

@[simp]
theorem iSup_add_nat (o : Ordinal) : ⨆ n : ℕ, o + n = o + ω :=
  (isNormal_add_right o).apply_omega0

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

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

Разделы

Аффилиация

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