pow_le_choose — Mathlib

English

For natural numbers r,n, the inequality ((n+1−r)^r)/(r!) ≤ C(n,r) holds in any ordered semifield.

Русский

Для натуральных чисел r,n выполняется неравенство \\frac{(n+1−r)^r}{r!} ≤ \\binom{n}{r}.

LaTeX

$$$$ \\frac{(n+1 - r)^{\,r}}{r!} \\le \\binom{n}{r} $$$$

Lean4

theorem pow_le_choose (r n : ℕ) : ((n + 1 - r : ℕ) ^ r : α) / r ! ≤ n.choose r :=
  by
  rw [div_le_iff₀']
  · norm_cast
    rw [← Nat.descFactorial_eq_factorial_mul_choose]
    exact n.pow_sub_le_descFactorial r
  exact mod_cast r.factorial_pos

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