strictMono — Mathlib

English

If f is a normal ordinal function, then f is strictly increasing: whenever a < b, we have f(a) < f(b).

Русский

Если f — нормальная функция на ординалах, то она строго возрастает: при a < b выполняется f(a) < f(b).

LaTeX

$$$\forall f\,\bigl(\mathrm{IsNormal}(f)\bigr)\;\forall a\,\forall b\; (a < b) \Rightarrow (f(a) < f(b)).$$$

Lean4

theorem strictMono {f} (H : IsNormal f) : StrictMono f :=
  Order.IsNormal.strictMono H

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