omega0_lt_epsilon

Mathlib.SetTheory.Ordinal.Veblen

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

← MathLib Explorer

English

For every ordinal o, the omega number ω is strictly below the epsilon number ε_o.

Русский

Для любого ординала o верно, что ω < ε_o.

LaTeX

$$$\\omega < \\varepsilon_o$$$

Lean4

theorem omega0_lt_epsilon (o : Ordinal) : ω < ε_ o :=
  by
  apply lt_of_lt_of_le _ <| (veblen_right_strictMono _).monotone (Ordinal.zero_le o)
  simpa using iterate_omega0_opow_lt_epsilon0 2

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

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

Разделы

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

Аффилиация

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