mapRange_multiset_sum — Mathlib

English

For a mapRange f and a multiset m of finitely supported functions, applying mapRange to the sum equals the sum of mapRange applied to each element.

Русский

При применении mapRange к сумме мульсетa функций FinSupp получается то же самое, что сумма применения mapRange к каждому элементу.

LaTeX

$$mapRange f (map_zero f) m.sum = (m.map (λ x, mapRange f (map_zero f) x)).sum$$

Lean4

theorem mapRange_multiset_sum (f : F) (m : Multiset (α →₀ M)) :
    mapRange f (map_zero f) m.sum = (m.map fun x => mapRange f (map_zero f) x).sum :=
  (mapRange.addMonoidHom (f : M →+ N) : (α →₀ _) →+ _).map_multiset_sum _

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