veblen_right_strictMono

Mathlib.SetTheory.Ordinal.Veblen

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

English

For every ordinal o, the function x ↦ veblen(o, x) is strictly increasing in x.

Русский

Для каждого ординала o функция x ↦ veblen(o, x) строго возрастает по x.

LaTeX

$$$$\\forall x,y\\, (x

Lean4

theorem veblen_right_strictMono (o : Ordinal) : StrictMono (veblen o) :=
  veblenWith_right_strictMono (isNormal_opow one_lt_omega0) o

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

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

Разделы

Аффилиация

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