choose_succ_le_two_pow — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem choose_succ_le_two_pow (n k : ℕ) : (n + 1).choose k ≤ 2 ^ n :=
  by
  by_cases lt : n + 1 < k
  · simp [choose_eq_zero_of_lt lt]
  ·
    cases n with
    | zero => cases k <;> simp_all
    | succ n =>
      rcases k with - | k
      · rw [choose_zero_right]
        exact Nat.one_le_two_pow
      · rw [choose_succ_succ', two_pow_succ]
        exact Nat.add_le_add (choose_succ_le_two_pow n k) (choose_succ_le_two_pow n (k + 1))

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