fwdDiff_iter_choose — Mathlib

English

For all j, k ∈ ℕ, Δ_1^[k] (x ↦ x.choose (k + j)) = x ↦ x.choose j.

Русский

Для всех j,k ∈ ℕ, Δ_1^[k] (x ↦ x.choose (k + j)) = x ↦ x.choose j.

LaTeX

$$$ \Delta_1^{[k]} \bigl(x \mapsto {x \choose k+j}\bigr) = x \mapsto {x \choose j} $$$

Lean4

theorem fwdDiff_iter_choose (j k : ℕ) : Δ_[1]^[k] (fun x ↦ x.choose (k + j) : ℕ → ℤ) = fun x ↦ x.choose j := by
  induction k generalizing j with
  | zero => simp only [zero_add, iterate_zero, id_eq]
  | succ k IH => simp only [iterate_succ_apply', add_assoc, add_comm 1 j, IH, fwdDiff_choose]

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