EqHaar

📁 Source: Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean

Statistics

Metric	Count
Definitions measure, Icc01, piIcc01	3
Theorems measure_def, measure_parallelepiped, quasiMeasurePreserving, quasiMeasurePreserving, const_smul, addHaar_affineSubspace, addHaar_ball, addHaar_ball_center, addHaar_ball_mul, addHaar_ball_mul_of_pos, addHaar_ball_of_pos, addHaar_closedBall, addHaar_closedBall', addHaar_closedBall_center, addHaar_closedBall_eq_addHaar_ball, addHaar_closedBall_mul, addHaar_closedBall_mul_of_pos, addHaar_eq_zero_of_disjoint_translates, addHaar_eq_zero_of_disjoint_translates_aux, addHaar_image_continuousLinearEquiv, addHaar_image_continuousLinearMap, addHaar_image_homothety, addHaar_image_linearMap, addHaar_nnreal_smul, addHaar_parallelepiped, addHaar_preimage_continuousLinearEquiv, addHaar_preimage_continuousLinearMap, addHaar_preimage_linearEquiv, addHaar_preimage_linearMap, addHaar_preimage_smul, addHaar_real_ball_center, addHaar_real_closedBall, addHaar_real_closedBall', addHaar_real_closedBall_center, addHaar_real_closedBall_eq_addHaar_real_ball, addHaar_singleton_add_smul_div_singleton_add_smul, addHaar_smul, addHaar_smul_of_nonneg, addHaar_sphere, addHaar_sphere_of_ne_zero, addHaar_submodule, addHaar_unitClosedBall_eq_addHaar_unitBall, eventually_nonempty_inter_smul_of_density_one, instIsAddLeftInvariantMeasure, instIsLocallyFiniteMeasureMeasure, isUnifLocDoublingMeasureOfIsAddHaarMeasure, map_addHaar_smul, map_linearMap_addHaar_eq_smul_addHaar, map_linearMap_addHaar_pi_eq_smul_addHaar, quasiMeasurePreserving_smul, tendsto_addHaar_inter_smul_one_of_density_one, tendsto_addHaar_inter_smul_one_of_density_one_aux, tendsto_addHaar_inter_smul_zero_of_density_zero, tendsto_addHaar_inter_smul_zero_of_density_zero_aux1, tendsto_addHaar_inter_smul_zero_of_density_zero_aux2, addHaarMeasure_eq_volume, addHaarMeasure_eq_volume_pi, isAddHaarMeasure_volume_pi, map_addHaar, parallelepiped_basisFun, parallelepiped_eq_map	61
Total	64

AlternatingMap

Definitions

Name	Category	Theorems
measure 📖	CompOp	6 math math: MeasureTheory.Measure.instIsAddLeftInvariantMeasure, Orientation.measure_eq_volume, measure_def, measure_parallelepiped, MeasureTheory.Measure.instIsLocallyFiniteMeasureMeasure, Orientation.measure_orthonormalBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measure_def 📖	mathematical	—	measure NNReal MeasureTheory.Measure MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal NNReal.instCommSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id NNNorm.nnnorm Real SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing DFunLike.coe AlternatingMap Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField Real.instAddCommMonoid InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instFunLike Module.Basis Module.Basis.instFunLike Module.finBasisOfFinrankEq commRing_strongRankCondition Real.commRing Real.instNontrivial Module.Basis.addHaar Fin.fintype	—	commRing_strongRankCondition Real.instNontrivial
measure_parallelepiped 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike measure parallelepiped Fin.fintype NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup ENNReal.ofReal abs Real.lattice Real.instAddGroup AlternatingMap Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instFunLike	—	Algebra.to_smulCommClass commRing_strongRankCondition Real.instNontrivial Module.Free.of_divisionRing Fact.out eq_smul_basis_det measure_def MeasureTheory.Measure.addHaar_parallelepiped abs_mul Real.instIsOrderedRing ENNReal.ofReal_mul abs_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addHaarMeasure_eq_volume 📖	mathematical	—	Measure.addHaarMeasure Real Real.instAddGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instIsTopologicalAddGroupReal Real.measurableSpace Real.borelSpace TopologicalSpace.PositiveCompacts.Icc01 MeasureSpace.volume Real.measureSpace	—	instIsTopologicalAddGroupReal Real.borelSpace IsScalarTower.right Real.volume_Icc sub_zero ENNReal.ofReal_one one_smul Measure.addHaarMeasure_unique instSecondCountableTopologyReal Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace TopologicalSpace.SecondCountableTopology.to_separableSpace instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal Measure.IsAddHaarMeasure.toIsAddLeftInvariant
addHaarMeasure_eq_volume_pi 📖	mathematical	—	Measure.addHaarMeasure Pi.addGroup Real Real.instAddGroup Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Pi.topologicalAddGroup instIsTopologicalAddGroupReal MeasurableSpace.pi Real.measurableSpace Pi.borelSpace Finite.to_countable Finite.of_fintype instSecondCountableTopologyReal Real.borelSpace TopologicalSpace.PositiveCompacts.piIcc01 MeasureSpace.volume MeasureSpace.pi Real.measureSpace	—	Pi.topologicalAddGroup instIsTopologicalAddGroupReal Pi.borelSpace Finite.to_countable Finite.of_fintype instSecondCountableTopologyReal Real.borelSpace IsScalarTower.right volume_pi_pi Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace TopologicalSpace.SecondCountableTopology.to_separableSpace instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal Finset.prod_congr Real.volume_Icc sub_zero ENNReal.ofReal_one Finset.prod_const_one one_smul Measure.addHaarMeasure_unique TopologicalSpace.instSecondCountableTopologyForallOfCountable Measure.instSigmaFiniteForallVolume Pi.isAddLeftInvariant_volume ContinuousAdd.measurableAdd instSeparatelyContinuousAddOfContinuousAdd IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal Measure.IsAddHaarMeasure.toIsAddLeftInvariant
isAddHaarMeasure_volume_pi 📖	mathematical	—	Measure.IsAddHaarMeasure Pi.addGroup Real Real.instAddGroup Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace MeasureSpace.toMeasurableSpace MeasureSpace.pi Real.measureSpace MeasureSpace.volume	—	Measure.instIsAddHaarMeasureForallVolumeOfMeasurableAddOfSigmaFinite ContinuousAdd.measurableAdd Real.borelSpace instSeparatelyContinuousAddOfContinuousAdd IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal

