veblen_eq_of_lt_invVeblen₁

Mathlib.SetTheory.Ordinal.Veblen

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

English

If o is less than invVeblen1(x), then veblen(o,x) = x.

Русский

Если o меньше invVeblen1(x), тогда veblen(o,x) = x.

LaTeX

$$$$o < \\operatorname{invVeblen}_1(x) \\Rightarrow \\operatorname{veblen}(o,x) = x.$$$$

Lean4

theorem veblen_eq_of_lt_invVeblen₁ (h : o < invVeblen₁ x) : veblen o x = x := by simpa using notMem_of_lt_csInf' h

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

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

Разделы

Аффилиация

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