monotone

Mathlib.SetTheory.Ordinal.Arithmetic

URI: https://scilib.ai/kg/mathlib#Ordinal.IsNormal.monotone

English

If f is a normal ordinal function, then f is monotone: a ≤ b implies f(a) ≤ f(b).

Русский

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

LaTeX

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

Lean4

theorem monotone {f} (H : IsNormal f) : Monotone f :=
  H.strictMono.monotone

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

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

Разделы

Аффилиация

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