sum_range_choose — Mathlib

English

A standard halfway estimate: the central binomial coefficient (2n choose n) is bounded by 4^n, giving a central growth bound.

Русский

Стандартная оценка посередине: центральный биномиальный коэффициент (2n choose n) ограничен сверху 4^n.

LaTeX

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

Lean4

/-- The sum of entries in a row of Pascal's triangle -/
theorem sum_range_choose (n : ℕ) : (∑ m ∈ range (n + 1), n.choose m) = 2 ^ n :=
  by
  have := (add_pow 1 1 n).symm
  simpa [one_add_one_eq_two] using this

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