epsilon0_lt_gamma

Mathlib.SetTheory.Ordinal.Veblen

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

← MathLib Explorer

English

ε₀ < Γ_o for all o.

Русский

ε₀ < Γ_o для любого o.

LaTeX

$$$\\varepsilon_0 < Γ_o$$$

Lean4

theorem epsilon0_lt_gamma (o : Ordinal) : ε₀ < Γ_ o :=
  by
  apply lt_of_lt_of_le _ <| (gamma_le_gamma.2 (Ordinal.zero_le _))
  simpa using iterate_veblen_lt_gamma0 2

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

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

Разделы

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

Аффилиация

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