invVeblen₁_epsilon

Mathlib.SetTheory.Ordinal.Veblen

URI: https://scilib.ai/kg/mathlib#Ordinal.invVeblen₁_epsilon

English

If o < ε_o, then invVeblen₁(ε_o) = 1.

Русский

Если o < ε_o, то invVeblen₁(ε_o) = 1.

LaTeX

$$$o < \\varepsilon_o \\implies \\operatorname{invVeblen}_1(\\varepsilon_o) = 1$$$

Lean4

theorem invVeblen₁_epsilon (h : o < ε_ o) : invVeblen₁ (ε_ o) = 1 :=
  invVeblen₁_veblen h

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

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

Разделы

Аффилиация

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