Theorems · Theorem · group theory

finsum_mem_biUnion

∀ {α : Type u_1} {ι : Type u_3} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {I : Set ι} {t : ι → Set α},
  I.PairwiseDisjoint t →
    I.Finite →
      (∀ i ∈ I, (t i).Finite) →
        ∑ᶠ (a : α) (_ : a ∈ ⋃ x ∈ I, t x), f a = ∑ᶠ (i : ι) (_ : i ∈ I) (j : α) (_ : j ∈ t i), f j

Given a family of sets t : ι → Set α, a finite set I in the index type such that all sets t i, i ∈ I, are finite, if all t i, i ∈ I, are pairwise disjoint, then the sum of f a over a ∈ ⋃ i ∈ I, t i is equal to the sum over i ∈ I of the sums of f a over a ∈ t i.

Defined in

Mathlib.Algebra.BigOperators.Finprod

Cited by

2 results in Mathlib

Foundations

Depth 88 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoid