pow_succ_le_ascFactorial — Mathlib

English

For all n,k ∈ ℕ, n^k ≤ n^{\overline{k}}.

Русский

Для всех n,k ∈ ℕ верно: n^k ≤ n^{\overline{k}}.

LaTeX

$$$$\forall n,k \in \mathbb{N},\ n^{k} \le n^{\overline{k}}$$$$

Lean4

theorem pow_succ_le_ascFactorial (n : ℕ) : ∀ k : ℕ, n ^ k ≤ n.ascFactorial k
  | 0 => by rw [ascFactorial_zero, Nat.pow_zero]
  | k + 1 => by
    rw [Nat.pow_succ, Nat.mul_comm, ascFactorial_succ, ← succ_ascFactorial]
    exact
      Nat.mul_le_mul (Nat.le_refl n)
        (Nat.le_trans (Nat.pow_le_pow_left (le_succ n) k) (pow_succ_le_ascFactorial n.succ k))

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