ascFactorial_le_pow_add — Mathlib

English

For all n ∈ ℕ and k ≥ 2, (n+1)^k < (n+1)^{\overline{k}}.

Русский

Для всех n ∈ ℕ и k ≥ 2 верно: (n+1)^k < (n+1)^{\overline{k}}.

LaTeX

$$$$\forall n \in \mathbb{N}, \forall k \in \mathbb{N}, k \ge 2 \Rightarrow (n+1)^k < (n+1)^{\overline{k}}$$$$

Lean4

theorem ascFactorial_le_pow_add (n : ℕ) : ∀ k : ℕ, (n + 1).ascFactorial k ≤ (n + k) ^ k
  | 0 => by rw [ascFactorial_zero, Nat.pow_zero]
  | k + 1 => by
    rw [ascFactorial_succ, Nat.pow_succ, Nat.mul_comm, ← Nat.add_assoc, Nat.add_right_comm n 1 k]
    exact Nat.mul_le_mul_right _ (Nat.le_trans (ascFactorial_le_pow_add _ k) (Nat.pow_le_pow_left (le_succ _) _))

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