Quotient

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

Statistics

Metric	Count
Definitions	0
Theorems AddQuotientMeasureEqMeasurePreimage_AddHaarMeasure, AddQuotientMeasureEqMeasurePreimage_vaddAddHaarMeasure, QuotientMeasureEqMeasurePreimage_HaarMeasure, QuotientMeasureEqMeasurePreimage_smulHaarMeasure, addHaarMeasure_quotient, addInvariantMeasure_quotient, vaddInvariantMeasure_quotient, absolutelyContinuous_map, absolutelyContinuous_map, addQuotientMeasureEqMeasurePreimage_of_set, quotientMeasureEqMeasurePreimage_of_set, haarMeasure_quotient, mulInvariantMeasure_quotient, smulInvariantMeasure_quotient, leftInvariantIsAddQuotientMeasureEqMeasurePreimage, leftInvariantIsQuotientMeasureEqMeasurePreimage, integral_eq_integral_automorphize, integral_mul_eq_integral_automorphize_mul, measurableVAdd, integral_eq_integral_automorphize, integral_mul_eq_integral_automorphize_mul, measurableSMul, essSup_comp_quotientAddGroup_mk, essSup_comp_quotientGroup_mk, measurePreserving_quotientAddGroup_mk_of_AddQuotientMeasureEqMeasurePreimage, measurePreserving_quotientGroup_mk_of_QuotientMeasureEqMeasurePreimage	26
Total	26

