StrictMonoOn — Mathlib

English

A function f is strictly monotone on s if a,b ∈ s and a < b imply f a < f b.

Русский

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

LaTeX

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

Lean4

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

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