Theorems · Theorem · measure theory

MeasureTheory.addContent_iUnion_eq_sum_of_tendsto_zero

∀ {α : Type u_1} {C : Set (Set α)},
  MeasureTheory.IsSetRing C →
    ∀ (m : MeasureTheory.AddContent ENNReal C),
      (∀ s ∈ C, m s ≠ ⊤) →
        (∀ ⦃s : ℕ → Set α⦄,
            (∀ (n : ℕ), s n ∈ C) →
              Antitone s → ⋂ n, s n = ∅ → Filter.Tendsto (fun n => m (s n)) Filter.atTop (nhds 0)) →
          ∀ ⦃f : ℕ → Set α⦄,
            (∀ (i : ℕ), f i ∈ C) →
              ⋃ i, f i ∈ C → Pairwise (Function.onFun Disjoint f) → m (⋃ i, f i) = ∑' (i : ℕ), m (f i)

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.

Defined in

Mathlib.MeasureTheory.Measure.AddContent

Cited by

2 results in Mathlib

Foundations

Depth 134 from the axioms · uses propext, Classical.choice, Quot.sound