IsFundamentalDomain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
AddQuotientMeasureEqMeasurePreimage_AddHaarMeasure 📖	mathematical	MeasureTheory.IsAddFundamentalDomain AddOpposite AddSubgroup AddOpposite.instAddGroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.op AddSubgroup.zero AddSubgroup.instVAdd Set.Nonempty HasQuotient.Quotient QuotientAddGroup.instHasQuotientAddSubgroup interior QuotientAddGroup.instTopologicalSpace MeasurableSet QuotientAddGroup.measurableSpace DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike Set.instInter Set.preimage	MeasureTheory.AddQuotientMeasureEqMeasurePreimage AddSubgroup.toAddGroup AddAction.instAddAction AddMonoid.toOppositeAddAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	MeasureTheory.Measure.IsAddLeftInvariant.addQuotientMeasureEqMeasurePreimage_of_set MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant MeasureTheory.Measure.IsOpenPosMeasure.open_pos MeasureTheory.Measure.IsAddHaarMeasure.toIsOpenPosMeasure isOpen_interior Set.Nonempty.mono preimage_interior_subset_interior_preimage continuous_coinduced_rng Set.Nonempty.preimage' Set.subset_univ MeasureTheory.measure_mono_null MeasureTheory.Measure.instOuterMeasureClass interior_subset MeasureTheory.IsAddFundamentalDomain.measure_zero_of_invariant AddSubgroup.instMeasurableConstVAdd MeasurableVAdd.toMeasurableConstVAdd measurableVAdd_opposite_of_add ContinuousAdd.measurableAdd IsTopologicalAddGroup.toContinuousAdd MeasureTheory.Subgroup.vaddInvariantMeasure MeasureTheory.Measure.IsAddRightInvariant.toVAddInvariantMeasure_op AddSubgroup.instCountableSubtypeAddOppositeMemOp QuotientAddGroup.sound
AddQuotientMeasureEqMeasurePreimage_vaddAddHaarMeasure 📖	mathematical	MeasureTheory.IsAddFundamentalDomain AddOpposite AddSubgroup AddOpposite.instAddGroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.op AddSubgroup.zero AddSubgroup.instVAdd	MeasureTheory.AddQuotientMeasureEqMeasurePreimage AddSubgroup.toAddGroup AddAction.instAddAction AddMonoid.toOppositeAddAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid ENNReal MeasureTheory.Measure HasQuotient.Quotient QuotientAddGroup.instHasQuotientAddSubgroup QuotientAddGroup.measurableSpace MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right DFunLike.coe Set MeasureTheory.Measure.instFunLike Set.instInter Set.preimage SetLike.coe TopologicalSpace.PositiveCompacts QuotientAddGroup.instTopologicalSpace TopologicalSpace.PositiveCompacts.instSetLike MeasureTheory.Measure.addHaarMeasure QuotientAddGroup.Quotient.addGroup QuotientAddGroup.instIsTopologicalAddGroup AddCosetSpace.borelSpace	—	IsScalarTower.right QuotientAddGroup.instIsTopologicalAddGroup AddCosetSpace.borelSpace Mathlib.Tactic.Contrapose.contrapose₄ MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass Set.inter_subset_right top_unique MeasureTheory.Measure.addHaarMeasure_self mul_one AddQuotientMeasureEqMeasurePreimage_AddHaarMeasure MeasureTheory.isAddLeftInvariant_smul MeasureTheory.Measure.isAddLeftInvariant_addHaarMeasure CanLift.prf ENNReal.canLift MeasureTheory.SMul.sigmaFinite MeasureTheory.Measure.sigmaFinite_addHaarMeasure IsCompact.measurableSet BorelSpace.opensMeasurable TopologicalSpace.PositiveCompacts.isCompact TopologicalSpace.PositiveCompacts.interior_nonempty
QuotientMeasureEqMeasurePreimage_HaarMeasure 📖	mathematical	MeasureTheory.IsFundamentalDomain MulOpposite Subgroup MulOpposite.instGroup SetLike.instMembership Subgroup.instSetLike Subgroup.op Subgroup.one Subgroup.instSMul Set.Nonempty HasQuotient.Quotient QuotientGroup.instHasQuotientSubgroup interior QuotientGroup.instTopologicalSpace MeasurableSet QuotientGroup.measurableSpace DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike Set.instInter Set.preimage	MeasureTheory.QuotientMeasureEqMeasurePreimage Subgroup.toGroup MulAction.instMulAction Monoid.toOppositeMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid	—	MeasureTheory.Measure.IsMulLeftInvariant.quotientMeasureEqMeasurePreimage_of_set MeasureTheory.Measure.IsHaarMeasure.toIsMulLeftInvariant MeasureTheory.Measure.IsOpenPosMeasure.open_pos MeasureTheory.Measure.IsHaarMeasure.toIsOpenPosMeasure Set.Nonempty.mono preimage_interior_subset_interior_preimage continuous_coinduced_rng Set.Nonempty.preimage' MeasureTheory.measure_mono_null MeasureTheory.Measure.instOuterMeasureClass interior_subset MeasureTheory.IsFundamentalDomain.measure_zero_of_invariant Subgroup.instMeasurableConstSMul MeasurableSMul.toMeasurableConstSMul measurableSMul_opposite_of_mul ContinuousMul.measurableMul IsTopologicalGroup.toContinuousMul MeasureTheory.Subgroup.smulInvariantMeasure MeasureTheory.Measure.IsMulRightInvariant.toSMulInvariantMeasure_op Subgroup.instCountableSubtypeMulOppositeMemOp QuotientGroup.sound
QuotientMeasureEqMeasurePreimage_smulHaarMeasure 📖	mathematical	MeasureTheory.IsFundamentalDomain MulOpposite Subgroup MulOpposite.instGroup SetLike.instMembership Subgroup.instSetLike Subgroup.op Subgroup.one Subgroup.instSMul	MeasureTheory.QuotientMeasureEqMeasurePreimage Subgroup.toGroup MulAction.instMulAction Monoid.toOppositeMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid ENNReal MeasureTheory.Measure HasQuotient.Quotient QuotientGroup.instHasQuotientSubgroup QuotientGroup.measurableSpace MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right DFunLike.coe Set MeasureTheory.Measure.instFunLike Set.instInter Set.preimage SetLike.coe TopologicalSpace.PositiveCompacts QuotientGroup.instTopologicalSpace TopologicalSpace.PositiveCompacts.instSetLike MeasureTheory.Measure.haarMeasure QuotientGroup.Quotient.group QuotientGroup.instIsTopologicalGroup CosetSpace.borelSpace	—	IsScalarTower.right QuotientGroup.instIsTopologicalGroup CosetSpace.borelSpace Mathlib.Tactic.Contrapose.contrapose₄ MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass Set.inter_subset_right top_unique MeasureTheory.Measure.haarMeasure_self mul_one QuotientMeasureEqMeasurePreimage_HaarMeasure MeasureTheory.isMulLeftInvariant_smul MeasureTheory.Measure.isMulLeftInvariant_haarMeasure CanLift.prf ENNReal.canLift MeasureTheory.SMul.sigmaFinite MeasureTheory.Measure.sigmaFinite_haarMeasure IsCompact.measurableSet BorelSpace.opensMeasurable TopologicalSpace.PositiveCompacts.isCompact TopologicalSpace.PositiveCompacts.interior_nonempty

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
leftInvariantIsAddQuotientMeasureEqMeasurePreimage 📖	mathematical	addCovolume AddOpposite AddSubgroup AddOpposite.instAddGroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.op AddSubgroup.zero AddSubgroup.instVAdd DFunLike.coe Measure HasQuotient.Quotient QuotientAddGroup.instHasQuotientAddSubgroup QuotientAddGroup.measurableSpace Set ENNReal Measure.instFunLike Set.univ	AddQuotientMeasureEqMeasurePreimage AddSubgroup.toAddGroup AddAction.instAddAction AddMonoid.toOppositeAddAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	HasAddFundamentalDomain.ExistsIsAddFundamentalDomain measure_lt_top Measure.measure_univ_eq_zero IsAddFundamentalDomain.covolume_eq_volume AddSubgroup.instCountableSubtypeAddOppositeMemOp AddSubgroup.instMeasurableConstVAdd MeasurableVAdd.toMeasurableConstVAdd measurableVAdd_opposite_of_add ContinuousAdd.measurableAdd IsTopologicalAddGroup.toContinuousAdd Subgroup.vaddInvariantMeasure Measure.IsAddRightInvariant.toVAddInvariantMeasure_op IsAddFundamentalDomain.addQuotientMeasureEqMeasurePreimage_of_zero Measure.IsAddLeftInvariant.addQuotientMeasureEqMeasurePreimage_of_set MeasurableSet.univ Set.univ_inter LT.lt.ne
leftInvariantIsQuotientMeasureEqMeasurePreimage 📖	mathematical	covolume MulOpposite Subgroup MulOpposite.instGroup SetLike.instMembership Subgroup.instSetLike Subgroup.op Subgroup.one Subgroup.instSMul DFunLike.coe Measure HasQuotient.Quotient QuotientGroup.instHasQuotientSubgroup QuotientGroup.measurableSpace Set ENNReal Measure.instFunLike Set.univ	QuotientMeasureEqMeasurePreimage Subgroup.toGroup MulAction.instMulAction Monoid.toOppositeMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid	—	HasFundamentalDomain.ExistsIsFundamentalDomain measure_lt_top Measure.measure_univ_eq_zero IsFundamentalDomain.covolume_eq_volume Subgroup.instCountableSubtypeMulOppositeMemOp Subgroup.instMeasurableConstSMul MeasurableSMul.toMeasurableConstSMul measurableSMul_opposite_of_mul ContinuousMul.measurableMul IsTopologicalGroup.toContinuousMul Subgroup.smulInvariantMeasure Measure.IsMulRightInvariant.toSMulInvariantMeasure_op IsFundamentalDomain.quotientMeasureEqMeasurePreimage_of_zero Measure.IsMulLeftInvariant.quotientMeasureEqMeasurePreimage_of_set MeasurableSet.univ Set.univ_inter LT.lt.ne