MeasureTheory.Measure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addHaar_affineSubspace 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike SetLike.coe AffineSubspace Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toNormedAddTorsor AffineSubspace.instSetLike instZeroENNReal	—	AffineSubspace.eq_bot_or_nonempty AffineSubspace.bot_coe MeasureTheory.measure_empty instOuterMeasureClass AffineSubspace.coe_direction_eq_vsub_set_right Set.image_congr sub_eq_add_neg Set.image_add_right neg_neg MeasureTheory.measure_preimage_add_right ContinuousAdd.measurableAdd instSeparatelyContinuousAddOfContinuousAdd IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.IsAddLeftInvariant.isAddRightInvariant IsAddHaarMeasure.toIsAddLeftInvariant addHaar_submodule AffineSubspace.direction_eq_top_iff_of_nonempty
addHaar_ball 📖	mathematical	Real Real.instLE Real.instZero	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofReal Real Monoid.toPow Real.instMonoid Module.finrank Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instOne	—	addHaar_ball_mul mul_one
addHaar_ball_center 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	preimage_add_ball sub_self MeasureTheory.measure_preimage_add ContinuousAdd.measurableAdd instSeparatelyContinuousAddOfContinuousAdd IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsAddHaarMeasure.toIsAddLeftInvariant
addHaar_ball_mul 📖	mathematical	Real Real.instLE Real.instZero	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real Real.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofReal Monoid.toPow Real.instMonoid Module.finrank Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	LE.le.eq_or_lt MulZeroClass.zero_mul Metric.ball_zero MeasureTheory.measure_empty instOuterMeasureClass zero_pow LT.lt.ne' Module.finrank_pos commRing_strongRankCondition Real.instNontrivial Real.instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors ENNReal.ofReal_zero addHaar_ball_mul_of_pos
addHaar_ball_mul_of_pos 📖	mathematical	Real Real.instLT Real.instZero	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real Real.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofReal Monoid.toPow Real.instMonoid Module.finrank Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	smul_ball LT.lt.ne' smul_zero abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid LT.lt.le addHaar_ball_center addHaar_smul abs_pow Real.instIsOrderedRing
addHaar_ball_of_pos 📖	mathematical	Real Real.instLT Real.instZero	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofReal Real Monoid.toPow Real.instMonoid Module.finrank Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instOne	—	addHaar_ball_mul_of_pos mul_one
addHaar_closedBall 📖	mathematical	Real Real.instLE Real.instZero	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofReal Real Monoid.toPow Real.instMonoid Module.finrank Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField Metric.ball NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instOne	—	addHaar_closedBall' addHaar_unitClosedBall_eq_addHaar_unitBall
addHaar_closedBall' 📖	mathematical	Real Real.instLE Real.instZero	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofReal Real Monoid.toPow Real.instMonoid Module.finrank Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instOne	—	addHaar_closedBall_mul zero_le_one Real.instZeroLEOneClass mul_one
addHaar_closedBall_center 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	preimage_add_closedBall sub_self MeasureTheory.measure_preimage_add ContinuousAdd.measurableAdd instSeparatelyContinuousAddOfContinuousAdd IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsAddHaarMeasure.toIsAddLeftInvariant
addHaar_closedBall_eq_addHaar_ball 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Metric.ball	—	Metric.closedBall_eq_empty Metric.ball_eq_empty LT.lt.le addHaar_closedBall addHaar_ball
addHaar_closedBall_mul 📖	mathematical	Real Real.instLE Real.instZero	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real Real.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofReal Monoid.toPow Real.instMonoid Module.finrank Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	smul_closedBall smul_zero abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid addHaar_closedBall_center addHaar_smul abs_pow Real.instIsOrderedRing
addHaar_closedBall_mul_of_pos 📖	mathematical	Real Real.instLT Real.instZero	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real Real.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofReal Monoid.toPow Real.instMonoid Module.finrank Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	smul_closedBall' LT.lt.ne' smul_zero abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid LT.lt.le addHaar_closedBall_center addHaar_smul abs_pow Real.instIsOrderedRing
addHaar_eq_zero_of_disjoint_translates 📖	mathematical	Bornology.IsBounded PseudoMetricSpace.toBornology SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.range Pairwise Function.onFun Set Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Set.instSingletonSet MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike instZeroENNReal	—	addHaar_eq_zero_of_disjoint_translates_aux Bornology.IsBounded.subset Metric.isBounded_closedBall Set.inter_subset_right pairwise_disjoint_mono Set.add_subset_add Set.Subset.rfl Set.inter_subset_left MeasurableSet.inter measurableSet_closedBall BorelSpace.opensMeasurable le_antisymm Metric.iUnion_inter_closedBall_nat MeasureTheory.measure_iUnion_le instOuterMeasureClass instCountableNat tsum_zero zero_le ENNReal.instCanonicallyOrderedAdd
addHaar_eq_zero_of_disjoint_translates_aux 📖	mathematical	Bornology.IsBounded PseudoMetricSpace.toBornology SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.range Pairwise Function.onFun Set Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Set.instSingletonSet MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike instZeroENNReal	—	lt_irrefl ENNReal.tsum_const_eq_top_of_ne_zero instInfiniteNat Set.singleton_add Set.image_add_left MeasureTheory.measure_preimage_add ContinuousAdd.measurableAdd instSeparatelyContinuousAddOfContinuousAdd IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsAddHaarMeasure.toIsAddLeftInvariant MeasureTheory.measure_iUnion instCountableNat Measurable.const_add measurable_id Set.iUnion_add Set.iUnion_singleton_eq_range Bornology.IsBounded.measure_lt_top FiniteDimensional.proper_real IsAddHaarMeasure.toIsFiniteMeasureOnCompacts Bornology.IsBounded.add
addHaar_image_continuousLinearEquiv 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Set.image ContinuousLinearEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField EquivLike.toFunLike ContinuousLinearEquiv.equivLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofReal abs Real.lattice Real.instAddGroup MonoidHom LinearMap CommRing.toCommSemiring Real.commRing AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det ContinuousLinearMap.toLinearMap ContinuousLinearEquiv.toContinuousLinearMap	—	RingHomInvPair.ids addHaar_image_linearMap
addHaar_image_continuousLinearMap 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Set.image ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofReal abs Real.lattice Real.instAddGroup MonoidHom LinearMap CommRing.toCommSemiring Real.commRing AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det ContinuousLinearMap.toLinearMap	—	addHaar_image_linearMap
addHaar_image_homothety 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Set.image AffineMap Real CommRing.toRing Real.commRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toNormedAddTorsor AffineMap.instFunLike AffineMap.homothety Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofReal abs Real.lattice Real.instAddGroup Monoid.toPow Real.instMonoid Module.finrank Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	Set.image_congr Set.image_image Set.image_add_right MeasureTheory.measure_preimage_add_right ContinuousAdd.measurableAdd instSeparatelyContinuousAddOfContinuousAdd IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.IsAddLeftInvariant.isAddRightInvariant IsAddHaarMeasure.toIsAddLeftInvariant addHaar_smul
addHaar_image_linearMap 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Set.image LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField LinearMap.instFunLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofReal abs Real.lattice Real.instAddGroup MonoidHom CommRing.toCommSemiring Real.commRing AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det	—	ne_or_eq RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Real.instCompleteSpace TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace ContinuousLinearEquiv.image_eq_preimage_symm addHaar_preimage_continuousLinearEquiv abs_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid ENNReal.ofReal_zero MulZeroClass.zero_mul RingHomSurjective.ids addHaar_submodule LT.lt.ne LinearMap.range_lt_top_of_det_eq_zero le_antisymm le_trans MeasureTheory.measure_mono instOuterMeasureClass Set.image_subset_range Eq.le zero_le ENNReal.instCanonicallyOrderedAdd
addHaar_nnreal_smul 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike NNReal 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 NNReal.instSemiring NNReal.instDistribMulActionOfReal Module.toDistribMulAction Real Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Monoid.toPow ENNReal.ofNNReal Module.finrank	—	addHaar_smul abs_pow Real.instIsOrderedRing NNReal.abs_eq ENNReal.ofReal_pow ENNReal.ofReal_coe_nnreal
addHaar_parallelepiped 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Module.Basis.addHaar parallelepiped NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup ENNReal.ofReal abs Real.lattice Real.instAddGroup AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule AlternatingMap.instFunLike Module.Basis.det	—	Module.Basis.finiteDimensional_of_finite Finite.of_fintype RingHomInvPair.ids AddMonoid.nat_smulCommClass' image_parallelepiped Module.Basis.constr_basis addHaar_image_linearMap isAddHaarMeasure_basis_addHaar Module.Basis.addHaar_self mul_one smulCommClass_self LinearMap.det_toMatrix Module.Basis.toMatrix_eq_toMatrix_constr Module.Basis.det_apply
addHaar_preimage_continuousLinearEquiv 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Set.preimage ContinuousLinearEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField EquivLike.toFunLike ContinuousLinearEquiv.equivLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofReal abs Real.lattice Real.instAddGroup MonoidHom LinearMap CommRing.toCommSemiring Real.commRing AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det ContinuousLinearMap.toLinearMap ContinuousLinearEquiv.toContinuousLinearMap ContinuousLinearEquiv.symm	—	RingHomInvPair.ids addHaar_preimage_linearEquiv
addHaar_preimage_continuousLinearMap 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Set.preimage ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofReal abs Real.lattice Real.instAddGroup Real.instInv MonoidHom LinearMap CommRing.toCommSemiring Real.commRing AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det ContinuousLinearMap.toLinearMap	—	addHaar_preimage_linearMap
addHaar_preimage_linearEquiv 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Set.preimage LinearEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofReal abs Real.lattice Real.instAddGroup MonoidHom LinearMap CommRing.toCommSemiring Real.commRing AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det LinearEquiv.toLinearMap LinearEquiv.symm	—	RingHomInvPair.ids IsUnit.ne_zero Real.instNontrivial LinearEquiv.isUnit_det' LinearEquiv.det_coe_symm addHaar_preimage_linearMap
addHaar_preimage_linearMap 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Set.preimage LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField LinearMap.instFunLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofReal abs Real.lattice Real.instAddGroup Real.instInv MonoidHom CommRing.toCommSemiring Real.commRing AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det	—	RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Real.instCompleteSpace TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MeasurableEquiv.map_apply IsScalarTower.right map_linearMap_addHaar_eq_smul_addHaar
addHaar_preimage_smul 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Set.preimage Real 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 Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofReal abs Real.lattice Real.instAddGroup Real.instInv Monoid.toPow Module.finrank	—	Units.continuousConstSMul UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul isUnit_iff_ne_zero MeasurableEquiv.map_apply IsScalarTower.right map_addHaar_smul coe_smul Pi.smul_apply smul_eq_mul
addHaar_real_ball_center 📖	mathematical	—	real Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	addHaar_ball_center
addHaar_real_closedBall 📖	mathematical	Real Real.instLE Real.instZero	real Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real Real.instMul Monoid.toPow Real.instMonoid Module.finrank Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField Metric.ball NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instOne	—	addHaar_real_closedBall' addHaar_unitClosedBall_eq_addHaar_unitBall
addHaar_real_closedBall' 📖	mathematical	Real Real.instLE Real.instZero	real Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real Real.instMul Monoid.toPow Real.instMonoid Module.finrank Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instOne	—	addHaar_closedBall' ENNReal.toReal_mul IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero Real.instIsDomain pow_nonneg IsOrderedRing.toZeroLEOneClass Real.instIsOrderedRing IsOrderedRing.toPosMulMono
addHaar_real_closedBall_center 📖	mathematical	—	real Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	addHaar_closedBall_center
addHaar_real_closedBall_eq_addHaar_real_ball 📖	mathematical	—	real Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Metric.ball	—	addHaar_closedBall_eq_addHaar_ball
addHaar_singleton_add_smul_div_singleton_add_smul 📖	mathematical	—	ENNReal DivInvMonoid.toDiv ENNReal.instDivInvMonoid DFunLike.coe MeasureTheory.Measure Set instFunLike Set.add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Set.instSingletonSet Real Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toModule Real.normedField	—	Set.singleton_add Set.image_add_left MeasureTheory.measure_preimage_add ContinuousAdd.measurableAdd instSeparatelyContinuousAddOfContinuousAdd IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsAddHaarMeasure.toIsAddLeftInvariant addHaar_smul abs_pow Real.instIsOrderedRing div_eq_mul_inv ENNReal.mul_inv pow_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instZeroLEOneClass abs_pos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul ENNReal.mul_inv_cancel one_mul
addHaar_smul 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Real 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 Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofReal abs Real.lattice Real.instAddGroup Monoid.toPow Module.finrank	—	ne_or_eq Set.preimage_smul_inv₀ addHaar_preimage_smul inv_ne_zero inv_pow inv_inv Set.eq_empty_or_nonempty Set.smul_set_empty MeasureTheory.measure_empty instOuterMeasureClass MulZeroClass.mul_zero Set.zero_smul_set Set.singleton_zero Subsingleton.eq_univ_of_nonempty Module.finrank_zero_iff commRing_strongRankCondition Real.instNontrivial Real.instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors Set.singleton_nonempty pow_zero abs_one Real.instIsOrderedRing ENNReal.ofReal_one one_mul MeasureTheory.NoAtoms.measure_singleton IsAddHaarMeasure.noAtoms SeminormedAddCommGroup.toIsTopologicalAddGroup T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper FiniteDimensional.proper_real Real.punctured_nhds_module_neBot IsTopologicalAddGroup.toContinuousAdd Module.nontrivial_of_finrank_pos bot_lt_iff_ne_bot IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul zero_pow abs_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid ENNReal.ofReal_zero MulZeroClass.zero_mul
addHaar_smul_of_nonneg 📖	mathematical	Real Real.instLE Real.instZero	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Real 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 Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofReal Monoid.toPow Module.finrank	—	addHaar_smul abs_pow Real.instIsOrderedRing abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
addHaar_sphere 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Metric.sphere SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instZeroENNReal	—	eq_or_ne Metric.sphere_zero MeasureTheory.NoAtoms.measure_singleton IsAddHaarMeasure.noAtoms SeminormedAddCommGroup.toIsTopologicalAddGroup T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper FiniteDimensional.proper_real Real.punctured_nhds_module_neBot IsTopologicalAddGroup.toContinuousAdd IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul addHaar_sphere_of_ne_zero
addHaar_sphere_of_ne_zero 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Metric.sphere SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instZeroENNReal	—	Ne.lt_or_gt Metric.closedBall_eq_empty Set.empty_diff MeasureTheory.measure_empty instOuterMeasureClass Metric.closedBall_diff_ball MeasureTheory.measure_diff Metric.ball_subset_closedBall MeasurableSet.nullMeasurableSet measurableSet_ball BorelSpace.opensMeasurable LT.lt.ne MeasureTheory.measure_ball_lt_top FiniteDimensional.proper_real IsAddHaarMeasure.toIsFiniteMeasureOnCompacts addHaar_ball_of_pos addHaar_closedBall LT.lt.le tsub_self ENNReal.instCanonicallyOrderedAdd ENNReal.instOrderedSub
addHaar_submodule 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike SetLike.coe Submodule Real Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField Submodule.setLike instZeroENNReal	—	Nat.instAtLeastTwoHAddOfNat one_div PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNNRat_lt_true instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.instAtLeastTwo Filter.Tendsto.smul_const IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul tendsto_pow_atTop_nhds_zero_of_lt_one AddGroup.existsAddOfLE Real.instArchimedean instOrderTopologyReal LT.lt.le Metric.isBounded_range_of_tendsto addHaar_eq_zero_of_disjoint_translates Set.singleton_add Set.image_add_left sub_smul add_sub_add_right_eq_sub neg_sub_neg Submodule.sub_mem StrictAnti.injective pow_right_strictAnti₀ smul_smul inv_mul_cancel₀ one_smul Submodule.smul_mem IsClosed.measurableSet BorelSpace.opensMeasurable Submodule.closed_of_finiteDimensional Real.instCompleteSpace SeminormedAddCommGroup.toIsTopologicalAddGroup TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace FiniteDimensional.finiteDimensional_submodule
addHaar_unitClosedBall_eq_addHaar_unitBall 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real Real.instOne Metric.ball	—	le_antisymm ENNReal.Tendsto.mul ENNReal.tendsto_ofReal Filter.Tendsto.pow IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Filter.tendsto_id' nhdsWithin_le_nhds one_pow ENNReal.ofReal_one NeZero.charZero_one ENNReal.instCharZero tendsto_const_nhds le_of_tendsto instClosedIicTopology OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology nhdsLT_neBot instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial one_mul Filter.mp_mem Ioo_mem_nhdsLT HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid zero_lt_one Real.instZeroLEOneClass RCLike.charZero_rclike Filter.univ_mem' addHaar_closedBall' LT.lt.le MeasureTheory.measure_mono instOuterMeasureClass Metric.closedBall_subset_ball Metric.ball_subset_closedBall
eventually_nonempty_inter_smul_of_density_one 📖	mathematical	Filter.Tendsto Real ENNReal DivInvMonoid.toDiv ENNReal.instDivInvMonoid DFunLike.coe MeasureTheory.Measure Set instFunLike Set.instInter Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero Set.Ioi Real.instPreorder nhds ENNReal.instTopologicalSpace AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal MeasurableSet	Filter.Eventually Real Set.Nonempty Set Set.instInter Set.add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Set.instSingletonSet Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toModule Real.normedField nhdsWithin Real.pseudoMetricSpace Real.instZero Set.Ioi Real.instPreorder	—	exists_subset_measure_lt_top IsAddHaarMeasure.sigmaFinite SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace SeminormedAddCommGroup.toIsTopologicalAddGroup TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper FiniteDimensional.proper_real instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper Ne.bot_lt Filter.mp_mem tendsto_order ENNReal.instOrderTopology tendsto_addHaar_inter_smul_one_of_density_one LT.lt.ne' LT.lt.ne zero_lt_one IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing NeZero.charZero_one ENNReal.instCharZero Filter.univ_mem' ENNReal.zero_div MeasureTheory.nonempty_of_measure_ne_zero Set.Nonempty.mono Set.inter_subset_inter Set.Subset.rfl Set.add_subset_add Set.smul_set_mono
instIsAddLeftInvariantMeasure 📖	mathematical	—	IsAddLeftInvariant AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AlternatingMap.measure	—	commRing_strongRankCondition Real.instNontrivial AlternatingMap.measure_def MeasureTheory.isAddLeftInvariant_smul_nnreal IsAddHaarMeasure.toIsAddLeftInvariant isAddHaarMeasure_basis_addHaar
instIsLocallyFiniteMeasureMeasure 📖	mathematical	—	MeasureTheory.IsLocallyFiniteMeasure UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AlternatingMap.measure	—	commRing_strongRankCondition Real.instNontrivial AlternatingMap.measure_def MeasureTheory.isLocallyFiniteMeasureSMulNNReal MeasureTheory.isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper FiniteDimensional.proper_real IsAddHaarMeasure.toIsFiniteMeasureOnCompacts isAddHaarMeasure_basis_addHaar
isUnifLocDoublingMeasureOfIsAddHaarMeasure 📖	mathematical	—	IsUnifLocDoublingMeasure SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	Nat.instAtLeastTwoHAddOfNat Filter.mp_mem self_mem_nhdsWithin Filter.univ_mem' addHaar_closedBall_mul zero_le_two Real.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid le_of_lt addHaar_closedBall_center ENNReal.ofReal.eq_1 Real.toNNReal_pow Real.toNNReal_ofNat
map_addHaar_smul 📖	mathematical	—	map Real 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 Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField ENNReal MeasureTheory.Measure instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right ENNReal.ofReal abs Real.lattice Real.instAddGroup Real.instInv Monoid.toPow Module.finrank	—	smulCommClass_self IsScalarTower.right LinearMap.det_smul Module.Free.of_divisionRing map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass mul_one pow_ne_zero isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass map_linearMap_addHaar_eq_smul_addHaar
map_linearMap_addHaar_eq_smul_addHaar 📖	mathematical	—	map DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField LinearMap.instFunLike ENNReal MeasureTheory.Measure instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right ENNReal.ofReal abs Real.lattice Real.instAddGroup Real.instInv MonoidHom CommRing.toCommSemiring Real.commRing AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det	—	Module.finrank_fintype_fun_eq_card commRing_strongRankCondition Real.instNontrivial Fintype.card_fin RingHomInvPair.ids Module.Free.of_divisionRing Module.Free.function Finite.of_fintype Module.Free.self FiniteDimensional.finiteDimensional_pi' FiniteDimensional.rclike_to_real RingHomCompTriple.ids IsScalarTower.right LinearMap.det_conj LinearMap.ext LinearMap.comp.congr_simp LinearEquiv.symm_apply_apply LinearMap.continuous_of_finiteDimensional SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Pi.topologicalAddGroup instIsTopologicalAddGroupReal instContinuousSMulForall IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Real.instCompleteSpace TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Pi.t2Space map_map Continuous.measurable Pi.opensMeasurableSpace instCountableFin instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace Pi.borelSpace Continuous.comp map_linearMap_addHaar_pi_eq_smul_addHaar AddEquiv.isAddHaarMeasure_map IsTopologicalAddGroup.toContinuousAdd SemilinearEquivClass.toAddEquivClass LinearEquiv.instSemilinearEquivClass map_smul map_id
map_linearMap_addHaar_pi_eq_smul_addHaar 📖	mathematical	—	map MeasurableSpace.pi Real Real.measurableSpace DFunLike.coe LinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid Real.instAddCommMonoid Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal LinearMap.instFunLike ENNReal MeasureTheory.Measure instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right ENNReal.ofReal abs Real.lattice Real.instAddGroup Real.instInv MonoidHom CommRing.toCommSemiring Real.commRing AddCommGroup.toAddCommMonoid Pi.addCommGroup Real.instAddCommGroup MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det	—	nonempty_fintype IsScalarTower.right Pi.topologicalAddGroup instIsTopologicalAddGroupReal Pi.borelSpace Finite.to_countable instSecondCountableTopologyReal Real.borelSpace addHaarMeasure_unique TopologicalSpace.instSecondCountableTopologyForallOfCountable IsAddHaarMeasure.sigmaFinite instSigmaCompactSpaceForallOfFinite SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace TopologicalSpace.SecondCountableTopology.to_separableSpace instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal IsAddHaarMeasure.toIsAddLeftInvariant Finite.of_fintype MeasureTheory.addHaarMeasure_eq_volume_pi map_smul Real.map_linearMap_volume_pi_eq_smul_volume_pi SMulCommClass.smul_comm instSMulCommClass Algebra.to_smulCommClass
quasiMeasurePreserving_smul 📖	mathematical	—	QuasiMeasurePreserving Real 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 Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField	—	MeasurableConstSMul.measurable_const_smul MeasurableSMul.toMeasurableConstSMul ContinuousSMul.toMeasurableSMul BorelSpace.opensMeasurable Real.borelSpace IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul IsScalarTower.right map_addHaar_smul smul_absolutelyContinuous
tendsto_addHaar_inter_smul_one_of_density_one 📖	mathematical	Filter.Tendsto Real ENNReal DivInvMonoid.toDiv ENNReal.instDivInvMonoid DFunLike.coe MeasureTheory.Measure Set instFunLike Set.instInter Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero Set.Ioi Real.instPreorder nhds ENNReal.instTopologicalSpace AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal MeasurableSet	Filter.Tendsto Real ENNReal DivInvMonoid.toDiv ENNReal.instDivInvMonoid DFunLike.coe MeasureTheory.Measure Set instFunLike Set.instInter Set.add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Set.instSingletonSet Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toModule Real.normedField nhdsWithin Real.pseudoMetricSpace Real.instZero Set.Ioi Real.instPreorder nhds ENNReal.instTopologicalSpace AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	tendsto_addHaar_inter_smul_one_of_density_one_aux MeasureTheory.measurableSet_toMeasurable tendsto_of_tendsto_of_tendsto_of_le_of_le' ENNReal.instOrderTopology tendsto_const_nhds Filter.Eventually.of_forall ENNReal.div_le_div MeasureTheory.measure_mono instOuterMeasureClass Set.inter_subset_inter MeasureTheory.subset_toMeasurable subset_refl Set.instReflSubset le_refl Filter.mp_mem self_mem_nhdsWithin Filter.univ_mem' ENNReal.div_le_of_le_mul one_mul Set.inter_subset_right Filter.Tendsto.congr measure_toMeasurable_inter_of_sFinite MeasureTheory.instSFiniteOfSigmaFinite IsAddHaarMeasure.sigmaFinite SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace SeminormedAddCommGroup.toIsTopologicalAddGroup TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper FiniteDimensional.proper_real instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper Set.singleton_add Set.image_add_left Continuous.measurable BorelSpace.opensMeasurable continuous_const_add instSeparatelyContinuousAddOfContinuousAdd IsTopologicalAddGroup.toContinuousAdd MeasurableSet.const_smul₀ MeasurableSMul.toMeasurableConstSMul ContinuousSMul.toMeasurableSMul Real.borelSpace IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
tendsto_addHaar_inter_smul_one_of_density_one_aux 📖	mathematical	MeasurableSet Filter.Tendsto Real ENNReal DivInvMonoid.toDiv ENNReal.instDivInvMonoid DFunLike.coe MeasureTheory.Measure Set instFunLike Set.instInter Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero Set.Ioi Real.instPreorder nhds ENNReal.instTopologicalSpace AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	Filter.Tendsto Real ENNReal DivInvMonoid.toDiv ENNReal.instDivInvMonoid DFunLike.coe MeasureTheory.Measure Set instFunLike Set.instInter Set.add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Set.instSingletonSet Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toModule Real.normedField nhdsWithin Real.pseudoMetricSpace Real.instZero Set.Ioi Real.instPreorder nhds ENNReal.instTopologicalSpace AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	div_eq_mul_inv ENNReal.sub_mul Set.inter_comm ENNReal.eq_sub_of_add_eq' MeasureTheory.measure_inter_add_diff Filter.Tendsto.congr' Filter.mp_mem self_mem_nhdsWithin Filter.univ_mem' ENNReal.mul_inv_cancel LT.lt.ne' Metric.measure_closedBall_pos IsAddHaarMeasure.toIsOpenPosMeasure LT.lt.ne MeasureTheory.measure_closedBall_lt_top FiniteDimensional.proper_real IsAddHaarMeasure.toIsFiniteMeasureOnCompacts tendsto_const_nhds ENNReal.Tendsto.sub ENNReal.one_ne_top compl_compl MeasurableSet.compl tsub_self ENNReal.instCanonicallyOrderedAdd ENNReal.instOrderedSub tendsto_addHaar_inter_smul_zero_of_density_zero addHaar_singleton_add_smul_div_singleton_add_smul ENNReal.div_self Set.singleton_add Set.image_add_left MeasureTheory.measure_preimage_add ContinuousAdd.measurableAdd instSeparatelyContinuousAddOfContinuousAdd IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsAddHaarMeasure.toIsAddLeftInvariant addHaar_smul abs_pow Real.instIsOrderedRing abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid LT.lt.le ENNReal.instNoZeroDivisors pow_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instZeroLEOneClass ENNReal.ofReal_pow covariant_swap_add_of_covariant_add isReduced_of_noZeroDivisors tsub_zero
tendsto_addHaar_inter_smul_zero_of_density_zero 📖	mathematical	Filter.Tendsto Real ENNReal DivInvMonoid.toDiv ENNReal.instDivInvMonoid DFunLike.coe MeasureTheory.Measure Set instFunLike Set.instInter Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero Set.Ioi Real.instPreorder nhds ENNReal.instTopologicalSpace instZeroENNReal MeasurableSet	Filter.Tendsto Real ENNReal DivInvMonoid.toDiv ENNReal.instDivInvMonoid DFunLike.coe MeasureTheory.Measure Set instFunLike Set.instInter Set.add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Set.instSingletonSet Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toModule Real.normedField nhdsWithin Real.pseudoMetricSpace Real.instZero Set.Ioi Real.instPreorder nhds ENNReal.instTopologicalSpace instZeroENNReal	—	tendsto_order ENNReal.instOrderTopology ENNReal.not_lt_zero eq_or_ne Filter.univ_mem' le_antisymm MeasureTheory.measure_mono instOuterMeasureClass Set.inter_subset_right Set.singleton_add Set.image_add_left MeasureTheory.measure_preimage_add ContinuousAdd.measurableAdd instSeparatelyContinuousAddOfContinuousAdd IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsAddHaarMeasure.toIsAddLeftInvariant addHaar_smul MulZeroClass.mul_zero zero_le ENNReal.instCanonicallyOrderedAdd ENNReal.zero_div Nat.instAtLeastTwoHAddOfNat LT.lt.ne LE.le.trans_lt Set.diff_subset Ne.lt_top MeasureTheory.tendsto_measure_iInter_atTop instIsCountablyGenerated_atTop OrderTopology.of_linearLocallyFinite instDiscreteTopologyNat TopologicalSpace.SecondCountableTopology.to_separableSpace TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace instCountableNat PseudoEMetricSpace.pseudoMetrizableSpace MeasurableSet.nullMeasurableSet MeasurableSet.diff measurableSet_closedBall BorelSpace.opensMeasurable Set.diff_subset_diff Set.Subset.rfl Metric.closedBall_subset_closedBall Nat.cast_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike Set.iInter_eq_compl_iUnion_compl compl_compl Metric.iUnion_closedBall_nat Set.compl_univ Set.inter_empty ENNReal.mul_pos LT.lt.ne' ENNReal.half_pos Filter.Eventually.exists Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.Eventually.and Filter.Ioi_mem_atTop instNoTopOrderOfNoMaxOrder Nat.instNoMaxOrder MeasureTheory.measure_empty tendsto_addHaar_inter_smul_zero_of_density_zero_aux2 Nat.cast_pos Real.instIsOrderedRing Real.instNontrivial Filter.mp_mem self_mem_nhdsWithin Set.inter_union_distrib_left Set.add_union Set.smul_set_union Set.inter_union_diff MeasureTheory.measure_union_le add_le_add_right ENNReal.instIsOrderedAddMonoid ENNReal.div_le_div le_refl ENNReal.add_div ENNReal.add_lt_add addHaar_singleton_add_smul_div_singleton_add_smul ENNReal.div_lt_iff ENNReal.add_halves
tendsto_addHaar_inter_smul_zero_of_density_zero_aux1 📖	mathematical	Filter.Tendsto Real ENNReal DivInvMonoid.toDiv ENNReal.instDivInvMonoid DFunLike.coe MeasureTheory.Measure Set instFunLike Set.instInter Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero Set.Ioi Real.instPreorder nhds ENNReal.instTopologicalSpace instZeroENNReal Set.instHasSubset NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instOne	Filter.Tendsto Real ENNReal DivInvMonoid.toDiv ENNReal.instDivInvMonoid DFunLike.coe MeasureTheory.Measure Set instFunLike Set.instInter Set.add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Set.instSingletonSet Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toModule Real.normedField nhdsWithin Real.pseudoMetricSpace Real.instZero Set.Ioi Real.instPreorder nhds ENNReal.instTopologicalSpace instZeroENNReal	—	tendsto_of_tendsto_of_tendsto_of_le_of_le' ENNReal.instOrderTopology tendsto_const_nhds Filter.Eventually.of_forall zero_le ENNReal.instCanonicallyOrderedAdd Filter.mp_mem self_mem_nhdsWithin Filter.univ_mem' le_imp_le_of_le_of_le ENNReal.div_le_div MeasureTheory.measure_mono instOuterMeasureClass Set.inter_subset_inter subset_refl Set.instReflSubset Set.add_subset_add Set.smul_set_mono le_refl vadd_eq_add Set.singleton_vadd affinity_unitClosedBall LT.lt.le Filter.Tendsto.congr' smul_closedBall Real.instZeroLEOneClass smul_zero Real.norm_of_nonneg mul_one singleton_add_closedBall add_zero addHaar_singleton_add_smul_div_singleton_add_smul LT.lt.ne' addHaar_closedBall_center Set.singleton_add Set.image_add_left MeasureTheory.measure_preimage_add ContinuousAdd.measurableAdd instSeparatelyContinuousAddOfContinuousAdd IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsAddHaarMeasure.toIsAddLeftInvariant ENNReal.Tendsto.mul LT.lt.ne MeasureTheory.measure_closedBall_lt_top FiniteDimensional.proper_real IsAddHaarMeasure.toIsFiniteMeasureOnCompacts ENNReal.zero_ne_top div_eq_mul_inv Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul ENNReal.mul_inv_cancel Metric.measure_closedBall_pos IsAddHaarMeasure.toIsOpenPosMeasure one_mul MulZeroClass.zero_mul
tendsto_addHaar_inter_smul_zero_of_density_zero_aux2 📖	mathematical	Filter.Tendsto Real ENNReal DivInvMonoid.toDiv ENNReal.instDivInvMonoid DFunLike.coe MeasureTheory.Measure Set instFunLike Set.instInter Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero Set.Ioi Real.instPreorder nhds ENNReal.instTopologicalSpace instZeroENNReal Real.instLT Set.instHasSubset NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	Filter.Tendsto Real ENNReal DivInvMonoid.toDiv ENNReal.instDivInvMonoid DFunLike.coe MeasureTheory.Measure Set instFunLike Set.instInter Set.add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Set.instSingletonSet Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toModule Real.normedField nhdsWithin Real.pseudoMetricSpace Real.instZero Set.Ioi Real.instPreorder nhds ENNReal.instTopologicalSpace instZeroENNReal	—	tendsto_addHaar_inter_smul_zero_of_density_zero_aux1 addHaar_smul inv_pow ENNReal.instNoZeroDivisors IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add LT.lt.ne' pow_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instZeroLEOneClass LE.le.trans_eq Set.smul_set_mono smul_closedBall LT.lt.le smul_zero Real.norm_of_nonneg inv_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE inv_mul_cancel₀ tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within Filter.Tendsto.mono_left Filter.Tendsto.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal tendsto_const_nhds Filter.tendsto_id nhdsWithin_le_nhds Filter.mp_mem self_mem_nhdsWithin Filter.univ_mem' MulZeroClass.mul_zero mul_pos Filter.Tendsto.congr' mul_comm smul_smul mul_assoc mul_inv_cancel₀ mul_one Filter.Tendsto.comp

