Documentation
LeanPool
.
SardMoreira
.
MeasureNNReal
Search
return to top
source
Imports
Init
LeanPool.SardMoreira.MeasureComap
Mathlib.MeasureTheory.Measure.Haar.OfBasis
Imported by
instMeasureSpaceNNRealLeanPool
NNReal
.
volume_def
instSigmaFiniteNNRealVolume_leanPool
LeanPool.SardMoreira.MeasureNNReal
#
source
@[implicit_reducible]
noncomputable instance
instMeasureSpaceNNRealLeanPool
:
MeasureTheory.MeasureSpace
NNReal
Equations
instMeasureSpaceNNRealLeanPool
=
{
toMeasurableSpace
:=
NNReal.measurableSpace
,
volume
:=
MeasureTheory.Measure.comap
NNReal.toReal
MeasureTheory.volume
}
source
theorem
NNReal
.
volume_def
:
MeasureTheory.volume
=
MeasureTheory.Measure.comap
toReal
MeasureTheory.volume
source
instance
instSigmaFiniteNNRealVolume_leanPool
:
MeasureTheory.SigmaFinite
MeasureTheory.volume