factorial_mul_pow_sub_le_factorial

English

If n ≤ m, then n! · n^(m−n) ≤ m!, i.e., factorial dominates the growth of powers.

Русский

Если n ≤ m, то n! · n^(m−n) ≤ m!, то есть факториал растет быстрее степеней.

LaTeX

$$$n \le m \Rightarrow n! \cdot n^{(m-n)} \le m!$$$

Lean4

theorem factorial_mul_pow_sub_le_factorial {n m : ℕ} (hnm : n ≤ m) : n ! * n ^ (m - n) ≤ m ! := by
  calc
    _ ≤ n ! * (n + 1) ^ (m - n) := Nat.mul_le_mul_left _ (Nat.pow_le_pow_left n.le_succ _)
    _ ≤ _ := by simpa [hnm] using @Nat.factorial_mul_pow_le_factorial n (m - n)

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