Theorems · Definition · measure theory

MeasureTheory.AddContent.measure

{α : Type u_1} →
  {C : Set (Set α)} →
    [mα : MeasurableSpace α] →
      (m : MeasureTheory.AddContent ENNReal C) →
        MeasureTheory.IsSetSemiring C →
          mα ≤ MeasurableSpace.generateFrom C → m.IsSigmaSubadditive → MeasureTheory.Measure α

Construct a measure from a sigma-subadditive content on a semiring, assuming the semiring generates a given measurable structure. The measure is defined on this measurable structure.

Defined in

Mathlib.MeasureTheory.OuterMeasure.OfAddContent

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasurableSpace