monotoneOn_nat_Ici_of_le_succ — Mathlib

English

If f: ℕ → α is nondecreasing on the tail {x | x ≥ k}, then f is monotone on that tail.

Русский

Если f: ℕ → α неубывающая на хвосте {x | x ≥ k}, то она монотонна на этом хвосте.

LaTeX

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

Lean4

theorem monotoneOn_nat_Ici_of_le_succ {f : ℕ → α} {k : ℕ} (hf : ∀ n ≥ k, f n ≤ f (n + 1)) : MonotoneOn f {x | k ≤ x} :=
  fun _ hab _ _ hle ↦ Nat.rel_of_forall_rel_succ_of_le_of_le (· ≤ ·) hf hab hle

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