mono

Mathlib.Order.OrdContinuous

URI: https://scilib.ai/kg/mathlib#RightOrdContinuous.mono

English

If f is RightOrdContinuous, then f is monotone: x ≤ y implies f(x) ≤ f(y).

Русский

Если f — правая непрерывная функция, то она монотонна: x ≤ y ⇒ f(x) ≤ f(y).

LaTeX

$$$ \\forall x,y,\\ x \\le y\\ \\Rightarrow\\ f(x) \\le f(y). $$$

Lean4

theorem mono (hf : RightOrdContinuous f) : Monotone f :=
  hf.orderDual.mono.dual

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

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

Разделы

Аффилиация

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