antitoneOn_nat_Ici_of_succ_le — Mathlib

English

If f: ℕ → α is antitone on the tail from k onward, then AntitoneOn f {x | x ≥ k}.

Русский

Если f: ℕ → α антитонна на хвосте, начиная с k, то AntitoneOn f на {x | x ≥ k}.

LaTeX

$$$\\forall f : \\mathbb{N} \\to α, \\forall k : \\mathbb{N}, (\\forall n, n \\ge k \\Rightarrow f (n + 1) \\le f n) \\Rightarrow \\mathrm{AntitoneOn} f \\{x \\mid k \\le x\\}$$$

Lean4

theorem antitoneOn_nat_Ici_of_succ_le {f : ℕ → α} {k : ℕ} (hf : ∀ n ≥ k, f (n + 1) ≤ f n) : AntitoneOn f {x | k ≤ x} :=
  @monotoneOn_nat_Ici_of_le_succ αᵒᵈ _ f k hf

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