veblen_succ

Mathlib.SetTheory.Ordinal.Veblen

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

English

For every ordinal o, the Veblen function at the successor satisfies veBlèn(succ o) = deriv(veblen o).

Русский

Для любого ординала o верно: Veblen(succ(o)) = deriv(Veblen(o)).

LaTeX

$$$$\\operatorname{veblen}(\\operatorname{succ} o) = \\operatorname{deriv}(\\operatorname{veblen}(o)).$$$$

Lean4

theorem veblen_succ (o : Ordinal) : veblen (succ o) = deriv (veblen o) :=
  veblenWith_succ (isNormal_opow one_lt_omega0) o

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

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

Разделы

Аффилиация

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