two_le_centralBinom

Mathlib.Data.Nat.Choose.Central

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

← MathLib Explorer

English

If n > 0, then 2 ≤ centralBinom(n).

Русский

Если n > 0, то 2 ≤ centralBinom(n).

LaTeX

$$$$ 2 \\le \\binom{2n}{n}. $$$$

Lean4

theorem two_le_centralBinom (n : ℕ) (n_pos : 0 < n) : 2 ≤ centralBinom n :=
  calc
    2 ≤ 2 * n := Nat.le_mul_of_pos_right _ n_pos
    _ = (2 * n).choose 1 := (choose_one_right (2 * n)).symm
    _ ≤ centralBinom n := choose_le_centralBinom 1 n

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

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

Разделы

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

Аффилиация

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