descFactorial_le_pow — Mathlib

English

For n with k+2 ≤ n, (n−(k+1))^{k+2} < n.descFactorial(k+2).

Русский

Для n с k+2 ≤ n имеем (n−(k+1))^{k+2} < n↓(k+2).

LaTeX

$$(n - (k + 1))^{(k + 2)} < n.descFactorial (k + 2)$$

Lean4

theorem descFactorial_le_pow (n : ℕ) : ∀ k : ℕ, n.descFactorial k ≤ n ^ k
  | 0 => by rw [descFactorial_zero, Nat.pow_zero]
  | k + 1 => by
    rw [descFactorial_succ, Nat.pow_succ, Nat.mul_comm _ n]
    exact Nat.mul_le_mul (Nat.sub_le _ _) (descFactorial_le_pow _ k)

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