Monotone

Mathlib.Order.Monotone.Defs

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

English

A function f is monotone if a ≤ b implies f a ≤ f b.

Русский

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

LaTeX

$$$\\mathrm{Monotone}(f)\\;\\text{defined as }\\forall a b,\\ a ≤ b \\Rightarrow f a ≤ f b.$$$

Lean4

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

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

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

Разделы

Аффилиация

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