MonotoneOn — Mathlib

English

A function f is monotone on a set s if for all a,b ∈ s with a ≤ b we have f a ≤ f b.

Русский

Функция f монотонна на множестве s, если для любых a,b ∈ s с a ≤ b выполняется f(a) ≤ f(b).

LaTeX

$$$\\mathrm{MonotoneOn}(f,s)\\;:=\\forall a\\in s\\,\\forall b\\in s,\\ a \\le b \\Rightarrow f(a) \\le f(b).$$$

Lean4

/-- A function `f` is monotone on `s` if, for all `a, b ∈ s`, `a ≤ b` implies `f a ≤ f b`. -/
def MonotoneOn (f : α → β) (s : Set α) : Prop :=
  ∀ ⦃a⦄ (_ : a ∈ s) ⦃b⦄ (_ : b ∈ s), a ≤ b → f a ≤ f b

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