English
For a finite index set S and S.toSet.PairwiseDisjoint s with all s(i) ∈ C, m(⋃ i∈S s(i)) = ∑ i∈S m(s(i)).
Русский
Для конечного набора индексов S и попарно непересекающихся s(i) ∈ C, сумма значений m равна значению объединения.
LaTeX
$$m(\bigcup_{i \in S} s(i)) = \sum_{i \in S} m(s(i))$$
Lean4
/-- A function which is additive on disjoint elements in a ring of sets `C` defines an
additive content on `C`. -/
def addContent_of_union (m : Set α → ℝ≥0∞) (hC : IsSetRing C) (m_empty : m ∅ = 0)
(m_add : ∀ {s t : Set α} (_hs : s ∈ C) (_ht : t ∈ C), Disjoint s t → m (s ∪ t) = m s + m t) : AddContent C
where
toFun := m
empty' := m_empty
sUnion' I h_ss h_dis
h_mem := by
classical
induction I using Finset.induction with
| empty => simp only [Finset.coe_empty, Set.sUnion_empty, Finset.sum_empty, m_empty]
| insert s I hsI h =>
rw [Finset.coe_insert] at *
rw [Set.insert_subset_iff] at h_ss
rw [Set.pairwiseDisjoint_insert_of_notMem] at h_dis
swap; · exact hsI
have h_sUnion_mem : ⋃₀ ↑I ∈ C := by
rw [Set.sUnion_eq_biUnion]
apply hC.biUnion_mem
intro n hn
exact h_ss.2 hn
rw [Set.sUnion_insert, m_add h_ss.1 h_sUnion_mem (Set.disjoint_sUnion_right.mpr h_dis.2), Finset.sum_insert hsI,
h h_ss.2 h_dis.1]
rwa [Set.sUnion_insert] at h_mem