MeasureTheory.AddQuotientMeasureEqMeasurePreimage

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addHaarMeasure_quotient 📖	mathematical	—	MeasureTheory.Measure.IsAddHaarMeasure HasQuotient.Quotient AddSubgroup QuotientAddGroup.instHasQuotientAddSubgroup QuotientAddGroup.Quotient.addGroup QuotientAddGroup.instTopologicalSpace QuotientAddGroup.measurableSpace	—	TopologicalSpace.PositiveCompacts.nonempty' instWeaklyLocallyCompactSpaceOfLocallyCompactSpace Zero.instNonempty QuotientAddGroup.isOpenMap_coe IsTopologicalAddGroup.toContinuousAdd IsScalarTower.right QuotientAddGroup.instIsTopologicalAddGroup AddCosetSpace.borelSpace MeasureTheory.Measure.addHaarMeasure_unique MeasureTheory.sigmaFinite_of_locallyFinite MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure addInvariantMeasure_quotient MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant ne_top_of_lt covolume_ne_top MeasureTheory.Subgroup.vaddInvariantMeasure MeasureTheory.Measure.IsAddRightInvariant.toVAddInvariantMeasure_op AddSubgroup.instCountableSubtypeAddOppositeMemOp AddSubgroup.instMeasurableConstVAdd MeasurableVAdd.toMeasurableConstVAdd measurableVAdd_opposite_of_add ContinuousAdd.measurableAdd MeasureTheory.IsAddFundamentalDomain.addProjection_respects_measure_apply IsCompact.measurableSet BorelSpace.opensMeasurable TopologicalSpace.PositiveCompacts.isCompact MeasureTheory.Measure.IsAddHaarMeasure.smul MeasureTheory.Measure.isAddHaarMeasure_addHaarMeasure MeasureTheory.Measure.IsAddHaarMeasure.toIsOpenPosMeasure MeasureTheory.Measure.IsOpenPosMeasure.open_pos isOpen_interior TopologicalSpace.PositiveCompacts.interior_nonempty MeasureTheory.measure_mono_null MeasureTheory.Measure.instOuterMeasureClass HasSubset.Subset.trans Set.instIsTransSubset interior_subset QuotientAddGroup.coe_mk' Set.subset_preimage_image MeasureTheory.IsAddFundamentalDomain.measure_zero_of_invariant QuotientAddGroup.sound ne_of_lt lt_of_le_of_lt MeasureTheory.measure_mono Set.inter_subset_right Ne.lt_top MeasureTheory.IsAddFundamentalDomain.covolume_eq_volume
addInvariantMeasure_quotient 📖	mathematical	—	MeasureTheory.Measure.IsAddLeftInvariant HasQuotient.Quotient AddSubgroup QuotientAddGroup.instHasQuotientAddSubgroup QuotientAddGroup.measurableSpace AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid QuotientAddGroup.Quotient.addGroup	—	MeasureTheory.Measure.ext AddAction.left_quotientAction MeasureTheory.Measure.map_apply MeasurableAdd.measurable_const_add ContinuousAdd.measurableAdd AddCosetSpace.borelSpace IsTopologicalAddGroup.toContinuousAdd QuotientAddGroup.instIsTopologicalAddGroup AddAction.Quotient.coe_vadd_out Quotient.out_eq MeasureTheory.measure_preimage_vadd vaddInvariantMeasure_quotient
vaddInvariantMeasure_quotient 📖	mathematical	—	MeasureTheory.VAddInvariantMeasure HasQuotient.Quotient AddSubgroup QuotientAddGroup.instHasQuotientAddSubgroup AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddAction.quotient AddMonoid.toAddAction AddAction.left_quotientAction QuotientAddGroup.measurableSpace	—	AddAction.left_quotientAction Continuous.measurable BorelSpace.opensMeasurable Quotient.borelSpace T1Space.t0Space T2Space.t1Space continuous_quotient_mk' MeasureTheory.HasAddFundamentalDomain.ExistsIsAddFundamentalDomain MeasureTheory.IsAddFundamentalDomain.vadd_of_comm MeasurableVAdd.toMeasurableConstVAdd measurableVAdd_of_add ContinuousAdd.measurableAdd IsTopologicalAddGroup.toContinuousAdd MeasureTheory.Measure.IsAddLeftInvariant.vaddInvariantMeasure AddSubgroup.vaddCommClass_right VAddCommClass.opposite_mid VAddAssocClass.left MeasureTheory.IsAddFundamentalDomain.addProjection_respects_measure_apply measurableSet_preimage MeasurableConstVAdd.measurable_const_vadd QuotientAddGroup.measurableVAdd AddCosetSpace.borelSpace Set.ext Set.mem_preimage Set.preimage_inter neg_add_cancel_left MeasureTheory.measure_preimage_add Set.preimage_vadd_neg

