Measure

📁 Source: Mathlib/Geometry/Euclidean/Volume/Measure.lean

Statistics

Metric	Count
Definitions euclideanHausdorffMeasure, «termμHE[_]»	2
Theorems euclideanHausdorffMeasure_coe_image, euclideanHausdorffMeasure_eq, measurePreserving_vaddConst, euclideanHausdorffMeasure_eq_volume, euclideanHausdorffMeasure_eq_volume, euclideanHausdorffMeasure_image, euclideanHausdorffMeasure_preimage, map_euclideanHausdorffMeasure, measurePreserving_euclideanHausdorffMeasure, addHaarScalarFactor_volume_hausdorffMeasure_ne_zero, euclideanHausdorffMeasure_def, euclideanHausdorffMeasure_smul₀, euclideanHausdorffMeasure_zero, euclideanHausdorffMeasure_zero_or_top, euclideanHausdorffMeasure_homothety_image, euclideanHausdorffMeasure_homothety_preimage, isAddHaarMeasure_euclideanHausdorffMeasure, instIsAddHaarMeasureEuclideanSpaceRealFinHausdorffMeasureCast, instIsAddLeftInvariantEuclideanHausdorffMeasureOfIsIsometricVAdd, instIsAddRightInvariantEuclideanHausdorffMeasureOfIsIsometricVAddAddOpposite, instVAddInvariantMeasureEuclideanHausdorffMeasureOfIsIsometricVAdd	21
Total	23

AffineSubspace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
euclideanHausdorffMeasure_coe_image 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.Measure.euclideanHausdorffMeasure MetricSpace.toEMetricSpace Set.image AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership instSetLike Subtype.instMeasurableSpace instEMetricSpaceSubtype Subtype.borelSpace UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace	—	Isometry.euclideanHausdorffMeasure_image Subtype.borelSpace isometry_subtype_coe

EuclideanGeometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
euclideanHausdorffMeasure_eq 📖	mathematical	—	MeasureTheory.Measure.euclideanHausdorffMeasure MetricSpace.toEMetricSpace Module.finrank Real Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike MeasureTheory.Measure.map MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace DFunLike.coe IsometryEquiv PseudoMetricSpace.toPseudoEMetricSpace MetricSpace.toPseudoMetricSpace EquivLike.toFunLike IsometryEquiv.instEquivLike IsometryEquiv.vaddConst MeasureTheory.MeasureSpace.volume	—	MeasureTheory.MeasurePreserving.map_eq IsometryEquiv.measurePreserving_euclideanHausdorffMeasure InnerProductSpace.euclideanHausdorffMeasure_eq_volume
measurePreserving_vaddConst 📖	mathematical	—	MeasureTheory.MeasurePreserving MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace DFunLike.coe IsometryEquiv PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MetricSpace.toPseudoMetricSpace EquivLike.toFunLike IsometryEquiv.instEquivLike IsometryEquiv.vaddConst MeasureTheory.MeasureSpace.volume MeasureTheory.Measure.euclideanHausdorffMeasure MetricSpace.toEMetricSpace Module.finrank Real Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike	—	Homeomorph.measurable BorelSpace.opensMeasurable euclideanHausdorffMeasure_eq

EuclideanSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
euclideanHausdorffMeasure_eq_volume 📖	mathematical	—	MeasureTheory.Measure.euclideanHausdorffMeasure EuclideanSpace Real PiLp.instEMetricSpace ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal fact_one_le_two_ennreal Fin.fintype MetricSpace.toEMetricSpace Real.metricSpace WithLp.measurableSpace MeasurableSpace.pi Real.measurableSpace PiLp.borelSpace instCountableFin UniformSpace.toTopologicalSpace Real.borelSpace instSecondCountableTopologyReal MeasureTheory.MeasureSpace.volume measureSpaceOfInnerProductSpace PiLp.normedAddCommGroup Real.normedAddCommGroup PiLp.innerProductSpace Real.instRCLike RCLike.toInnerProductSpaceReal WithLp.instModuleFinite DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Real.instDivisionRing Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup Pi.module Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid NormedSpace.toModule FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.rclike_to_real	—	fact_one_le_two_ennreal PiLp.borelSpace instCountableFin Real.borelSpace instSecondCountableTopologyReal WithLp.instModuleFinite FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.rclike_to_real IsScalarTower.right SeminormedAddCommGroup.toIsTopologicalAddGroup instIsAddHaarMeasureEuclideanSpaceRealFinHausdorffMeasureCast MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts instIsAddHaarMeasureVolume MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant MeasureTheory.Measure.euclideanHausdorffMeasure_def MeasureTheory.Measure.isAddLeftInvariant_eq_smul locallyCompact_of_proper FiniteDimensional.proper_real PiLp.secondCountableTopology

InnerProductSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
euclideanHausdorffMeasure_eq_volume 📖	mathematical	—	MeasureTheory.Measure.euclideanHausdorffMeasure MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Module.finrank Real Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField toNormedSpace Real.instRCLike MeasureTheory.MeasureSpace.volume measureSpaceOfInnerProductSpace	—	fact_one_le_two_ennreal WithLp.instModuleFinite FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.rclike_to_real PiLp.borelSpace Finite.to_countable Real.borelSpace instSecondCountableTopologyReal RingHomInvPair.ids MeasureTheory.MeasurePreserving.map_eq OrthonormalBasis.measurePreserving_repr_symm instCountableFin IsometryEquiv.measurePreserving_euclideanHausdorffMeasure EuclideanSpace.euclideanHausdorffMeasure_eq_volume

Isometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
euclideanHausdorffMeasure_image 📖	mathematical	Isometry EMetricSpace.toPseudoEMetricSpace	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.Measure.euclideanHausdorffMeasure Set.image	—	IsScalarTower.right fact_one_le_two_ennreal SeminormedAddCommGroup.toIsTopologicalAddGroup WithLp.instModuleFinite FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.rclike_to_real PiLp.borelSpace instCountableFin Real.borelSpace instSecondCountableTopologyReal instIsAddHaarMeasureEuclideanSpaceRealFinHausdorffMeasureCast MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts instIsAddHaarMeasureVolume MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant MeasureTheory.Measure.euclideanHausdorffMeasure_def hausdorffMeasure_image Real.instIsOrderedRing
euclideanHausdorffMeasure_preimage 📖	mathematical	Isometry EMetricSpace.toPseudoEMetricSpace	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.Measure.euclideanHausdorffMeasure Set.preimage Set.instInter Set.range	—	IsScalarTower.right fact_one_le_two_ennreal SeminormedAddCommGroup.toIsTopologicalAddGroup WithLp.instModuleFinite FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.rclike_to_real PiLp.borelSpace instCountableFin Real.borelSpace instSecondCountableTopologyReal instIsAddHaarMeasureEuclideanSpaceRealFinHausdorffMeasureCast MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts instIsAddHaarMeasureVolume MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant MeasureTheory.Measure.euclideanHausdorffMeasure_def hausdorffMeasure_preimage Real.instIsOrderedRing
map_euclideanHausdorffMeasure 📖	mathematical	Isometry EMetricSpace.toPseudoEMetricSpace	MeasureTheory.Measure.map MeasureTheory.Measure.euclideanHausdorffMeasure MeasureTheory.Measure.restrict Set.range	—	IsScalarTower.right fact_one_le_two_ennreal SeminormedAddCommGroup.toIsTopologicalAddGroup WithLp.instModuleFinite FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.rclike_to_real PiLp.borelSpace instCountableFin Real.borelSpace instSecondCountableTopologyReal instIsAddHaarMeasureEuclideanSpaceRealFinHausdorffMeasureCast MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts instIsAddHaarMeasureVolume MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant MeasureTheory.Measure.euclideanHausdorffMeasure_def MeasureTheory.Measure.map_smul map_hausdorffMeasure Real.instIsOrderedRing MeasureTheory.Measure.restrict_smul

IsometryEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurePreserving_euclideanHausdorffMeasure 📖	mathematical	—	MeasureTheory.MeasurePreserving DFunLike.coe IsometryEquiv EMetricSpace.toPseudoEMetricSpace EquivLike.toFunLike instEquivLike MeasureTheory.Measure.euclideanHausdorffMeasure	—	MeasureTheory.MeasurePreserving.smul_measure measurePreserving_hausdorffMeasure fact_one_le_two_ennreal instIsAddHaarMeasureEuclideanSpaceRealFinHausdorffMeasureCast

MeasureTheory

Definitions

Name	Category	Theorems
«termμHE[_]» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
euclideanHausdorffMeasure_homothety_image 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Measure.euclideanHausdorffMeasure MetricSpace.toEMetricSpace Set.image AffineMap CommRing.toRing EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineMap.instFunLike AffineMap.homothety NNReal Algebra.toSMul NNReal.instCommSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NNReal.instSemiring NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing	—	IsScalarTower.right fact_one_le_two_ennreal SeminormedAddCommGroup.toIsTopologicalAddGroup WithLp.instModuleFinite FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.rclike_to_real PiLp.borelSpace instCountableFin Real.borelSpace instSecondCountableTopologyReal instIsAddHaarMeasureEuclideanSpaceRealFinHausdorffMeasureCast Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts instIsAddHaarMeasureVolume Measure.IsAddHaarMeasure.toIsAddLeftInvariant Measure.euclideanHausdorffMeasure_def hausdorffMeasure_homothety_image Real.instIsOrderedRing SMulCommClass.smul_comm ENNReal.smulCommClass_left ENNReal.smulCommClass_right Algebra.to_smulCommClass NNReal.rpow_natCast
euclideanHausdorffMeasure_homothety_preimage 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Measure.euclideanHausdorffMeasure MetricSpace.toEMetricSpace Set.preimage AffineMap CommRing.toRing EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineMap.instFunLike AffineMap.homothety NNReal Algebra.toSMul NNReal.instCommSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NNReal.instSemiring NNReal.instInv NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing	—	IsScalarTower.right fact_one_le_two_ennreal SeminormedAddCommGroup.toIsTopologicalAddGroup WithLp.instModuleFinite FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.rclike_to_real PiLp.borelSpace instCountableFin Real.borelSpace instSecondCountableTopologyReal instIsAddHaarMeasureEuclideanSpaceRealFinHausdorffMeasureCast Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts instIsAddHaarMeasureVolume Measure.IsAddHaarMeasure.toIsAddLeftInvariant Measure.euclideanHausdorffMeasure_def hausdorffMeasure_homothety_preimage Real.instIsOrderedRing SMulCommClass.smul_comm ENNReal.smulCommClass_left ENNReal.smulCommClass_right Algebra.to_smulCommClass NNReal.rpow_natCast
isAddHaarMeasure_euclideanHausdorffMeasure 📖	mathematical	—	Measure.IsAddHaarMeasure NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Measure.euclideanHausdorffMeasure MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Module.finrank Real Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField	—	IsScalarTower.right fact_one_le_two_ennreal SeminormedAddCommGroup.toIsTopologicalAddGroup WithLp.instModuleFinite FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.rclike_to_real PiLp.borelSpace instCountableFin Real.borelSpace instSecondCountableTopologyReal instIsAddHaarMeasureEuclideanSpaceRealFinHausdorffMeasureCast Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts instIsAddHaarMeasureVolume Measure.IsAddHaarMeasure.toIsAddLeftInvariant Measure.euclideanHausdorffMeasure_def ENNReal.smul_def Measure.IsAddHaarMeasure.smul isAddHaarMeasure_hausdorffMeasure Measure.addHaarScalarFactor_volume_hausdorffMeasure_ne_zero

MeasureTheory.Measure

Definitions

