add_le_nat — Mathlib

English

For a strictly increasing function f: ℕ → ℕ and natural numbers m,n, one has m + f(n) ≤ f(m + n).

Русский

Для строго возрастающей функции f: ℕ → ℕ и натуральных чисел m,n выполняется m + f(n) ≤ f(m + n).

LaTeX

$$$\\forall (f : \\mathbb{N} \\to \\mathbb{N}) (m n : \\mathbb{N}),\\; StrictMono f \\to m + f(n) \\le f(m + n)$$$

Lean4

theorem add_le_nat {f : ℕ → ℕ} (hf : StrictMono f) (m n : ℕ) : m + f n ≤ f (m + n) :=
  by
  rw [Nat.add_comm m, Nat.add_comm m]
  induction m with
  | zero => rw [Nat.add_zero, Nat.add_zero]
  | succ m ih =>
    rw [← Nat.add_assoc, ← Nat.add_assoc, Nat.succ_le]
    exact ih.trans_lt (hf (n + m).lt_succ_self)

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