strictAnti_nat_of_succ_lt — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem strictAnti_nat_of_succ_lt {f : ℕ → α} (hf : ∀ n, f (n + 1) < f n) : StrictAnti f :=
  @strictMono_nat_of_lt_succ αᵒᵈ _ f hf

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