fwdDiff_finset_sum — Mathlib

English

Forward difference commutes with finite sums: Δ_h (∑_{k∈s} f(k)) = ∑_{k∈s} Δ_h (f(k)).

Русский

Передняя разность коммутирует сложение по конечному множеству: Δ_h (∑_{k∈s} f(k)) = ∑_{k∈s} Δ_h (f(k)).

LaTeX

$$$ \Delta_h \left( \sum_{k \in s} f(k) \right) = \sum_{k \in s} \Delta_h (f(k)) $$$

Lean4

@[simp]
theorem fwdDiff_finset_sum {α : Type*} (s : Finset α) (f : α → M → G) : Δ_[h] (∑ k ∈ s, f k) = ∑ k ∈ s, Δ_[h] (f k) :=
  map_sum (fwdDiffₗ M G h) f s

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