gamma_succ_eq_nfp

Mathlib.SetTheory.Ordinal.Veblen

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

English

Γ_(succ o) equals the fixed point of the same function evaluated at succ(Γ_o).

Русский

Γ_(succ o) равно фиксированной точке той же функции в точке succ(Γ_o).

LaTeX

$$$Γ_{(succ o)} = \operatorname{nfp}(\lambda x. \\veblen(x,0)) (succ(Γ_o))$$$

Lean4

theorem gamma_succ_eq_nfp (o : Ordinal) : Γ_ (succ o) = nfp (veblen · 0) (succ (Γ_ o)) :=
  deriv_succ _ _

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

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

Разделы

Аффилиация

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