veblenWith_right_strictMono — Mathlib

English

The map a ↦ veblenWith f o is a strictly increasing function in a, for any fixed o with IsNormal f.

Русский

Функция a ↦ veblenWith f o строго возрастает по a при любом фиксированном o, для которого f нормальна.

LaTeX

$$theorem veblenWith_right_strictMono (o : Ordinal) : StrictMono (veblenWith f o)$$

Lean4

theorem veblenWith_right_strictMono (o : Ordinal) : StrictMono (veblenWith f o) :=
  (hf.veblenWith o).strictMono

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