right_le_veblenWith — Mathlib

English

Let f be a normal function on ordinals. For every o and a, one has a ≤ veblenWith(f, o, a).

Русский

Пусть f — нормальная функция на ординалах. Для любых o и a выполняется a ≤ veblenWith(f, o, a).

LaTeX

$$$\forall f:\,\operatorname{Ordinal} \to \operatorname{Ordinal},\ \operatorname{IsNormal}(f)\ \Rightarrow\ \forall o,a\in \operatorname{Ordinal},\ a \le \operatorname{veblenWith}(f,o,a)$$$

Lean4

theorem right_le_veblenWith (o a : Ordinal) : a ≤ veblenWith f o a :=
  (veblenWith_right_strictMono hf o).le_apply

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