natCast_lt_epsilon

Mathlib.SetTheory.Ordinal.Veblen

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

English

For every natural number n and ordinal o, the natural number n is less than ε_o.

Русский

Для любых n ∈ ℕ и o ∈ Ordinal выполняется n < ε_o.

LaTeX

$$$n < \\varepsilon_o$$$

Lean4

theorem natCast_lt_epsilon (n : ℕ) (o : Ordinal) : n < ε_ o :=
  (nat_lt_omega0 n).trans <| omega0_lt_epsilon o

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

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

Разделы

Аффилиация

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