antitone_add_nat_of_succ_le — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem antitone_add_nat_of_succ_le {f : ℕ → α} {k : ℕ} (hf : ∀ n ≥ k, f (n + 1) ≤ f n) :
    Antitone (fun n ↦ f (n + k)) :=
  @monotone_add_nat_of_le_succ αᵒᵈ _ f k hf

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