choose_lt_descFactorial

Mathlib.Data.Nat.Choose.Bounds

URI: https://scilib.ai/kg/mathlib#Nat.choose_lt_descFactorial

← MathLib Explorer

English

If k ≥ 2 and k ≤ n, then C(n,k) < n.descFactorial k.

Русский

Если k ≥ 2 и k ≤ n, то C(n,k) < n↓k.

LaTeX

$$$$ \binom{n}{k} < \frac{n^{\downarrow k}}{k!} $$$$

Lean4

theorem choose_lt_descFactorial (hk : 2 ≤ k) (hkn : k ≤ n) : n.choose k < n.descFactorial k := by
  rw [choose_eq_descFactorial_div_factorial]; exact Nat.div_lt_self (by simpa) (by simpa)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru