choose_le_pow_div — Mathlib

English

For all n,k, in any semifield α, (n choose k) ≤ (n^k)/k! after casting to α.

Русский

Для любых n,k в полях α, после приведения к α имеет место неравенство: C(n,k) ≤ n^k / k!.

LaTeX

$$$$ (n\choose k) \le (n^k) / k! $$$$

Lean4

theorem choose_le_pow_div (r n : ℕ) : (n.choose r : α) ≤ (n ^ r : α) / r ! :=
  by
  rw [le_div_iff₀']
  · norm_cast
    rw [← Nat.descFactorial_eq_factorial_mul_choose]
    exact n.descFactorial_le_pow r
  exact mod_cast r.factorial_pos

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