eq_nat_or_omega0_le

Mathlib.SetTheory.Ordinal.Arithmetic

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

← MathLib Explorer

English

For any ordinal o, either o is a natural number or ω ≤ o.

Русский

Для любого ординала o либо o является натуральным, либо ω ≤ o.

LaTeX

$$(∃ n : ℕ, o = n) ∨ ω ≤ o$$

Lean4

theorem eq_nat_or_omega0_le (o : Ordinal) : (∃ n : ℕ, o = n) ∨ ω ≤ o :=
  by
  obtain ho | ho := lt_or_ge o ω
  · exact Or.inl <| lt_omega0.1 ho
  · exact Or.inr ho

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

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

Разделы

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

Аффилиация

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