factorial_mul_pow_le_factorial — Mathlib

English

For all m,n ∈ ℕ, m! · (m+1)^n ≤ (m+n)!.

Русский

Для любых m,n ∈ ℕ: m! · (m+1)^n ≤ (m+n)!.

LaTeX

$$$\forall {m,n:\mathbb{N}}, m! \cdot (m+1)^n \le (m+n)!$$$

Lean4

theorem factorial_mul_pow_le_factorial : ∀ {m n : ℕ}, m ! * (m + 1) ^ n ≤ (m + n)!
  | m, 0 => by simp
  | m, n + 1 => by
    rw [← Nat.add_assoc, factorial_succ, Nat.mul_comm (_ + 1), Nat.pow_succ, ← Nat.mul_assoc]
    exact Nat.mul_le_mul factorial_mul_pow_le_factorial (succ_le_succ (le_add_right _ _))

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