antitone_int_of_succ_le — Mathlib

English

If f: ℤ → α satisfies f(n+1) ≤ f(n) for all n, then f is antitone on ℤ.

Русский

Если f: ℤ → α удовлетворяет f(n+1) ≤ f(n) для всех n, тогда f антитонна на ℤ.

LaTeX

$$$\\forall f : \\mathbb{Z} \\to α, (\\forall n : \\mathbb{Z}, f (n + 1) \\le f n) \\Rightarrow \\mathrm{Antitone} f$$$

Lean4

theorem antitone_int_of_succ_le {f : ℤ → α} (hf : ∀ n, f (n + 1) ≤ f n) : Antitone f :=
  Int.rel_of_forall_rel_succ_of_le (· ≥ ·) hf

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