monotone_add_nat_of_le_succ — Mathlib

English

If hf: ∀ n ≥ k, f(n) ≤ f(n+1) for some k, then the shifted function n ↦ f(n+k) is monotone.

Русский

Если hf: ∀ n ≥ k, f(n) ≤ f(n+1), тогда отображение n ↦ f(n+k) монотонно.

LaTeX

$$$\\forall {f : \\mathbb{N} \\to \\alpha} {k : \\mathbb{N}}, (\\forall n \\ge k, f n \\le f (n + 1)) \\Rightarrow \\forall m n : \\mathbb{N}, m \\le n \\Rightarrow f (m + k) \\le f (n + k)$$$

Lean4

theorem monotone_add_nat_of_le_succ {f : ℕ → α} {k : ℕ} (hf : ∀ n ≥ k, f n ≤ f (n + 1)) :
    Monotone (fun n ↦ f (n + k)) := fun _ _ hle ↦
  Nat.rel_of_forall_rel_succ_of_le_of_le (· ≤ ·) hf (Nat.le_add_left k _)
    (Nat.add_le_add_iff_right.mpr hle)
      -- TODO replace `{ x | k ≤ x }` with `Set.Ici k`

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