left_le_veblen

Mathlib.SetTheory.Ordinal.Veblen

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

English

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

Русский

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

LaTeX

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

Lean4

theorem left_le_veblen (o a : Ordinal) : o ≤ veblen o a :=
  left_le_veblenWith (isNormal_opow one_lt_omega0) (by simp) o a

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

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

Разделы

Аффилиация

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