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.instMeasureSpaceElemReal : MeasureTheory.MeasureSpace ↑unitInterval

Equations

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

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

instance unitInterval.instIsProbabilityMeasureElemRealVolume : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

Equations

• unitInterval.instIsProbabilityMeasureElemRealVolume = ⋯

theorem unitInterval.measurable_symm : Measurable unitInterval.symm