choose_succ_left

Mathlib.Data.Nat.Choose.Basic

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

← MathLib Explorer

English

If k > 0, then choose(n+1, k) = choose(n, k-1) + choose(n,k).

Русский

Если k > 0, то choose(n+1, k) = choose(n, k-1) + choose(n, k).

LaTeX

$$$\mathrm{choose}(n+1, k) = \mathrm{choose}(n, k-1) + \mathrm{choose}(n, k) \quad (k>0)$$$

Lean4

theorem choose_succ_left (n k : ℕ) (hk : 0 < k) : choose (n + 1) k = choose n (k - 1) + choose n k :=
  by
  obtain ⟨l, rfl⟩ : ∃ l, k = l + 1 := Nat.exists_eq_add_of_le' hk
  rfl

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

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

Разделы

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

Аффилиация

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