fwdDiff_choose

Mathlib.Algebra.Group.ForwardDiff

URI: https://scilib.ai/kg/mathlib#fwdDiff_choose

← MathLib Explorer

English

For all j ≥ 0, Δ_[1] (x ↦ x.choose (j + 1)) = x ↦ x.choose j.

Русский

Для любого j ≥ 0, Δ_[1] (x ↦ C(x, j+1)) = x ↦ C(x, j).

LaTeX

$$$ \Delta_1 \bigl(x \mapsto {x \choose j+1}\bigr) = x \mapsto {x \choose j} $$$

Lean4

theorem fwdDiff_choose (j : ℕ) : Δ_[1] (fun x ↦ x.choose (j + 1) : ℕ → ℤ) = fun x ↦ x.choose j :=
  by
  ext n
  simp only [fwdDiff, choose_succ_succ' n j, cast_add, add_sub_cancel_right]

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

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

Разделы

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

Аффилиация

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