choose_le_centralBinom — Mathlib

English

For all r,n, (2n) choose r ≤ centralBinom(n).

Русский

Для всех r,n: (2n) choose r ≤ centralBinom(n).

LaTeX

$$$$ \\binom{2n}{r} \\le \\text{centralBinom}(n). $$$$

Lean4

/-- The central binomial coefficient is the largest binomial coefficient.
-/
theorem choose_le_centralBinom (r n : ℕ) : choose (2 * n) r ≤ centralBinom n :=
  calc
    (2 * n).choose r ≤ (2 * n).choose (2 * n / 2) := choose_le_middle r (2 * n)
    _ = (2 * n).choose n := by rw [Nat.mul_div_cancel_left n zero_lt_two]

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