MulEquivHaarChar

📁 Source: Mathlib/MeasureTheory/Measure/Haar/MulEquivHaarChar.lean

Statistics

Metric	Count
Definitions addEquivAddHaarChar, mulEquivHaarChar	2
Theorems addEquivAddHaarChar_eq, addEquivAddHaarChar_pos, addEquivAddHaarChar_refl, addEquivAddHaarChar_smul_eq_comap, addEquivAddHaarChar_smul_integral_map, addEquivAddHaarChar_smul_map, addEquivAddHaarChar_smul_preimage, addEquivAddHaarChar_symm, addEquivAddHaarChar_trans, integral_comap_eq_addEquivAddHaarChar_smul, integral_comap_eq_mulEquivHaarChar_smul, mulEquivHaarChar_eq, mulEquivHaarChar_pos, mulEquivHaarChar_refl, mulEquivHaarChar_smul_eq_comap, mulEquivHaarChar_smul_integral_map, mulEquivHaarChar_smul_map, mulEquivHaarChar_smul_preimage, mulEquivHaarChar_symm, mulEquivHaarChar_trans	20
Total	22

MeasureTheory

Definitions

Name	Category	Theorems
addEquivAddHaarChar 📖	CompOp	10 math math: addEquivAddHaarChar_pos, addEquivAddHaarChar_smul_preimage, addEquivAddHaarChar_eq, integral_comap_eq_addEquivAddHaarChar_smul, addEquivAddHaarChar_smul_map, addEquivAddHaarChar_smul_eq_comap, addEquivAddHaarChar_refl, addEquivAddHaarChar_symm, addEquivAddHaarChar_trans, addEquivAddHaarChar_smul_integral_map
mulEquivHaarChar 📖	CompOp	10 math math: mulEquivHaarChar_smul_integral_map, mulEquivHaarChar_symm, mulEquivHaarChar_eq, mulEquivHaarChar_pos, mulEquivHaarChar_smul_map, mulEquivHaarChar_refl, mulEquivHaarChar_trans, mulEquivHaarChar_smul_preimage, mulEquivHaarChar_smul_eq_comap, integral_comap_eq_mulEquivHaarChar_smul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addEquivAddHaarChar_eq 📖	mathematical	—	addEquivAddHaarChar Measure.addHaarScalarFactor Measure.map DFunLike.coe ContinuousAddEquiv AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid EquivLike.toFunLike ContinuousAddEquiv.instEquivLike ContinuousAddEquiv.isAddHaarMeasure_map Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts Measure.IsAddHaarMeasure.toIsAddLeftInvariant	—	IsScalarTower.right Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts Measure.isAddHaarMeasure_addHaarMeasure Measure.isAddLeftInvariant_addHaarMeasure Measure.isAddLeftInvariant_eq_smul_of_regular Measure.regular_addHaarMeasure ContinuousAddEquiv.isAddHaarMeasure_map Measure.IsAddHaarMeasure.toIsAddLeftInvariant Measure.map_smul Measure.addHaarScalarFactor.congr_simp Measure.addHaarScalarFactor_smul_smul LT.lt.ne' Measure.addHaarScalarFactor_pos_of_isAddHaarMeasure
addEquivAddHaarChar_pos 📖	mathematical	—	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instZeroNNReal addEquivAddHaarChar	—	Measure.addHaarScalarFactor_pos_of_isAddHaarMeasure Measure.isAddHaarMeasure_addHaarMeasure
addEquivAddHaarChar_refl 📖	mathematical	—	addEquivAddHaarChar ContinuousAddEquiv.refl AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NNReal instOneNNReal	—	Measure.map_id' Measure.addHaarScalarFactor.congr_simp Measure.addHaarScalarFactor_self
addEquivAddHaarChar_smul_eq_comap 📖	mathematical	—	NNReal Measure Measure.instSMul Algebra.toSMul ENNReal instCommSemiringNNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id IsScalarTower.right addEquivAddHaarChar Measure.comap DFunLike.coe ContinuousAddEquiv AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid EquivLike.toFunLike ContinuousAddEquiv.instEquivLike	—	IsScalarTower.right MeasurableEquiv.map_symm Measure.Regular.map addEquivAddHaarChar_smul_map ContinuousAddEquiv.isAddHaarMeasure_map Measure.map_map Continuous.measurable BorelSpace.opensMeasurable ContinuousMapClass.map_continuous HomeomorphClass.instContinuousMapClass ContinuousAddEquiv.instHomeomorphClass ContinuousAddEquiv.self_comp_symm Measure.map_id
addEquivAddHaarChar_smul_integral_map 📖	mathematical	—	NNReal Real Algebra.toSMul instCommSemiringNNReal Real.semiring NNReal.instAlgebraOfReal Algebra.id Real.instCommSemiring addEquivAddHaarChar integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Measure.map DFunLike.coe ContinuousAddEquiv AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid EquivLike.toFunLike ContinuousAddEquiv.instEquivLike	—	IsScalarTower.right addEquivAddHaarChar_smul_map integral_smul_nnreal_measure
addEquivAddHaarChar_smul_map 📖	mathematical	—	NNReal Measure Measure.instSMul Algebra.toSMul ENNReal instCommSemiringNNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id IsScalarTower.right addEquivAddHaarChar Measure.map DFunLike.coe ContinuousAddEquiv AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid EquivLike.toFunLike ContinuousAddEquiv.instEquivLike	—	IsScalarTower.right ContinuousAddEquiv.isAddHaarMeasure_map Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts Measure.IsAddHaarMeasure.toIsAddLeftInvariant addEquivAddHaarChar_eq Measure.Regular.map Measure.isAddLeftInvariant_eq_smul_of_regular
addEquivAddHaarChar_smul_preimage 📖	mathematical	—	NNReal ENNReal Algebra.toSMul instCommSemiringNNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id addEquivAddHaarChar DFunLike.coe Measure Set Measure.instFunLike Set.preimage ContinuousAddEquiv AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid EquivLike.toFunLike ContinuousAddEquiv.instEquivLike	—	IsScalarTower.right addEquivAddHaarChar_smul_map MeasurableEquiv.map_apply
addEquivAddHaarChar_symm 📖	mathematical	—	addEquivAddHaarChar ContinuousAddEquiv.symm AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NNReal NNReal.instInv	—	inv_eq_of_mul_eq_one_right addEquivAddHaarChar_trans addEquivAddHaarChar.congr_simp ContinuousAddEquiv.self_trans_symm addEquivAddHaarChar_refl
addEquivAddHaarChar_trans 📖	mathematical	—	addEquivAddHaarChar ContinuousAddEquiv.trans AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal	—	ContinuousAddEquiv.isAddHaarMeasure_map Measure.isAddHaarMeasure_addHaarMeasure Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts Measure.IsAddHaarMeasure.toIsAddLeftInvariant addEquivAddHaarChar_eq Measure.regular_addHaarMeasure Continuous.measurable BorelSpace.opensMeasurable ContinuousMapClass.map_continuous HomeomorphClass.instContinuousMapClass ContinuousAddEquiv.instHomeomorphClass Measure.map_map Measure.addHaarScalarFactor.congr_simp Measure.Regular.map Measure.addHaarScalarFactor_eq_mul
integral_comap_eq_addEquivAddHaarChar_smul 📖	mathematical	—	integral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Measure.comap DFunLike.coe ContinuousAddEquiv AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid EquivLike.toFunLike ContinuousAddEquiv.instEquivLike NNReal Algebra.toSMul instCommSemiringNNReal Real.semiring NNReal.instAlgebraOfReal Algebra.id Real.instCommSemiring addEquivAddHaarChar	—	ContinuousAddEquiv.isAddHaarMeasure_map Measure.Regular.map MeasurableEquiv.map_symm addEquivAddHaarChar_smul_integral_map Measure.map_map MeasurableEquiv.measurable AddEquivClass.apply_coe_symm_apply ContinuousAddEquiv.instAddEquivClass Measure.map_id
integral_comap_eq_mulEquivHaarChar_smul 📖	mathematical	—	integral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Measure.comap DFunLike.coe ContinuousMulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid EquivLike.toFunLike ContinuousMulEquiv.instEquivLike NNReal Algebra.toSMul instCommSemiringNNReal Real.semiring NNReal.instAlgebraOfReal Algebra.id Real.instCommSemiring mulEquivHaarChar	—	ContinuousMulEquiv.isHaarMeasure_map Measure.Regular.map MeasurableEquiv.map_symm mulEquivHaarChar_smul_integral_map Measure.map_map MeasurableEquiv.measurable MulEquivClass.apply_coe_symm_apply ContinuousMulEquiv.instMulEquivClass Measure.map_id
mulEquivHaarChar_eq 📖	mathematical	—	mulEquivHaarChar Measure.haarScalarFactor Measure.map DFunLike.coe ContinuousMulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid EquivLike.toFunLike ContinuousMulEquiv.instEquivLike ContinuousMulEquiv.isHaarMeasure_map Measure.IsHaarMeasure.toIsFiniteMeasureOnCompacts Measure.IsHaarMeasure.toIsMulLeftInvariant	—	IsScalarTower.right Measure.IsHaarMeasure.toIsFiniteMeasureOnCompacts Measure.isHaarMeasure_haarMeasure Measure.isMulLeftInvariant_haarMeasure Measure.isMulLeftInvariant_eq_smul_of_regular Measure.regular_haarMeasure ContinuousMulEquiv.isHaarMeasure_map Measure.IsHaarMeasure.toIsMulLeftInvariant Measure.map_smul Measure.haarScalarFactor.congr_simp Measure.haarScalarFactor_smul_smul LT.lt.ne' Measure.haarScalarFactor_pos_of_isHaarMeasure
mulEquivHaarChar_pos 📖	mathematical	—	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instZeroNNReal mulEquivHaarChar	—	Measure.haarScalarFactor_pos_of_isHaarMeasure Measure.isHaarMeasure_haarMeasure
mulEquivHaarChar_refl 📖	mathematical	—	mulEquivHaarChar ContinuousMulEquiv.refl MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid NNReal instOneNNReal	—	Measure.map_id' Measure.haarScalarFactor.congr_simp Measure.haarScalarFactor_self
mulEquivHaarChar_smul_eq_comap 📖	mathematical	—	NNReal Measure Measure.instSMul Algebra.toSMul ENNReal instCommSemiringNNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id IsScalarTower.right mulEquivHaarChar Measure.comap DFunLike.coe ContinuousMulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid EquivLike.toFunLike ContinuousMulEquiv.instEquivLike	—	IsScalarTower.right MeasurableEquiv.map_symm Measure.Regular.map mulEquivHaarChar_smul_map ContinuousMulEquiv.isHaarMeasure_map Measure.map_map Continuous.measurable BorelSpace.opensMeasurable ContinuousMapClass.map_continuous HomeomorphClass.instContinuousMapClass ContinuousMulEquiv.instHomeomorphClass ContinuousMulEquiv.self_comp_symm Measure.map_id
mulEquivHaarChar_smul_integral_map 📖	mathematical	—	NNReal Real Algebra.toSMul instCommSemiringNNReal Real.semiring NNReal.instAlgebraOfReal Algebra.id Real.instCommSemiring mulEquivHaarChar integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Measure.map DFunLike.coe ContinuousMulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid EquivLike.toFunLike ContinuousMulEquiv.instEquivLike	—	IsScalarTower.right mulEquivHaarChar_smul_map integral_smul_nnreal_measure
mulEquivHaarChar_smul_map 📖	mathematical	—	NNReal Measure Measure.instSMul Algebra.toSMul ENNReal instCommSemiringNNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id IsScalarTower.right mulEquivHaarChar Measure.map DFunLike.coe ContinuousMulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid EquivLike.toFunLike ContinuousMulEquiv.instEquivLike	—	IsScalarTower.right ContinuousMulEquiv.isHaarMeasure_map Measure.IsHaarMeasure.toIsFiniteMeasureOnCompacts Measure.IsHaarMeasure.toIsMulLeftInvariant mulEquivHaarChar_eq Measure.Regular.map Measure.isMulLeftInvariant_eq_smul_of_regular
mulEquivHaarChar_smul_preimage 📖	mathematical	—	NNReal ENNReal Algebra.toSMul instCommSemiringNNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id mulEquivHaarChar DFunLike.coe Measure Set Measure.instFunLike Set.preimage ContinuousMulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid EquivLike.toFunLike ContinuousMulEquiv.instEquivLike	—	IsScalarTower.right mulEquivHaarChar_smul_map MeasurableEquiv.map_apply
mulEquivHaarChar_symm 📖	mathematical	—	mulEquivHaarChar ContinuousMulEquiv.symm MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid NNReal NNReal.instInv	—	inv_eq_of_mul_eq_one_right mulEquivHaarChar.congr_simp ContinuousMulEquiv.self_trans_symm mulEquivHaarChar_refl
mulEquivHaarChar_trans 📖	mathematical	—	mulEquivHaarChar ContinuousMulEquiv.trans MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid NNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal	—	ContinuousMulEquiv.isHaarMeasure_map Measure.isHaarMeasure_haarMeasure Measure.IsHaarMeasure.toIsFiniteMeasureOnCompacts Measure.IsHaarMeasure.toIsMulLeftInvariant mulEquivHaarChar_eq Measure.regular_haarMeasure Continuous.measurable BorelSpace.opensMeasurable ContinuousMapClass.map_continuous HomeomorphClass.instContinuousMapClass ContinuousMulEquiv.instHomeomorphClass Measure.map_map Measure.haarScalarFactor.congr_simp Measure.Regular.map Measure.haarScalarFactor_eq_mul

---

← Back to Index