Name	Category	Theorems
euclideanHausdorffMeasure 📖	CompOp	19 math math: EuclideanGeometry.euclideanHausdorffMeasure_eq, euclideanHausdorffMeasure_zero, instIsAddLeftInvariantEuclideanHausdorffMeasureOfIsIsometricVAdd, euclideanHausdorffMeasure_zero_or_top, instVAddInvariantMeasureEuclideanHausdorffMeasureOfIsIsometricVAdd, MeasureTheory.euclideanHausdorffMeasure_homothety_image, MeasureTheory.euclideanHausdorffMeasure_homothety_preimage, EuclideanGeometry.measurePreserving_vaddConst, Isometry.euclideanHausdorffMeasure_image, Isometry.map_euclideanHausdorffMeasure, InnerProductSpace.euclideanHausdorffMeasure_eq_volume, instIsAddRightInvariantEuclideanHausdorffMeasureOfIsIsometricVAddAddOpposite, EuclideanSpace.euclideanHausdorffMeasure_eq_volume, euclideanHausdorffMeasure_smul₀, MeasureTheory.isAddHaarMeasure_euclideanHausdorffMeasure, IsometryEquiv.measurePreserving_euclideanHausdorffMeasure, Isometry.euclideanHausdorffMeasure_preimage, AffineSubspace.euclideanHausdorffMeasure_coe_image, euclideanHausdorffMeasure_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addHaarScalarFactor_volume_hausdorffMeasure_ne_zero 📖	—	—	—	—	fact_one_le_two_ennreal SeminormedAddCommGroup.toIsTopologicalAddGroup WithLp.instModuleFinite FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.rclike_to_real PiLp.borelSpace instCountableFin Real.borelSpace instSecondCountableTopologyReal instIsAddHaarMeasureEuclideanSpaceRealFinHausdorffMeasureCast IsAddHaarMeasure.toIsFiniteMeasureOnCompacts instIsAddHaarMeasureVolume IsAddHaarMeasure.toIsAddLeftInvariant IsScalarTower.right OrthonormalBasis.volume_parallelepiped MulZeroClass.zero_mul NeZero.charZero_one ENNReal.instCharZero isAddLeftInvariant_eq_smul locallyCompact_of_proper FiniteDimensional.proper_real PiLp.secondCountableTopology
euclideanHausdorffMeasure_def 📖	mathematical	—	euclideanHausdorffMeasure NNReal MeasureTheory.Measure instSMul Algebra.toSMul ENNReal NNReal.instCommSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id IsScalarTower.right addHaarScalarFactor EuclideanSpace Real PiLp.topologicalSpace instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup PiLp.normedAddCommGroup fact_one_le_two_ennreal Fin.fintype Real.normedAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup PiLp.seminormedAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace PiLp.innerProductSpace Real.instRCLike RCLike.toInnerProductSpaceReal WithLp.instModuleFinite DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Real.instDivisionRing Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup Pi.module Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid NormedSpace.toModule FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.rclike_to_real WithLp.measurableSpace MeasurableSpace.pi Real.measurableSpace PiLp.borelSpace instCountableFin Real.borelSpace instSecondCountableTopologyReal MeasureTheory.MeasureSpace.volume hausdorffMeasure PiLp.instEMetricSpace MetricSpace.toEMetricSpace Real.metricSpace Real.instNatCast instIsAddHaarMeasureEuclideanSpaceRealFinHausdorffMeasureCast IsAddHaarMeasure.toIsFiniteMeasureOnCompacts instIsAddHaarMeasureVolume IsAddHaarMeasure.toIsAddLeftInvariant SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	—
euclideanHausdorffMeasure_smul₀ 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike euclideanHausdorffMeasure MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NNReal Algebra.toSMul NNReal.instCommSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id Monoid.toPow NNReal.instSemiring NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing NormedDivisionRing.toNormedRing	—	IsScalarTower.right fact_one_le_two_ennreal SeminormedAddCommGroup.toIsTopologicalAddGroup WithLp.instModuleFinite FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.rclike_to_real PiLp.borelSpace instCountableFin Real.borelSpace instSecondCountableTopologyReal instIsAddHaarMeasureEuclideanSpaceRealFinHausdorffMeasureCast IsAddHaarMeasure.toIsFiniteMeasureOnCompacts instIsAddHaarMeasureVolume IsAddHaarMeasure.toIsAddLeftInvariant euclideanHausdorffMeasure_def smul_apply hausdorffMeasure_smul₀ Real.instIsOrderedRing SMulCommClass.smul_comm ENNReal.smulCommClass_left ENNReal.smulCommClass_right Algebra.to_smulCommClass NNReal.rpow_natCast
euclideanHausdorffMeasure_zero 📖	mathematical	—	euclideanHausdorffMeasure hausdorffMeasure Real Real.instZero	—	fact_one_le_two_ennreal Set.image_congr Finset.sum_congr Finset.univ_eq_empty Fin.isEmpty' Set.Nonempty.image_const Matrix.zero_empty Unique.instSubsingleton IsScalarTower.right SeminormedAddCommGroup.toIsTopologicalAddGroup WithLp.instModuleFinite FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.rclike_to_real PiLp.borelSpace instCountableFin Real.borelSpace instSecondCountableTopologyReal instIsAddHaarMeasureEuclideanSpaceRealFinHausdorffMeasureCast IsAddHaarMeasure.toIsFiniteMeasureOnCompacts instIsAddHaarMeasureVolume IsAddHaarMeasure.toIsAddLeftInvariant euclideanHausdorffMeasure_def hausdorffMeasure.congr_simp CharP.cast_eq_zero CharP.ofCharZero RCLike.charZero_rclike addHaarScalarFactor.congr_simp mul_one hausdorffMeasure_zero_singleton OrthonormalBasis.volume_parallelepiped isAddLeftInvariant_eq_smul AlexandrovDiscrete.toLocallyCompactSpace Finite.toAlexandrovDiscrete PiLp.secondCountableTopology one_smul
euclideanHausdorffMeasure_zero_or_top 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike euclideanHausdorffMeasure instZeroENNReal Top.top instTopENNReal	—	IsScalarTower.right fact_one_le_two_ennreal SeminormedAddCommGroup.toIsTopologicalAddGroup WithLp.instModuleFinite FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.rclike_to_real PiLp.borelSpace instCountableFin Real.borelSpace instSecondCountableTopologyReal instIsAddHaarMeasureEuclideanSpaceRealFinHausdorffMeasureCast IsAddHaarMeasure.toIsFiniteMeasureOnCompacts instIsAddHaarMeasureVolume IsAddHaarMeasure.toIsAddLeftInvariant euclideanHausdorffMeasure_def hausdorffMeasure_zero_or_top IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike smul_zero smul_apply ENNReal.smul_top instIsDomain DivisionSemiring.to_moduleIsTorsionFree

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsAddHaarMeasureEuclideanSpaceRealFinHausdorffMeasureCast 📖	mathematical	—	MeasureTheory.Measure.IsAddHaarMeasure EuclideanSpace Real NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup PiLp.normedAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal fact_one_le_two_ennreal Fin.fintype Real.normedAddCommGroup PiLp.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace WithLp.measurableSpace MeasurableSpace.pi Real.measurableSpace MeasureTheory.Measure.hausdorffMeasure PiLp.instEMetricSpace MetricSpace.toEMetricSpace Real.metricSpace PiLp.borelSpace instCountableFin Real.borelSpace instSecondCountableTopologyReal Real.instNatCast	—	fact_one_le_two_ennreal PiLp.borelSpace instCountableFin Real.borelSpace instSecondCountableTopologyReal MeasureTheory.Measure.hausdorffMeasure.congr_simp finrank_euclideanSpace Fintype.card_fin MeasureTheory.isAddHaarMeasure_hausdorffMeasure WithLp.instModuleFinite FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.rclike_to_real
instIsAddLeftInvariantEuclideanHausdorffMeasureOfIsIsometricVAdd 📖	mathematical	—	MeasureTheory.Measure.IsAddLeftInvariant AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid MeasureTheory.Measure.euclideanHausdorffMeasure	—	IsScalarTower.right fact_one_le_two_ennreal SeminormedAddCommGroup.toIsTopologicalAddGroup WithLp.instModuleFinite FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.rclike_to_real PiLp.borelSpace instCountableFin Real.borelSpace instSecondCountableTopologyReal instIsAddHaarMeasureEuclideanSpaceRealFinHausdorffMeasureCast MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts instIsAddHaarMeasureVolume MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant MeasureTheory.Measure.euclideanHausdorffMeasure_def MeasureTheory.isAddLeftInvariant_smul_nnreal MeasureTheory.instIsAddLeftInvariantHausdorffMeasureOfIsIsometricVAdd
instIsAddRightInvariantEuclideanHausdorffMeasureOfIsIsometricVAddAddOpposite 📖	mathematical	—	MeasureTheory.Measure.IsAddRightInvariant AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid MeasureTheory.Measure.euclideanHausdorffMeasure	—	IsScalarTower.right fact_one_le_two_ennreal SeminormedAddCommGroup.toIsTopologicalAddGroup WithLp.instModuleFinite FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.rclike_to_real PiLp.borelSpace instCountableFin Real.borelSpace instSecondCountableTopologyReal instIsAddHaarMeasureEuclideanSpaceRealFinHausdorffMeasureCast MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts instIsAddHaarMeasureVolume MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant MeasureTheory.Measure.euclideanHausdorffMeasure_def MeasureTheory.isAddRightInvariant_smul_nnreal MeasureTheory.instIsAddRightInvariantHausdorffMeasureOfIsIsometricVAddAddOpposite
instVAddInvariantMeasureEuclideanHausdorffMeasureOfIsIsometricVAdd 📖	mathematical	—	MeasureTheory.VAddInvariantMeasure AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction MeasureTheory.Measure.euclideanHausdorffMeasure	—	IsScalarTower.right fact_one_le_two_ennreal SeminormedAddCommGroup.toIsTopologicalAddGroup WithLp.instModuleFinite FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.rclike_to_real PiLp.borelSpace instCountableFin Real.borelSpace instSecondCountableTopologyReal instIsAddHaarMeasureEuclideanSpaceRealFinHausdorffMeasureCast MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts instIsAddHaarMeasureVolume MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant MeasureTheory.Measure.euclideanHausdorffMeasure_def MeasureTheory.VAddInvariantMeasure.vadd_nnreal MeasureTheory.instVAddInvariantMeasureHausdorffMeasureOfIsIsometricVAdd

---

← Back to Index