AntitoneOn — Mathlib

English

A function f is antitone on s if a ≤ b for a,b ∈ s implies f b ≤ f a.

Русский

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

LaTeX

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

Lean4

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

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