choose_succ_right

Mathlib.Data.Nat.Choose.Basic

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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