veblen_left_monotone

Mathlib.SetTheory.Ordinal.Veblen

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

English

For fixed o, the map x ↦ veblen(x,o) is monotone in x.

Русский

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

LaTeX

$$$$\\forall x,y\\ (x \\le y \\Rightarrow \\operatorname{veblen}(x,o) \\le \\operatorname{veblen}(y,o)).$$$$

Lean4

theorem veblen_left_monotone (o : Ordinal) : Monotone (veblen · o) :=
  veblenWith_left_monotone (isNormal_opow one_lt_omega0) o

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

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

Разделы

Аффилиация

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