epsilon0_le_of_omega0_opow_le

Mathlib.SetTheory.Ordinal.Veblen

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

← MathLib Explorer

English

ε₀ equals the nfp of the map a ↦ ω^a at 0.

Русский

ε₀ равно nfp отображения a ↦ ω^a в 0.

LaTeX

$$$\varepsilon_0 = nfp(\lambda a. ω^a) 0$$$

Lean4

theorem epsilon0_le_of_omega0_opow_le (h : ω ^ o ≤ o) : ε₀ ≤ o :=
  by
  rw [epsilon0_eq_nfp]
  exact nfp_le_fp (fun _ _ ↦ (opow_le_opow_iff_right one_lt_omega0).2) (Ordinal.zero_le o) h

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

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

Разделы

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

Аффилиация

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