choose_le_two_pow

Mathlib.Data.Nat.Choose.Bounds

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

← MathLib Explorer

English

For all n,k, C(n,k) ≤ 2^n.

Русский

Для любых n,k: C(n,k) ≤ 2^n.

LaTeX

$$$$ \\binom{n}{k} \\le 2^{n} $$$$

Lean4

theorem choose_le_two_pow (n k : ℕ) : n.choose k ≤ 2 ^ n :=
  by
  obtain (rfl | hk) := eq_zero_or_pos k
  · simp [Nat.one_le_two_pow]
  · obtain (rfl | hn) := eq_zero_or_pos n
    · have : choose 0 k = 0 := by convert Nat.choose_zero_succ (k - 1); omega
      simp [this]
    · exact (Nat.choose_lt_two_pow _ _ hn).le

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

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

Разделы

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

Аффилиация

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