natCast_add_omega0

Mathlib.SetTheory.Ordinal.Arithmetic

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

← MathLib Explorer

English

For any natural n, n + ω = ω.

Русский

Для любого натурального n, n + ω = ω.

LaTeX

$$$n + \omega = \omega$$$

Lean4

theorem natCast_add_omega0 (n : ℕ) : n + ω = ω :=
  by
  refine le_antisymm (le_of_forall_lt fun a ha ↦ ?_) (le_add_left _ _)
  obtain ⟨b, hb', hb⟩ := (lt_add_iff omega0_ne_zero).1 ha
  obtain ⟨m, rfl⟩ := lt_omega0.1 hb'
  apply hb.trans_lt
  exact_mod_cast nat_lt_omega0 (n + m)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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