invVeblen₂_epsilon

Mathlib.SetTheory.Ordinal.Veblen

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

English

If o < ε_o then invVeblen₂(ε_o) = o.

Русский

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

LaTeX

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

Lean4

theorem invVeblen₂_epsilon (h : o < ε_ o) : invVeblen₂ (ε_ o) = o :=
  invVeblen₂_veblen one_ne_zero h

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

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

Разделы

Аффилиация

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