MeasureTheory.IsAddFundamentalDomain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
absolutelyContinuous_map 📖	mathematical	MeasureTheory.IsAddFundamentalDomain AddOpposite AddSubgroup AddOpposite.instAddGroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.op AddSubgroup.zero AddSubgroup.instVAdd	MeasureTheory.Measure.AbsolutelyContinuous HasQuotient.Quotient QuotientAddGroup.instHasQuotientAddSubgroup MeasureTheory.Measure.map MeasureTheory.Measure.restrict	—	Continuous.measurable BorelSpace.opensMeasurable continuous_quotient_mk' MeasureTheory.Measure.map_apply measure_zero_of_invariant AddSubgroup.instMeasurableConstVAdd MeasurableVAdd.toMeasurableConstVAdd measurableVAdd_opposite_of_add ContinuousAdd.measurableAdd IsTopologicalAddGroup.toContinuousAdd MeasureTheory.Subgroup.vaddInvariantMeasure MeasureTheory.Measure.IsAddRightInvariant.toVAddInvariantMeasure_op AddSubgroup.instCountableSubtypeAddOppositeMemOp Set.ext Set.mem_vadd_set_iff_neg_vadd_mem Set.mem_preimage QuotientAddGroup.mk_add_of_mem MeasureTheory.Measure.restrict_apply MeasurableSet.preimage

MeasureTheory.IsFundamentalDomain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
absolutelyContinuous_map 📖	mathematical	MeasureTheory.IsFundamentalDomain MulOpposite Subgroup MulOpposite.instGroup SetLike.instMembership Subgroup.instSetLike Subgroup.op Subgroup.one Subgroup.instSMul	MeasureTheory.Measure.AbsolutelyContinuous HasQuotient.Quotient QuotientGroup.instHasQuotientSubgroup MeasureTheory.Measure.map MeasureTheory.Measure.restrict	—	Continuous.measurable BorelSpace.opensMeasurable continuous_quotient_mk' MeasureTheory.Measure.map_apply measure_zero_of_invariant Subgroup.instMeasurableConstSMul MeasurableSMul.toMeasurableConstSMul measurableSMul_opposite_of_mul ContinuousMul.measurableMul IsTopologicalGroup.toContinuousMul MeasureTheory.Subgroup.smulInvariantMeasure MeasureTheory.Measure.IsMulRightInvariant.toSMulInvariantMeasure_op Subgroup.instCountableSubtypeMulOppositeMemOp Set.ext Set.mem_smul_set_iff_inv_smul_mem Set.mem_preimage QuotientGroup.mk_mul_of_mem MeasureTheory.Measure.restrict_apply MeasurableSet.preimage

