pow_sub_le_descFactorial — Mathlib

English

For every n and k, (n+1−k)^k ≤ n.descFactorial k.

Русский

Для любых n,k выполняется (n+1−k)^k ≤ n↓k.

LaTeX

$$(n + 1 - k)^{k} \\le n.descFactorial k$$

Lean4

theorem pow_sub_le_descFactorial (n : ℕ) : ∀ k : ℕ, (n + 1 - k) ^ k ≤ n.descFactorial k
  | 0 => by rw [descFactorial_zero, Nat.pow_zero]
  | k + 1 => by
    rw [descFactorial_succ, Nat.pow_succ, succ_sub_succ, Nat.mul_comm]
    apply Nat.mul_le_mul_left
    exact (le_trans (Nat.pow_le_pow_left (Nat.sub_le_sub_right n.le_succ _) k) (pow_sub_le_descFactorial n k))

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