right_le_veblen

Mathlib.SetTheory.Ordinal.Veblen

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

English

For all o and a, a ≤ veblen(o,a).

Русский

Для каждого o и a верно a ≤ veblen(o,a).

LaTeX

$$$$a \\le \\operatorname{veblen}(o,a).$$$$

Lean4

theorem right_le_veblen (o a : Ordinal) : a ≤ veblen o a :=
  right_le_veblenWith (isNormal_opow one_lt_omega0) o a

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

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

Разделы

Аффилиация

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