MeasureTheory.Measure.IsAddLeftInvariant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addQuotientMeasureEqMeasurePreimage_of_set 📖	mathematical	MeasureTheory.IsAddFundamentalDomain AddOpposite AddSubgroup AddOpposite.instAddGroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.op AddSubgroup.zero AddSubgroup.instVAdd MeasurableSet HasQuotient.Quotient QuotientAddGroup.instHasQuotientAddSubgroup QuotientAddGroup.measurableSpace DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike Set.instInter Set.preimage	MeasureTheory.AddQuotientMeasureEqMeasurePreimage AddSubgroup.toAddGroup AddAction.instAddAction AddMonoid.toOppositeAddAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	MeasureTheory.IsAddFundamentalDomain.addQuotientMeasureEqMeasurePreimage MeasureTheory.Subgroup.vaddInvariantMeasure MeasureTheory.Measure.IsAddRightInvariant.toVAddInvariantMeasure_op AddSubgroup.instCountableSubtypeAddOppositeMemOp AddSubgroup.instMeasurableConstVAdd MeasurableVAdd.toMeasurableConstVAdd measurableVAdd_opposite_of_add ContinuousAdd.measurableAdd IsTopologicalAddGroup.toContinuousAdd MeasureTheory.Measure.ext Continuous.measurable BorelSpace.opensMeasurable Quotient.borelSpace T1Space.t0Space T2Space.t1Space continuous_quotient_mk' MeasureTheory.IsAddFundamentalDomain.addQuotientMeasureEqMeasurePreimage_addQuotientMeasure MeasureTheory.AddQuotientMeasureEqMeasurePreimage.addInvariantMeasure_quotient MeasureTheory.AddQuotientMeasureEqMeasurePreimage.sigmaFiniteQuotient IsScalarTower.right MeasureTheory.measure_eq_sub_vadd ContinuousAdd.measurableMul₂ AddCosetSpace.borelSpace QuotientAddGroup.instIsTopologicalAddGroup ContinuousNeg.measurableNeg IsTopologicalAddGroup.toContinuousNeg MeasureTheory.Measure.map_apply MeasureTheory.Measure.restrict_apply measurableSet_quotient ENNReal.div_self one_smul

MeasureTheory.Measure.IsMulLeftInvariant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
quotientMeasureEqMeasurePreimage_of_set 📖	mathematical	MeasureTheory.IsFundamentalDomain MulOpposite Subgroup MulOpposite.instGroup SetLike.instMembership Subgroup.instSetLike Subgroup.op Subgroup.one Subgroup.instSMul MeasurableSet HasQuotient.Quotient QuotientGroup.instHasQuotientSubgroup QuotientGroup.measurableSpace DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike Set.instInter Set.preimage	MeasureTheory.QuotientMeasureEqMeasurePreimage Subgroup.toGroup MulAction.instMulAction Monoid.toOppositeMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid	—	MeasureTheory.IsFundamentalDomain.quotientMeasureEqMeasurePreimage MeasureTheory.Subgroup.smulInvariantMeasure MeasureTheory.Measure.IsMulRightInvariant.toSMulInvariantMeasure_op Subgroup.instCountableSubtypeMulOppositeMemOp Subgroup.instMeasurableConstSMul MeasurableSMul.toMeasurableConstSMul measurableSMul_opposite_of_mul ContinuousMul.measurableMul IsTopologicalGroup.toContinuousMul MeasureTheory.Measure.ext Continuous.measurable BorelSpace.opensMeasurable Quotient.borelSpace T1Space.t0Space T2Space.t1Space continuous_quotient_mk' MeasureTheory.IsFundamentalDomain.quotientMeasureEqMeasurePreimage_quotientMeasure MeasureTheory.QuotientMeasureEqMeasurePreimage.mulInvariantMeasure_quotient MeasureTheory.QuotientMeasureEqMeasurePreimage.sigmaFiniteQuotient IsScalarTower.right MeasureTheory.measure_eq_div_smul ContinuousMul.measurableMul₂ CosetSpace.borelSpace QuotientGroup.instIsTopologicalGroup ContinuousInv.measurableInv IsTopologicalGroup.toContinuousInv MeasureTheory.Measure.map_apply MeasureTheory.Measure.restrict_apply measurableSet_quotient ENNReal.div_self one_smul

