theorem
MeasureTheory.tendsto_zero_of_regular_addContent
{α : Type u_1}
{C : Set (Set α)}
{R : Set (Set α)}
{s : ℕ → Set α}
(hR : MeasureTheory.IsSetRing R)
(m : MeasureTheory.AddContent R)
(hs : ∀ (n : ℕ), s n ∈ R)
(hs_anti : Antitone s)
(hs_Inter : ⋂ (n : ℕ), s n = ∅)
(hC : IsCompactSystem C)
(hCR : C ⊆ R)
(h_reg : ∀ A ∈ R, ∀ (ε : ENNReal), 0 < ε → ∃ K ∈ C, K ⊆ A ∧ m (A \ K) ≤ ε)
:
Filter.Tendsto (fun (n : ℕ) => m (s n)) Filter.atTop (nhds 0)
theorem
MeasureTheory.AddContent.sigma_additive_of_regular
{α : Type u_1}
{C : Set (Set α)}
{R : Set (Set α)}
(hR : MeasureTheory.IsSetRing R)
(m : MeasureTheory.AddContent R)
(hm_ne_top : ∀ s ∈ R, m s ≠ ⊤)
(hC : IsCompactSystem C)
(hCR : C ⊆ R)
(h_reg : ∀ A ∈ R, ∀ (ε : ENNReal), 0 < ε → ∃ K ∈ C, K ⊆ A ∧ m (A \ K) ≤ ε)
⦃f : ℕ → Set α⦄
(hf : ∀ (i : ℕ), f i ∈ R)
(hUf : ⋃ (i : ℕ), f i ∈ R)
(h_disj : Pairwise (Disjoint on f))
: