LeanPool.SardMoreira.MeasureNNReal

@[implicit_reducible]

noncomputable instance instMeasureSpaceNNRealLeanPool : MeasureTheory.MeasureSpace NNReal

Equations

• instMeasureSpaceNNRealLeanPool = { toMeasurableSpace := NNReal.measurableSpace, volume := MeasureTheory.Measure.comap NNReal.toReal MeasureTheory.volume }

theorem NNReal.volume_def : MeasureTheory.volume = MeasureTheory.Measure.comap toReal MeasureTheory.volume

instance instSigmaFiniteNNRealVolume_leanPool : MeasureTheory.SigmaFinite MeasureTheory.volume