The canonical measure on the unit interval

This file provides a MeasureTheory.MeasureSpace instance on unitInterval, and shows it is a probability measure.

noncomputable instance unitInterval.instMeasureSpaceElemRealUnitInterval : MeasureTheory.MeasureSpace ↑unitInterval

Equations

• unitInterval.instMeasureSpaceElemRealUnitInterval = MeasureTheory.Measure.Subtype.measureSpace

theorem unitInterval.volume_def : MeasureTheory.volume = MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume

instance unitInterval.instIsProbabilityMeasureElemRealUnitIntervalToMeasurableSpaceInstMeasureSpaceElemRealUnitIntervalVolume : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

Equations

• unitInterval.instIsProbabilityMeasureElemRealUnitIntervalToMeasurableSpaceInstMeasureSpaceElemRealUnitIntervalVolume = ⋯

theorem unitInterval.measurable_symm : Measurable unitInterval.symm