Theorems · Theorem · measure theory

MeasureTheory.addContent_iUnion_eq_tsum_of_disjoint_of_IsSigmaSubadditive

∀ {α : Type u_1} {C : Set (Set α)} {m : MeasureTheory.AddContent ENNReal C},
  MeasureTheory.IsSetSemiring C →
    m.IsSigmaSubadditive →
      ∀ (f : ℕ → Set α),
        (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Function.onFun Disjoint f) → m (⋃ i, f i) = ∑' (i : ℕ), m (f i)

If an AddContent is σ-subadditive on a semi-ring of sets, then it is σ-additive.

Defined in

Mathlib.MeasureTheory.Measure.AddContent

Cited by

0 results in Mathlib

Foundations

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