English
Let f: α → ENNReal and let {t_i} be a family of subsets of α that partitions the entire space into pairwise disjoint pieces (i.e., ⋃_i t_i = α and t_i ∩ t_j = ∅ for i ≠ j). Then the sum of f over the union equals the sum of sums over each piece: ∑_{x ∈ ⋃_i t_i} f(x) = ∑_i ∑_{x ∈ t_i} f(x).
Русский
Пусть f: α → ENNReal и пусть семейство множеств {t_i} разрезает всё множество на попарно непересекающиеся части, причём ⋃_i t_i = α и t_i ∩ t_j = ∅ при i ≠ j. Тогда сумма по объединению равна сумме сумм по частям: ∑_{x ∈ ⋃_i t_i} f(x) = ∑_i ∑_{x ∈ t_i} f(x).
LaTeX
$$$\sum_{x \in \bigcup_i t_i} f(x) = \sum_i \sum_{x \in t_i} f(x)$$$
Lean4
protected theorem tsum_biUnion {ι : Type*} {f : α → ENNReal} {t : ι → Set α} (h : Set.univ.PairwiseDisjoint t) :
∑' x : ⋃ i, t i, f x = ∑' (i) (x : t i), f x :=
by
nth_rw 2 [← tsum_univ]
rw [← ENNReal.tsum_biUnion' h, Set.biUnion_univ]
