Theorems · Theorem · measure theory

MeasureTheory.VectorMeasure.exists_extension_of_isSetRing_of_le_measure_of_dense

∀ {α : Type u_1} {hα : MeasurableSpace α} {E : Type u_2} [inst : NormedAddCommGroup E] [CompleteSpace E]
  {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {C : Set (Set α)} {m : MeasureTheory.AddContent E C},
  MeasureTheory.IsSetRing C →
    (∀ s ∈ C, MeasurableSet s) →
      (∀ s ∈ C, ‖m s‖ₑ ≤ μ s) →
        (∀ (t : Set α) (ε : ENNReal), MeasurableSet t → 0 < ε → ∃ s ∈ C, μ (symmDiff s t) < ε) →
          ∃ m', (∀ s ∈ C, m' s = m s) ∧ ∀ (s : Set α), ‖m' s‖ₑ ≤ μ s

Consider an additive content on a dense ring of sets. Assume that it is dominated by a finite positive measure. Then it extends to a countably additive vector measure.

Defined in

Mathlib.MeasureTheory.VectorMeasure.AddContent

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupCompleteSpaceMeasureTheory.IsFiniteMeasure