MeasureTheory.Measure.ContinuousLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
quasiMeasurePreserving 📖	mathematical	—	MeasureTheory.Measure.QuasiMeasurePreserving DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike	—	MeasureTheory.Measure.LinearMap.quasiMeasurePreserving

MeasureTheory.Measure.LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
quasiMeasurePreserving 📖	mathematical	—	MeasureTheory.Measure.QuasiMeasurePreserving DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField LinearMap.instFunLike	—	Continuous.measurable BorelSpace.opensMeasurable LinearMap.continuous_of_finiteDimensional SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Real.instCompleteSpace TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace IsScalarTower.right MeasureTheory.Measure.map_linearMap_addHaar_eq_smul_addHaar MeasureTheory.Measure.smul_absolutelyContinuous

MeasureTheory.Measure.NullMeasurableSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
const_smul 📖	mathematical	MeasureTheory.NullMeasurableSet	MeasureTheory.NullMeasurableSet Real Set 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 Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField	—	Set.eq_empty_or_nonempty Set.smul_set_empty eq_or_ne Set.zero_smul_set MeasureTheory.nullMeasurableSet_singleton MeasureTheory.NullMeasurableSet.instMeasurableSingletonClass instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable secondCountable_of_proper FiniteDimensional.proper_real TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MeasureTheory.Measure.instOuterMeasureClass MeasurableSet.const_smul_of_ne_zero MeasurableSMul.toMeasurableConstSMul ContinuousSMul.toMeasurableSMul Real.borelSpace IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul MeasureTheory.measure_symmDiff_eq_zero_iff Set.smul_set_symmDiff₀ MeasureTheory.Measure.addHaar_smul MulZeroClass.mul_zero

