centralBinom_pos

Mathlib.Data.Nat.Choose.Central

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

English

For every n, 0 < centralBinom(n).

Русский

Для любого n выполняется 0 < centralBinom(n).

LaTeX

$$$$ 0 < \\binom{2n}{n}. $$$$

Lean4

theorem centralBinom_pos (n : ℕ) : 0 < centralBinom n :=
  choose_pos (Nat.le_mul_of_pos_left _ zero_lt_two)

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

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

Разделы

Аффилиация

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