mapRange_finset_sum — Mathlib

English

For a mapRange f and a Finset s of indices, the image of the Finset sum equals the Finset sum of images.

Русский

Для mapRange f и суммирования по конечному множеству индексов, образ суммы равен сумме образов.

LaTeX

$$mapRange f (map_zero f) (∑ x ∈ s, g x) = ∑ x ∈ s, mapRange f (map_zero f) (g x)$$

Lean4

theorem mapRange_finset_sum (f : F) (s : Finset ι) (g : ι → α →₀ M) :
    mapRange f (map_zero f) (∑ x ∈ s, g x) = ∑ x ∈ s, mapRange f (map_zero f) (g x) :=
  map_sum (mapRange.addMonoidHom (f : M →+ N)) _ _

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