Theorems · Theorem · measure theory

MeasureTheory.VectorMeasure.exists_extension_of_isSetSemiring_of_le_measure

∀ {α : Type u_1} {hα : MeasurableSpace α} {E : Type u_2} [inst : NormedAddCommGroup E] [CompleteSpace E]
  {μ : MeasureTheory.Measure α} [NormedSpace ℝ E] [MeasureTheory.IsFiniteMeasure μ] {C : Set (Set α)}
  {m : MeasureTheory.AddContent E C},
  MeasureTheory.IsSetSemiring C →
    (∀ s ∈ C, ‖m s‖ₑ ≤ μ s) → (∀ s ∈ C, MeasurableSet s) → ∃ m', (∀ s ∈ C, m' s = m s) ∧ ∀ (s : Set α), ‖m' s‖ₑ ≤ μ s

Consider an additive content m on a semi-ring of measurable sets C, which is dominated by a finite measure μ. Then m extends to a countably additive vector measure which is dominated by μ.

Defined in

Mathlib.MeasureTheory.VectorMeasure.AddContent

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupCompleteSpaceNormedSpaceMeasureTheory.IsFiniteMeasure