gamma0_eq_nfp

Mathlib.SetTheory.Ordinal.Veblen

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

English

Γ₀ equals the fixed point of the function a ↦ veblen(a, 0).

Русский

Γ₀ равно фиксированной точке функции a ↦ veblen(a, 0).

LaTeX

$$$Γ_0 = \operatorname{nfp}(\lambda x. \\veblen(x,0)) (0)$$$

Lean4

theorem gamma0_eq_nfp : Γ₀ = nfp (veblen · 0) 0 :=
  deriv_zero_right _

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

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

Разделы

Аффилиация

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