veblen_gamma_zero

Mathlib.SetTheory.Ordinal.Veblen

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

English

veblen(Γ_o, 0) = Γ_o.

Русский

veblen(Γ_o, 0) = Γ_o.

LaTeX

$$$\\veblen(\\Gamma_o, 0) = \\Gamma_o$$$

Lean4

@[simp]
theorem veblen_gamma_zero (o : Ordinal) : veblen (Γ_ o) 0 = Γ_ o :=
  isNormal_veblen_zero.deriv_fp o

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

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

Разделы

Аффилиация

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