isNormal_veblen

Mathlib.SetTheory.Ordinal.Veblen

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

English

For any ordinal o, IsNormal(veblen o).

Русский

Для любого ординала o верно IsNormal(veblen(o)).

LaTeX

$$$\forall o:\operatorname{Ordinal},\ \operatorname{IsNormal}(\operatorname{veblen}(o))$$$

Lean4

theorem isNormal_veblen (o : Ordinal) : IsNormal (veblen o) :=
  (isNormal_opow one_lt_omega0).veblenWith o

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

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

Разделы

Аффилиация

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