StrictMono

Mathlib.Order.Monotone.Defs

URI: https://scilib.ai/kg/mathlib#StrictMono

English

A function f is strictly monotone if a < b implies f a < f b.

Русский

Функция f строго монотонна, если a < b тогда f(a) < f(b).

LaTeX

$$$\\mathrm{StrictMono}(f)\\;:=\\forall a b,\\ a < b \\Rightarrow f(a) < f(b).$$$

Lean4

/-- A function `f` is strictly monotone if `a < b` implies `f a < f b`. -/
def StrictMono (f : α → β) : Prop :=
  ∀ ⦃a b⦄, a < b → f a < f b

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

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

Разделы

Аффилиация

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