theorem
MeasureTheory.sigma_additive_addContent_of_tendsto_zero
{α : Type u_1}
{C : Set (Set α)}
(hC : MeasureTheory.IsSetRing C)
(m : MeasureTheory.AddContent C)
(hm_ne_top : ∀ s ∈ C, m s ≠ ⊤)
(hm_tendsto : ∀ ⦃s : ℕ → Set α⦄,
(∀ (n : ℕ), s n ∈ C) → Antitone s → ⋂ (n : ℕ), s n = ∅ → Filter.Tendsto (fun (n : ℕ) => m (s n)) Filter.atTop (nhds 0))
⦃f : ℕ → Set α⦄
(hf : ∀ (i : ℕ), f i ∈ C)
(hUf : ⋃ (i : ℕ), f i ∈ C)
(h_disj : Pairwise (Disjoint on f))
:
In a ring of sets, continuity of an additive content at ∅ implies σ-additivity.
This is not true in general in semirings, or without the hypothesis that m is finite. See the
examples 7 and 8 in Halmos' book Measure Theory (1974), page 40.
theorem
MeasureTheory.sUnion_eq_sum_of_union_eq_add
{α : Type u_1}
{C : Set (Set α)}
(hC_empty : ∅ ∈ C)
(hC_union : ∀ {s t : Set α}, s ∈ C → t ∈ C → s ∪ t ∈ C)
(m : Set α → ENNReal)
(m_empty : m ∅ = 0)
(m_add : ∀ {s t : Set α}, s ∈ C → t ∈ C → Disjoint s t → m (s ∪ t) = m s + m t)
(I : Finset (Set α))
(h_ss : ↑I ⊆ C)
(h_dis : (↑I).PairwiseDisjoint id)
(h_mem : ⋃₀ ↑I ∈ C)
:
theorem
MeasureTheory.sUnion_eq_sum_of_union_eq_add'
{α : Type u_1}
{C : Set (Set α)}
(hC_empty : ∅ ∈ C)
(hC_union : ∀ {s t : Set α}, s ∈ C → t ∈ C → s ∪ t ∈ C)
(m : (s : Set α) → s ∈ C → ENNReal)
(m_empty : m ∅ hC_empty = 0)
(m_add : ∀ {s t : Set α} (hs : s ∈ C) (ht : t ∈ C), Disjoint s t → m (s ∪ t) ⋯ = m s hs + m t ht)
(I : Finset (Set α))
(h_ss : ↑I ⊆ C)
(h_dis : (↑I).PairwiseDisjoint id)
(h_mem : ⋃₀ ↑I ∈ C)
: