choose_ne_zero

Mathlib.Data.Nat.Choose.Basic

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

English

If k ≤ n then nCk ≠ 0.

Русский

Если k ≤ n, то nCk ≠ 0.

LaTeX

$$$\\\\forall {n,k \\\\in \\\\mathbb{N}}, \\\\ k \\\\le n \\\\Rightarrow \\\\binom{n}{k} \\\\neq 0$$$

Lean4

theorem choose_ne_zero {n k : ℕ} (h : k ≤ n) : n.choose k ≠ 0 :=
  (choose_pos h).ne'

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

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

Разделы

Аффилиация

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