Module.Basis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_addHaar 📖	mathematical	—	MeasureTheory.Measure.map DFunLike.coe ContinuousLinearEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField EquivLike.toFunLike ContinuousLinearEquiv.equivLike addHaar map ContinuousLinearEquiv.toLinearEquiv	—	RingHomInvPair.ids addHaar_eq_iff MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite ContinuousLinearEquiv.isAddHaarMeasure_map SeminormedAddCommGroup.toIsTopologicalAddGroup isAddHaarMeasure_basis_addHaar MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant MeasureTheory.Measure.map_apply Continuous.measurable BorelSpace.opensMeasurable ContinuousLinearEquiv.continuous IsCompact.measurableSet TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace TopologicalSpace.PositiveCompacts.isCompact coe_parallelepiped coe_map image_parallelepiped Equiv.preimage_image addHaar_self
parallelepiped_basisFun 📖	mathematical	—	parallelepiped Pi.normedAddCommGroup Real Real.normedAddCommGroup Pi.normedSpace Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Pi.basisFun Real.semiring Finite.of_fintype TopologicalSpace.PositiveCompacts.piIcc01	—	SetLike.coe_injective Finite.of_fintype parallelepiped_single Set.uIcc_of_le zero_le_one Pi.instZeroLEOneClass Real.instZeroLEOneClass Set.pi_univ_Icc
parallelepiped_eq_map 📖	mathematical	—	parallelepiped TopologicalSpace.PositiveCompacts.map Pi.topologicalSpace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearEquiv Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Pi.Function.module Semiring.toModule NormedSpace.toModule Real.normedField EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm equivFun Finite.of_fintype ContinuousLinearEquiv.continuous DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace ContinuousLinearEquiv.symm equivFunL SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NormedSpace.toIsBoundedSMul Real.instCompleteSpace TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace ContinuousLinearEquiv.isOpenMap TopologicalSpace.PositiveCompacts.piIcc01	—	RingHomInvPair.ids Finite.of_fintype ContinuousLinearEquiv.continuous SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Real.instCompleteSpace TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace ContinuousLinearEquiv.isOpenMap parallelepiped_basisFun LinearMap.continuous_of_finiteDimensional finiteDimensional_of_finite LinearMap.isOpenMap_of_finiteDimensional LinearEquiv.surjective parallelepiped_map eq_of_apply_eq Pi.basisFun_apply equivFun_symm_apply Finset.sum_congr Pi.single_apply ite_smul one_smul zero_smul Finset.sum_ite_eq'

TopologicalSpace.PositiveCompacts

Definitions

Name	Category	Theorems
Icc01 📖	CompOp	1 math math: MeasureTheory.addHaarMeasure_eq_volume
piIcc01 📖	CompOp	3 math math: Module.Basis.parallelepiped_basisFun, MeasureTheory.addHaarMeasure_eq_volume_pi, Module.Basis.parallelepiped_eq_map

---

← Back to Index