Theorems · Theorem · measure theory

MeasureTheory.preVariation.iUnion

∀ {X : Type u_1} [inst : MeasurableSpace X] {f : Set X → ENNReal},
  MeasureTheory.IsSigmaSubadditiveSetFun f →
    f ∅ = 0 →
      ∀ (s : ℕ → Set X),
        (∀ (i : ℕ), MeasurableSet (s i)) →
          Pairwise (Function.onFun Disjoint s) →
            HasSum (fun i => MeasureTheory.preVariationFun f (s i)) (MeasureTheory.preVariationFun f (⋃ i, s i))

Additivity of preVariationFun for disjoint measurable sets.

Defined in

Mathlib.MeasureTheory.Measure.PreVariation

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpace