English
If a finite collection s(i) ∈ C are pairwise disjoint for i ∈ S, then m(⋃_{i∈S} s(i)) = ∑_{i∈S} m(s(i)).
Русский
Если множество s(i) ∈ C разбито на конечном наборе индексов S на пары, тогда сумма равна значению объединения.
LaTeX
$$m(\bigcup_{i \in S} s(i)) = \sum_{i \in S} m(s(i))$$
Lean4
theorem addContent_biUnion_eq {ι : Type*} (hC : IsSetRing C) {s : ι → Set α} {S : Finset ι} (hs : ∀ n ∈ S, s n ∈ C)
(hS : (S : Set ι).PairwiseDisjoint s) : m (⋃ i ∈ S, s i) = ∑ i ∈ S, m (s i) := by
classical
induction S using Finset.induction with
| empty => simp
| insert i S hiS h =>
rw [Finset.sum_insert hiS]
simp_rw [← Finset.mem_coe, Finset.coe_insert, Set.biUnion_insert]
simp only [Finset.mem_insert, forall_eq_or_imp] at hs
simp only [Finset.coe_insert, Set.pairwiseDisjoint_insert] at hS
rw [← h hs.2 hS.1]
refine addContent_union hC hs.1 (hC.biUnion_mem S hs.2) ?_
rw [disjoint_iUnion₂_right]
exact fun j hjS ↦ hS.2 j hjS (ne_of_mem_of_not_mem hjS hiS).symm
