StrictAntiOn — Mathlib

English

A function f is strictly antitone on s if a < b with a,b ∈ s implies f b < f a.

Русский

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

LaTeX

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

Lean4

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

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