English
If m is a σ-subadditive AddContent on a σ-set semiring C, then it is σ-additive: for a sequence f: ℕ → Set α with each f(i) ∈ C, and ⋃ i f(i) ∈ C and the f(i) pairwise disjoint, we have m(⋃ i f(i)) = ∑' i m(f(i)).
Русский
Если AddContent m на σ-полураме C σ-подадитивен, то он σ-аддитивен: для последовательности множеств f(i)∈C, их объединение ∪ f(i)∈C и дискретная взаимная непересекаемость выполняется m(∪ f(i)) = ∑' i m(f(i)).
LaTeX
$$$$ m\left( \bigcup_{i} f(i) \right) = \sum_{i}^{\prime} m(f(i)). $$$$
Lean4
/-- If an `AddContent` is σ-subadditive on a semi-ring of sets, then it is σ-additive. -/
theorem addContent_iUnion_eq_tsum_of_disjoint_of_IsSigmaSubadditive {m : AddContent C} (hC : IsSetSemiring C)
(m_subadd : m.IsSigmaSubadditive) (f : ℕ → Set α) (hf : ∀ i, f i ∈ C) (hf_Union : (⋃ i, f i) ∈ C)
(hf_disj : Pairwise (Disjoint on f)) : m (⋃ i, f i) = ∑' i, m (f i) :=
addContent_iUnion_eq_tsum_of_disjoint_of_addContent_iUnion_le hC (fun _ hf hf_Union _ ↦ m_subadd hf hf_Union) f hf
hf_Union hf_disj
