veblen_lt_veblen_iff_right

Mathlib.SetTheory.Ordinal.Veblen

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

English

For all o, a, b, the inequality veblen(o, a) < veblen(o, b) is equivalent to a < b.

Русский

Для всех o, a, b неравенство veblen(o, a) < veblen(o, b) эквивалентно a < b.

LaTeX

$$$$\\operatorname{veblen}(o,a) < \\operatorname{veblen}(o,b) \\iff a < b.$$$$

Lean4

@[simp]
theorem veblen_lt_veblen_iff_right : veblen o a < veblen o b ↔ a < b :=
  veblenWith_lt_veblenWith_iff_right (isNormal_opow one_lt_omega0)

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

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

Разделы

Аффилиация

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