MeasureTheory.QuotientMeasureEqMeasurePreimage

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
haarMeasure_quotient 📖	mathematical	—	MeasureTheory.Measure.IsHaarMeasure HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup QuotientGroup.Quotient.group QuotientGroup.instTopologicalSpace QuotientGroup.measurableSpace	—	TopologicalSpace.PositiveCompacts.nonempty' instWeaklyLocallyCompactSpaceOfLocallyCompactSpace One.instNonempty QuotientGroup.isOpenMap_coe IsTopologicalGroup.toContinuousMul IsScalarTower.right QuotientGroup.instIsTopologicalGroup CosetSpace.borelSpace MeasureTheory.Measure.haarMeasure_unique MeasureTheory.sigmaFinite_of_locallyFinite MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure mulInvariantMeasure_quotient MeasureTheory.Measure.IsHaarMeasure.toIsMulLeftInvariant ne_top_of_lt covolume_ne_top MeasureTheory.Subgroup.smulInvariantMeasure MeasureTheory.Measure.IsMulRightInvariant.toSMulInvariantMeasure_op Subgroup.instCountableSubtypeMulOppositeMemOp Subgroup.instMeasurableConstSMul MeasurableSMul.toMeasurableConstSMul measurableSMul_opposite_of_mul ContinuousMul.measurableMul MeasureTheory.IsFundamentalDomain.projection_respects_measure_apply IsCompact.measurableSet BorelSpace.opensMeasurable TopologicalSpace.PositiveCompacts.isCompact MeasureTheory.Measure.IsHaarMeasure.smul MeasureTheory.Measure.isHaarMeasure_haarMeasure MeasureTheory.Measure.IsHaarMeasure.toIsOpenPosMeasure MeasureTheory.Measure.IsOpenPosMeasure.open_pos isOpen_interior TopologicalSpace.PositiveCompacts.interior_nonempty MeasureTheory.measure_mono_null MeasureTheory.Measure.instOuterMeasureClass HasSubset.Subset.trans Set.instIsTransSubset interior_subset QuotientGroup.coe_mk' Set.subset_preimage_image MeasureTheory.IsFundamentalDomain.measure_zero_of_invariant QuotientGroup.sound ne_of_lt lt_of_le_of_lt MeasureTheory.measure_mono Set.inter_subset_right Ne.lt_top MeasureTheory.IsFundamentalDomain.covolume_eq_volume
mulInvariantMeasure_quotient 📖	mathematical	—	MeasureTheory.Measure.IsMulLeftInvariant HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup QuotientGroup.measurableSpace MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid QuotientGroup.Quotient.group	—	MeasureTheory.Measure.ext MulAction.left_quotientAction MeasureTheory.Measure.map_apply MeasurableMul.measurable_const_mul ContinuousMul.measurableMul CosetSpace.borelSpace IsTopologicalGroup.toContinuousMul QuotientGroup.instIsTopologicalGroup Quotient.out_eq MeasureTheory.measure_preimage_smul smulInvariantMeasure_quotient
smulInvariantMeasure_quotient 📖	mathematical	—	MeasureTheory.SMulInvariantMeasure HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction MulAction.quotient Monoid.toMulAction MulAction.left_quotientAction QuotientGroup.measurableSpace	—	MulAction.left_quotientAction Continuous.measurable BorelSpace.opensMeasurable Quotient.borelSpace T1Space.t0Space T2Space.t1Space continuous_quotient_mk' MeasureTheory.HasFundamentalDomain.ExistsIsFundamentalDomain MeasureTheory.IsFundamentalDomain.smul_of_comm MeasurableSMul.toMeasurableConstSMul measurableSMul_of_mul ContinuousMul.measurableMul IsTopologicalGroup.toContinuousMul MeasureTheory.Measure.IsMulLeftInvariant.smulInvariantMeasure Subgroup.smulCommClass_right SMulCommClass.opposite_mid IsScalarTower.left MeasureTheory.IsFundamentalDomain.projection_respects_measure_apply measurableSet_preimage MeasurableConstSMul.measurable_const_smul QuotientGroup.measurableSMul CosetSpace.borelSpace Set.ext Set.preimage_inter inv_mul_cancel_left MeasureTheory.measure_preimage_mul Set.preimage_smul_inv

QuotientAddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integral_eq_integral_automorphize 📖	mathematical	MeasureTheory.IsAddFundamentalDomain AddOpposite AddSubgroup AddOpposite.instAddGroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.op AddSubgroup.zero AddSubgroup.instVAdd MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup MeasureTheory.AEStronglyMeasurable HasQuotient.Quotient instHasQuotientAddSubgroup automorphize ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid MeasureTheory.Measure.map MeasureTheory.Measure.restrict	MeasureTheory.integral	—	MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum'' AddSubgroup.instMeasurableConstVAdd MeasurableVAdd.toMeasurableConstVAdd measurableVAdd_opposite_of_add ContinuousAdd.measurableAdd IsTopologicalAddGroup.toContinuousAdd MeasureTheory.Subgroup.vaddInvariantMeasure MeasureTheory.Measure.IsAddRightInvariant.toVAddInvariantMeasure_op AddSubgroup.instCountableSubtypeAddOppositeMemOp MeasureTheory.integral_tsum MeasureTheory.AEStronglyMeasurable.restrict MeasureTheory.AEStronglyMeasurable.comp_quasiMeasurePreserving MeasureTheory.MeasurePreserving.quasiMeasurePreserving MeasureTheory.measurePreserving_vadd MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum'' ne_of_lt MeasureTheory.integral_map Continuous.aemeasurable BorelSpace.opensMeasurable continuous_quotient_mk'
integral_mul_eq_integral_automorphize_mul 📖	mathematical	MeasureTheory.IsAddFundamentalDomain AddOpposite AddSubgroup AddOpposite.instAddGroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.op AddSubgroup.zero AddSubgroup.instVAdd MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing MeasureTheory.AEStronglyMeasurable HasQuotient.Quotient instHasQuotientAddSubgroup MeasureTheory.Measure.map MeasureTheory.Measure.restrict automorphize ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing	MeasureTheory.integral Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing	—	Continuous.measurable BorelSpace.opensMeasurable continuous_quotient_mk' automorphize_smul_left TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing MeasureTheory.AEStronglyMeasurable.comp_measurable MeasureTheory.AEStronglyMeasurable.mono_ac MeasureTheory.IsAddFundamentalDomain.absolutelyContinuous_map MeasureTheory.Integrable.essSup_smul NormedSpace.toIsBoundedSMul Continuous.comp_aestronglyMeasurable continuous_enorm MeasureTheory.AEStronglyMeasurable.aemeasurable TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace ENNReal.instMetrizableSpace ENNReal.borelSpace MeasureTheory.AEStronglyMeasurable.mul integral_eq_integral_automorphize
measurableVAdd 📖	mathematical	—	MeasurableVAdd HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddAction.quotient AddMonoid.toAddAction AddAction.left_quotientAction measurableSpace	—	AddAction.left_quotientAction MeasurableVAdd.toMeasurableConstVAdd ContinuousVAdd.toMeasurableVAdd BorelSpace.opensMeasurable instContinuousVAdd IsTopologicalAddGroup.toContinuousAdd Measurable.vadd_const measurable_id'

QuotientGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integral_eq_integral_automorphize 📖	mathematical	MeasureTheory.IsFundamentalDomain MulOpposite Subgroup MulOpposite.instGroup SetLike.instMembership Subgroup.instSetLike Subgroup.op Subgroup.one Subgroup.instSMul MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup MeasureTheory.AEStronglyMeasurable HasQuotient.Quotient instHasQuotientSubgroup automorphize ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid MeasureTheory.Measure.map MeasureTheory.Measure.restrict	MeasureTheory.integral	—	MeasureTheory.IsFundamentalDomain.integral_eq_tsum'' Subgroup.instMeasurableConstSMul MeasurableSMul.toMeasurableConstSMul measurableSMul_opposite_of_mul ContinuousMul.measurableMul IsTopologicalGroup.toContinuousMul MeasureTheory.Subgroup.smulInvariantMeasure MeasureTheory.Measure.IsMulRightInvariant.toSMulInvariantMeasure_op Subgroup.instCountableSubtypeMulOppositeMemOp MeasureTheory.integral_tsum MeasureTheory.AEStronglyMeasurable.restrict MeasureTheory.AEStronglyMeasurable.comp_quasiMeasurePreserving MeasureTheory.MeasurePreserving.quasiMeasurePreserving MeasureTheory.measurePreserving_smul MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum'' ne_of_lt MeasureTheory.integral_map Continuous.aemeasurable BorelSpace.opensMeasurable continuous_quotient_mk'
integral_mul_eq_integral_automorphize_mul 📖	mathematical	MeasureTheory.IsFundamentalDomain MulOpposite Subgroup MulOpposite.instGroup SetLike.instMembership Subgroup.instSetLike Subgroup.op Subgroup.one Subgroup.instSMul MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing MeasureTheory.AEStronglyMeasurable HasQuotient.Quotient instHasQuotientSubgroup MeasureTheory.Measure.map MeasureTheory.Measure.restrict automorphize ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing	MeasureTheory.integral Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing	—	Continuous.measurable BorelSpace.opensMeasurable continuous_quotient_mk' automorphize_smul_left TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing MeasureTheory.AEStronglyMeasurable.comp_measurable MeasureTheory.AEStronglyMeasurable.mono_ac MeasureTheory.IsFundamentalDomain.absolutelyContinuous_map MeasureTheory.Integrable.essSup_smul NormedSpace.toIsBoundedSMul Continuous.comp_aestronglyMeasurable continuous_enorm MeasureTheory.AEStronglyMeasurable.aemeasurable TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace ENNReal.instMetrizableSpace ENNReal.borelSpace MeasureTheory.AEStronglyMeasurable.mul integral_eq_integral_automorphize
measurableSMul 📖	mathematical	—	MeasurableSMul HasQuotient.Quotient Subgroup instHasQuotientSubgroup SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction MulAction.quotient Monoid.toMulAction MulAction.left_quotientAction measurableSpace	—	MulAction.left_quotientAction MeasurableSMul.toMeasurableConstSMul ContinuousSMul.toMeasurableSMul BorelSpace.opensMeasurable instContinuousSMul IsTopologicalGroup.toContinuousMul Measurable.smul_const measurable_id'

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
essSup_comp_quotientAddGroup_mk 📖	mathematical	MeasureTheory.IsAddFundamentalDomain AddOpposite AddSubgroup AddOpposite.instAddGroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.op AddSubgroup.zero AddSubgroup.instVAdd AEMeasurable HasQuotient.Quotient QuotientAddGroup.instHasQuotientAddSubgroup ENNReal ENNReal.measurableSpace MeasureTheory.Measure.map MeasureTheory.Measure.restrict	essSup ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder	—	Continuous.measurable BorelSpace.opensMeasurable continuous_quotient_mk' essSup_map_measure ENNReal.instSecondCountableTopology OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology ENNReal.borelSpace Measurable.aemeasurable MeasureTheory.IsAddFundamentalDomain.essSup_measure_restrict AddSubgroup.instMeasurableConstVAdd MeasurableVAdd.toMeasurableConstVAdd measurableVAdd_opposite_of_add ContinuousAdd.measurableAdd IsTopologicalAddGroup.toContinuousAdd MeasureTheory.Subgroup.vaddInvariantMeasure MeasureTheory.Measure.IsAddRightInvariant.toVAddInvariantMeasure_op AddSubgroup.instCountableSubtypeAddOppositeMemOp QuotientAddGroup.mk_add_of_mem
essSup_comp_quotientGroup_mk 📖	mathematical	MeasureTheory.IsFundamentalDomain MulOpposite Subgroup MulOpposite.instGroup SetLike.instMembership Subgroup.instSetLike Subgroup.op Subgroup.one Subgroup.instSMul AEMeasurable HasQuotient.Quotient QuotientGroup.instHasQuotientSubgroup ENNReal ENNReal.measurableSpace MeasureTheory.Measure.map MeasureTheory.Measure.restrict	essSup ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder	—	Continuous.measurable BorelSpace.opensMeasurable continuous_quotient_mk' essSup_map_measure ENNReal.instSecondCountableTopology OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology ENNReal.borelSpace Measurable.aemeasurable MeasureTheory.IsFundamentalDomain.essSup_measure_restrict Subgroup.instMeasurableConstSMul MeasurableSMul.toMeasurableConstSMul measurableSMul_opposite_of_mul ContinuousMul.measurableMul IsTopologicalGroup.toContinuousMul MeasureTheory.Subgroup.smulInvariantMeasure MeasureTheory.Measure.IsMulRightInvariant.toSMulInvariantMeasure_op Subgroup.instCountableSubtypeMulOppositeMemOp QuotientGroup.mk_mul_of_mem
measurePreserving_quotientAddGroup_mk_of_AddQuotientMeasureEqMeasurePreimage 📖	mathematical	MeasureTheory.IsAddFundamentalDomain AddOpposite AddSubgroup AddOpposite.instAddGroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.op AddSubgroup.zero AddSubgroup.instVAdd	MeasureTheory.MeasurePreserving HasQuotient.Quotient QuotientAddGroup.instHasQuotientAddSubgroup QuotientAddGroup.measurableSpace MeasureTheory.Measure.restrict	—	—
measurePreserving_quotientGroup_mk_of_QuotientMeasureEqMeasurePreimage 📖	mathematical	MeasureTheory.IsFundamentalDomain MulOpposite Subgroup MulOpposite.instGroup SetLike.instMembership Subgroup.instSetLike Subgroup.op Subgroup.one Subgroup.instSMul	MeasureTheory.MeasurePreserving HasQuotient.Quotient QuotientGroup.instHasQuotientSubgroup QuotientGroup.measurableSpace MeasureTheory.Measure.restrict	—	—

---

← Back to Index