FundamentalDomain

📁 Source: Mathlib/MeasureTheory/Group/FundamentalDomain.lean

Statistics

Metric	Count
Definitions `AddQuotientMeasureEqMeasurePreimage`, `HasAddFundamentalDomain`, `HasFundamentalDomain`, `IsAddFundamentalDomain`, `IsFundamentalDomain`, `QuotientMeasureEqMeasurePreimage`, `addCovolume`, `addFundamentalFrontier`, `addFundamentalInterior`, `covolume`, `fundamentalFrontier`, `fundamentalInterior`	12
Theorems `addProjection_respects_measure'`, `covolume_ne_top`, `isFiniteMeasure_quotient`, `sigmaFiniteQuotient`, `unique`, `ExistsIsAddFundamentalDomain`, `ExistsIsFundamentalDomain`, `addProjection_respects_measure`, `addProjection_respects_measure_apply`, `addQuotientMeasureEqMeasurePreimage`, `addQuotientMeasureEqMeasurePreimage_addQuotientMeasure`, `addQuotientMeasureEqMeasurePreimage_of_zero`, `addQuotientMeasure_eq`, `ae_covers`, `aedisjoint`, `aestronglyMeasurable_on_iff`, `covolume_eq_volume`, `essSup_measure_restrict`, `exists_ne_zero_vadd_eq`, `hasAddFundamentalDomain`, `hasFiniteIntegral_on_iff`, `iUnion_vadd_ae_eq`, `image_of_equiv`, `integrableOn_iff`, `integral_eq_tsum`, `integral_eq_tsum'`, `integral_eq_tsum''`, `integral_eq_tsum_of_ac`, `lintegral_eq_tsum`, `lintegral_eq_tsum'`, `lintegral_eq_tsum''`, `lintegral_eq_tsum_of_ac`, `measurePreserving_add_quotient_mk`, `measure_addFundamentalFrontier`, `measure_addFundamentalInterior`, `measure_eq`, `measure_eq_card_smul_of_vadd_ae_eq_self`, `measure_eq_tsum`, `measure_eq_tsum'`, `measure_eq_tsum_of_ac`, `measure_le_of_pairwise_disjoint`, `measure_ne_zero`, `measure_set_eq`, `measure_zero_of_invariant`, `mk'`, `mk''`, `mk_of_measure_univ_le`, `mono`, `nullMeasurableSet`, `nullMeasurableSet_vadd`, `pairwise_aedisjoint_of_ac`, `preimage_of_equiv`, `restrict_restrict`, `setIntegral_eq`, `setIntegral_eq_tsum`, `setIntegral_eq_tsum'`, `setLIntegral_eq`, `setLIntegral_eq_tsum`, `setLIntegral_eq_tsum'`, `sum_restrict`, `sum_restrict_of_ac`, `vadd`, `vadd_of_comm`, `ae_covers`, `aedisjoint`, `aestronglyMeasurable_on_iff`, `covolume_eq_volume`, `essSup_measure_restrict`, `exists_ne_one_smul_eq`, `fundamentalInterior`, `hasFiniteIntegral_on_iff`, `hasFundamentalDomain`, `iUnion_smul_ae_eq`, `image_of_equiv`, `integrableOn_iff`, `integral_eq_tsum`, `integral_eq_tsum'`, `integral_eq_tsum''`, `integral_eq_tsum_of_ac`, `lintegral_eq_tsum`, `lintegral_eq_tsum'`, `lintegral_eq_tsum''`, `lintegral_eq_tsum_of_ac`, `measurePreserving_quotient_mk`, `measure_eq`, `measure_eq_card_smul_of_smul_ae_eq_self`, `measure_eq_tsum`, `measure_eq_tsum'`, `measure_eq_tsum_of_ac`, `measure_fundamentalFrontier`, `measure_fundamentalInterior`, `measure_le_of_pairwise_disjoint`, `measure_ne_zero`, `measure_set_eq`, `measure_zero_of_invariant`, `mk'`, `mk''`, `mk_of_measure_univ_le`, `mono`, `nullMeasurableSet`, `nullMeasurableSet_smul`, `pairwise_aedisjoint_of_ac`, `preimage_of_equiv`, `projection_respects_measure`, `projection_respects_measure_apply`, `quotientMeasureEqMeasurePreimage`, `quotientMeasureEqMeasurePreimage_of_zero`, `quotientMeasureEqMeasurePreimage_quotientMeasure`, `quotientMeasure_eq`, `restrict_restrict`, `setIntegral_eq`, `setIntegral_eq_tsum`, `setIntegral_eq_tsum'`, `setLIntegral_eq`, `setLIntegral_eq_tsum`, `setLIntegral_eq_tsum'`, `smul`, `smul_of_comm`, `sum_restrict`, `sum_restrict_of_ac`, `addFundamentalFrontier`, `addFundamentalInterior`, `fundamentalFrontier`, `fundamentalInterior`, `covolume_ne_top`, `isFiniteMeasure_quotient`, `projection_respects_measure'`, `sigmaFiniteQuotient`, `unique`, `addFundamentalFrontier_subset`, `addFundamentalFrontier_union_addFundamentalInterior`, `addFundamentalFrontier_vadd`, `addFundamentalInterior_subset`, `addFundamentalInterior_union_addFundamentalFrontier`, `addFundamentalInterior_vadd`, `addMeasure_map_restrict_apply`, `disjoint_addFundamentalInterior_addFundamentalFrontier`, `disjoint_fundamentalInterior_fundamentalFrontier`, `fundamentalFrontier_smul`, `fundamentalFrontier_subset`, `fundamentalFrontier_union_fundamentalInterior`, `fundamentalInterior_smul`, `fundamentalInterior_subset`, `fundamentalInterior_union_fundamentalFrontier`, `instSigmaFiniteAddQuotientOrbitRelInstMeasurableSpaceToMeasurableSpace`, `instSigmaFiniteQuotientOrbitRelOfHasFundamentalDomainOfQuotientMeasureEqMeasurePreimageVolume`, `measure_map_restrict_apply`, `mem_addFundamentalFrontier`, `mem_addFundamentalInterior`, `mem_fundamentalFrontier`, `mem_fundamentalInterior`, `pairwise_disjoint_addFundamentalInterior`, `pairwise_disjoint_fundamentalInterior`, `sdiff_addFundamentalFrontier`, `sdiff_addFundamentalInterior`, `sdiff_fundamentalFrontier`, `sdiff_fundamentalInterior`	157
Total	169

MeasureTheory

Definitions

Name	Category	Theorems
`AddQuotientMeasureEqMeasurePreimage` 📖	CompData	8 math math: `IsAddFundamentalDomain.addQuotientMeasureEqMeasurePreimage`, `Measure.IsAddLeftInvariant.addQuotientMeasureEqMeasurePreimage_of_set`, `IsAddFundamentalDomain.addQuotientMeasureEqMeasurePreimage_of_zero`, `IsFundamentalDomain.AddQuotientMeasureEqMeasurePreimage_AddHaarMeasure`, `AddCircle.instAddQuotientMeasureEqMeasurePreimageSubtypeAddOppositeRealMemAddSubgroupOpZmultiplesVolume`, `IsAddFundamentalDomain.addQuotientMeasureEqMeasurePreimage_addQuotientMeasure`, `leftInvariantIsAddQuotientMeasureEqMeasurePreimage`, `IsFundamentalDomain.AddQuotientMeasureEqMeasurePreimage_vaddAddHaarMeasure`
`HasAddFundamentalDomain` 📖	CompData	2 math math: `IsAddFundamentalDomain.hasAddFundamentalDomain`, `AddCircle.instHasAddFundamentalDomainSubtypeAddOppositeRealMemAddSubgroupOpZmultiples`
`HasFundamentalDomain` 📖	CompData	1 math math: `IsFundamentalDomain.hasFundamentalDomain`
`IsAddFundamentalDomain` 📖	CompData	17 math math: `NumberField.mixedEmbedding.fundamentalDomain_integerLattice`, `IsAddFundamentalDomain.mk_of_measure_univ_le`, `AddCircle.isAddFundamentalDomain_of_ae_ball`, `IsAddFundamentalDomain.mono`, `IsAddFundamentalDomain.vadd_of_comm`, `NumberField.mixedEmbedding.fundamentalDomain_idealLattice`, `isAddFundamentalDomain_Ioc`, `IsAddFundamentalDomain.image_of_equiv`, `ZSpan.isAddFundamentalDomain'`, `IsAddFundamentalDomain.mk'`, `ZSpan.isAddFundamentalDomain`, `HasAddFundamentalDomain.ExistsIsAddFundamentalDomain`, `ZLattice.isAddFundamentalDomain`, `IsAddFundamentalDomain.vadd`, `IsAddFundamentalDomain.preimage_of_equiv`, `IsAddFundamentalDomain.mk''`, `isAddFundamentalDomain_Ioc'`
`IsFundamentalDomain` 📖	CompData	10 math math: `IsFundamentalDomain.mk''`, `IsFundamentalDomain.mono`, `HasFundamentalDomain.ExistsIsFundamentalDomain`, `IsFundamentalDomain.mk_of_measure_univ_le`, `IsFundamentalDomain.smul`, `IsFundamentalDomain.mk'`, `IsFundamentalDomain.fundamentalInterior`, `IsFundamentalDomain.preimage_of_equiv`, `IsFundamentalDomain.image_of_equiv`, `IsFundamentalDomain.smul_of_comm`
`QuotientMeasureEqMeasurePreimage` 📖	CompData	7 math math: `IsFundamentalDomain.quotientMeasureEqMeasurePreimage_of_zero`, `Measure.IsMulLeftInvariant.quotientMeasureEqMeasurePreimage_of_set`, `IsFundamentalDomain.quotientMeasureEqMeasurePreimage`, `IsFundamentalDomain.QuotientMeasureEqMeasurePreimage_HaarMeasure`, `IsFundamentalDomain.QuotientMeasureEqMeasurePreimage_smulHaarMeasure`, `IsFundamentalDomain.quotientMeasureEqMeasurePreimage_quotientMeasure`, `leftInvariantIsQuotientMeasureEqMeasurePreimage`
`addCovolume` 📖	CompOp	2 math math: `IsAddFundamentalDomain.covolume_eq_volume`, `AddQuotientMeasureEqMeasurePreimage.covolume_ne_top`
`addFundamentalFrontier` 📖	CompOp	10 math math: `sdiff_addFundamentalInterior`, `mem_addFundamentalFrontier`, `disjoint_addFundamentalInterior_addFundamentalFrontier`, `NullMeasurableSet.addFundamentalFrontier`, `addFundamentalInterior_union_addFundamentalFrontier`, `sdiff_addFundamentalFrontier`, `IsAddFundamentalDomain.measure_addFundamentalFrontier`, `addFundamentalFrontier_union_addFundamentalInterior`, `addFundamentalFrontier_vadd`, `addFundamentalFrontier_subset`
`addFundamentalInterior` 📖	CompOp	11 math math: `IsAddFundamentalDomain.measure_addFundamentalInterior`, `sdiff_addFundamentalInterior`, `disjoint_addFundamentalInterior_addFundamentalFrontier`, `mem_addFundamentalInterior`, `NullMeasurableSet.addFundamentalInterior`, `addFundamentalInterior_union_addFundamentalFrontier`, `addFundamentalInterior_subset`, `sdiff_addFundamentalFrontier`, `addFundamentalFrontier_union_addFundamentalInterior`, `pairwise_disjoint_addFundamentalInterior`, `addFundamentalInterior_vadd`
`covolume` 📖	CompOp	2 math math: `IsFundamentalDomain.covolume_eq_volume`, `QuotientMeasureEqMeasurePreimage.covolume_ne_top`
`fundamentalFrontier` 📖	CompOp	10 math math: `mem_fundamentalFrontier`, `fundamentalFrontier_smul`, `sdiff_fundamentalInterior`, `disjoint_fundamentalInterior_fundamentalFrontier`, `NullMeasurableSet.fundamentalFrontier`, `fundamentalFrontier_subset`, `sdiff_fundamentalFrontier`, `fundamentalFrontier_union_fundamentalInterior`, `IsFundamentalDomain.measure_fundamentalFrontier`, `fundamentalInterior_union_fundamentalFrontier`
`fundamentalInterior` 📖	CompOp	12 math math: `pairwise_disjoint_fundamentalInterior`, `mem_fundamentalInterior`, `sdiff_fundamentalInterior`, `disjoint_fundamentalInterior_fundamentalFrontier`, `fundamentalInterior_subset`, `sdiff_fundamentalFrontier`, `fundamentalFrontier_union_fundamentalInterior`, `NullMeasurableSet.fundamentalInterior`, `IsFundamentalDomain.fundamentalInterior`, `IsFundamentalDomain.measure_fundamentalInterior`, `fundamentalInterior_union_fundamentalFrontier`, `fundamentalInterior_smul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addFundamentalFrontier_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `addFundamentalFrontier`	—	`Set.inter_subset_left`
`addFundamentalFrontier_union_addFundamentalInterior` 📖	mathematical	—	`Set` `Set.instUnion` `addFundamentalFrontier` `addFundamentalInterior`	—	`Set.inter_union_diff`
`addFundamentalFrontier_vadd` 📖	mathematical	—	`addFundamentalFrontier` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`Set.vadd_set_inter` `Set.vadd_set_iUnion` `Set.iUnion_congr_Prop` `VAddCommClass.vadd_comm` `Set.vaddCommClass_set`
`addFundamentalInterior_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `addFundamentalInterior`	—	`Set.diff_subset`
`addFundamentalInterior_union_addFundamentalFrontier` 📖	mathematical	—	`Set` `Set.instUnion` `addFundamentalInterior` `addFundamentalFrontier`	—	`Set.diff_union_inter`
`addFundamentalInterior_vadd` 📖	mathematical	—	`addFundamentalInterior` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`Set.vadd_set_sdiff` `Set.vadd_set_iUnion` `Set.iUnion_congr_Prop` `VAddCommClass.vadd_comm` `Set.vaddCommClass_set`
`addMeasure_map_restrict_apply` 📖	mathematical	`MeasurableSet` `AddAction.orbitRel` `Quotient.instMeasurableSpace`	`DFunLike.coe` `Measure` `AddAction.orbitRel` `Quotient.instMeasurableSpace` `Set` `ENNReal` `Measure.instFunLike` `Measure.map` `Measure.restrict` `Set.instInter` `Set.preimage`	—	`Measure.map_apply` `measurableSet_quotient` `Measure.restrict_apply`
`disjoint_addFundamentalInterior_addFundamentalFrontier` 📖	mathematical	—	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `addFundamentalInterior` `addFundamentalFrontier`	—	`Disjoint.mono_right` `inf_le_right` `disjoint_sdiff_self_left`
`disjoint_fundamentalInterior_fundamentalFrontier` 📖	mathematical	—	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `fundamentalInterior` `fundamentalFrontier`	—	`Disjoint.mono_right` `inf_le_right` `disjoint_sdiff_self_left`
`fundamentalFrontier_smul` 📖	mathematical	—	`fundamentalFrontier` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`Set.smul_set_inter` `Set.smul_set_iUnion` `Set.iUnion_congr_Prop` `SMulCommClass.smul_comm` `Set.smulCommClass_set`
`fundamentalFrontier_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `fundamentalFrontier`	—	`Set.inter_subset_left`
`fundamentalFrontier_union_fundamentalInterior` 📖	mathematical	—	`Set` `Set.instUnion` `fundamentalFrontier` `fundamentalInterior`	—	`Set.inter_union_diff`
`fundamentalInterior_smul` 📖	mathematical	—	`fundamentalInterior` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`Set.smul_set_sdiff` `Set.smul_set_iUnion` `Set.iUnion_congr_Prop` `SMulCommClass.smul_comm` `Set.smulCommClass_set`
`fundamentalInterior_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `fundamentalInterior`	—	`Set.diff_subset`
`fundamentalInterior_union_fundamentalFrontier` 📖	mathematical	—	`Set` `Set.instUnion` `fundamentalInterior` `fundamentalFrontier`	—	`Set.diff_union_inter`
`instSigmaFiniteAddQuotientOrbitRelInstMeasurableSpaceToMeasurableSpace` 📖	mathematical	—	`SigmaFinite` `AddAction.orbitRel` `Quotient.instMeasurableSpace` `MeasureSpace.toMeasurableSpace`	—	`AddQuotientMeasureEqMeasurePreimage.sigmaFiniteQuotient`
`instSigmaFiniteQuotientOrbitRelOfHasFundamentalDomainOfQuotientMeasureEqMeasurePreimageVolume` 📖	mathematical	—	`SigmaFinite` `MulAction.orbitRel` `Quotient.instMeasurableSpace` `MeasureSpace.toMeasurableSpace`	—	`QuotientMeasureEqMeasurePreimage.sigmaFiniteQuotient`
`measure_map_restrict_apply` 📖	mathematical	`MeasurableSet` `MulAction.orbitRel` `Quotient.instMeasurableSpace`	`DFunLike.coe` `Measure` `MulAction.orbitRel` `Quotient.instMeasurableSpace` `Set` `ENNReal` `Measure.instFunLike` `Measure.map` `Measure.restrict` `Set.instInter` `Set.preimage`	—	`Measure.map_apply` `measurableSet_quotient` `Measure.restrict_apply`
`mem_addFundamentalFrontier` 📖	mathematical	—	`Set` `Set.instMembership` `addFundamentalFrontier` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`Set.mem_inter_iff` `Set.mem_iUnion`
`mem_addFundamentalInterior` 📖	mathematical	—	`Set` `Set.instMembership` `addFundamentalInterior` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`Set.mem_diff` `Set.mem_iUnion`
`mem_fundamentalFrontier` 📖	mathematical	—	`Set` `Set.instMembership` `fundamentalFrontier` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	—
`mem_fundamentalInterior` 📖	mathematical	—	`Set` `Set.instMembership` `fundamentalInterior` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	—
`pairwise_disjoint_addFundamentalInterior` 📖	mathematical	—	`Pairwise` `Function.onFun` `Set` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `addFundamentalInterior`	—	`Set.disjoint_left` `mem_addFundamentalInterior` `neg_add_eq_iff_eq_add` `add_zero` `AddSemigroupAction.add_vadd` `Set.mem_neg_vadd_set_iff` `Set.vadd_mem_vadd_set_iff`
`pairwise_disjoint_fundamentalInterior` 📖	mathematical	—	`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.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `fundamentalInterior`	—	`Set.disjoint_left` `mem_fundamentalInterior` `inv_mul_eq_iff_eq_mul` `mul_one` `SemigroupAction.mul_smul`
`sdiff_addFundamentalFrontier` 📖	mathematical	—	`Set` `Set.instSDiff` `addFundamentalFrontier` `addFundamentalInterior`	—	`Set.diff_self_inter`
`sdiff_addFundamentalInterior` 📖	mathematical	—	`Set` `Set.instSDiff` `addFundamentalInterior` `addFundamentalFrontier`	—	`sdiff_sdiff_right_self`
`sdiff_fundamentalFrontier` 📖	mathematical	—	`Set` `Set.instSDiff` `fundamentalFrontier` `fundamentalInterior`	—	`Set.diff_self_inter`
`sdiff_fundamentalInterior` 📖	mathematical	—	`Set` `Set.instSDiff` `fundamentalInterior` `fundamentalFrontier`	—	`sdiff_sdiff_right_self`

MeasureTheory.AddQuotientMeasureEqMeasurePreimage

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addProjection_respects_measure'` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`MeasureTheory.Measure.map` `AddAction.orbitRel` `Quotient.instMeasurableSpace` `MeasureTheory.Measure.restrict`	—	—
`covolume_ne_top` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `MeasureTheory.addCovolume` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `Top.top` `instTopENNReal`	—	`MeasureTheory.HasAddFundamentalDomain.ExistsIsAddFundamentalDomain` `MeasureTheory.IsFiniteMeasure.measure_univ_lt_top` `MeasureTheory.IsAddFundamentalDomain.covolume_eq_volume` `Set.univ_inter` `MeasureTheory.IsAddFundamentalDomain.addProjection_respects_measure_apply` `MeasurableSet.univ` `ENNReal.zero_lt_top`
`isFiniteMeasure_quotient` 📖	mathematical	—	`MeasureTheory.IsFiniteMeasure` `AddAction.orbitRel` `Quotient.instMeasurableSpace`	—	`MeasureTheory.HasAddFundamentalDomain.ExistsIsAddFundamentalDomain` `MeasureTheory.IsAddFundamentalDomain.addProjection_respects_measure` `MeasureTheory.IsAddFundamentalDomain.covolume_eq_volume` `Ne.lt_top` `MeasureTheory.Measure.isFiniteMeasure_map` `MeasureTheory.Restrict.isFiniteMeasure`
`sigmaFiniteQuotient` 📖	mathematical	—	`MeasureTheory.SigmaFinite` `AddAction.orbitRel` `Quotient.instMeasurableSpace`	—	`MeasureTheory.sigmaFinite_iff` `Set.mem_univ` `AddAction.quotient_preimage_image_eq_union_add` `measurableSet_quotient` `MeasurableSet.iUnion` `MeasurableSet.const_vadd` `MeasureTheory.IsAddFundamentalDomain.addProjection_respects_measure_apply` `Set.iUnion_inter` `lt_of_le_of_lt` `MeasureTheory.IsAddFundamentalDomain.measure_eq_tsum` `MeasureTheory.measure_iUnion_le` `MeasureTheory.Measure.instOuterMeasureClass` `Set.image_iUnion` `Set.image_univ_of_surjective` `Quotient.mk'_surjective`
`unique` 📖	—	—	—	—	`MeasureTheory.HasAddFundamentalDomain.ExistsIsAddFundamentalDomain` `MeasureTheory.IsAddFundamentalDomain.addProjection_respects_measure`

MeasureTheory.HasAddFundamentalDomain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ExistsIsAddFundamentalDomain` 📖	mathematical	—	`Set` `MeasureTheory.IsAddFundamentalDomain`	—	—

MeasureTheory.HasFundamentalDomain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ExistsIsFundamentalDomain` 📖	mathematical	—	`Set` `MeasureTheory.IsFundamentalDomain`	—	—

MeasureTheory.IsAddFundamentalDomain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addProjection_respects_measure` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`MeasureTheory.Measure.map` `AddAction.orbitRel` `Quotient.instMeasurableSpace` `MeasureTheory.Measure.restrict`	—	`MeasureTheory.AddQuotientMeasureEqMeasurePreimage.addProjection_respects_measure'`
`addProjection_respects_measure_apply` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `MeasurableSet` `AddAction.orbitRel` `Quotient.instMeasurableSpace`	`DFunLike.coe` `MeasureTheory.Measure` `AddAction.orbitRel` `Quotient.instMeasurableSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `Set.instInter` `Set.preimage`	—	`addProjection_respects_measure` `MeasureTheory.addMeasure_map_restrict_apply`
`addQuotientMeasureEqMeasurePreimage` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `MeasureTheory.Measure.map` `AddAction.orbitRel` `Quotient.instMeasurableSpace` `MeasureTheory.Measure.restrict`	`MeasureTheory.AddQuotientMeasureEqMeasurePreimage`	—	`addQuotientMeasureEqMeasurePreimage_addQuotientMeasure`
`addQuotientMeasureEqMeasurePreimage_addQuotientMeasure` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`MeasureTheory.AddQuotientMeasureEqMeasurePreimage` `MeasureTheory.Measure.map` `AddAction.orbitRel` `Quotient.instMeasurableSpace` `MeasureTheory.Measure.restrict`	—	`addQuotientMeasure_eq`
`addQuotientMeasureEqMeasurePreimage_of_zero` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `instZeroENNReal`	`MeasureTheory.AddQuotientMeasureEqMeasurePreimage` `MeasureTheory.Measure` `AddAction.orbitRel` `Quotient.instMeasurableSpace` `MeasureTheory.Measure.instZero`	—	`addQuotientMeasureEqMeasurePreimage` `MeasureTheory.Measure.ext` `MeasureTheory.addMeasure_map_restrict_apply` `MeasureTheory.measure_inter_null_of_null_right`
`addQuotientMeasure_eq` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`MeasureTheory.Measure.map` `AddAction.orbitRel` `Quotient.instMeasurableSpace` `MeasureTheory.Measure.restrict`	—	`MeasureTheory.Measure.ext` `MeasureTheory.addMeasure_map_restrict_apply` `measure_set_eq` `measurableSet_quotient` `Set.ext` `Set.mem_preimage`
`ae_covers` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain`	`Filter.Eventually` `Set` `Set.instMembership` `HVAdd.hVAdd` `instHVAdd` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	—
`aedisjoint` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain`	`Pairwise` `Function.onFun` `Set` `MeasureTheory.AEDisjoint` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet`	—	—
`aestronglyMeasurable_on_iff` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `HVAdd.hVAdd` `instHVAdd`	`MeasureTheory.AEStronglyMeasurable` `MeasureTheory.Measure.restrict`	—	`restrict_restrict` `sum_restrict_of_ac` `LE.le.absolutelyContinuous` `MeasureTheory.Measure.restrict_le_self` `Set.inter_comm` `aestronglyMeasurable_sum_measure_iff` `Set.vadd_set_inter` `vadd_neg_vadd` `Function.Surjective.forall` `neg_surjective` `neg_neg` `measurableEmbedding_const_vadd` `Set.image_vadd` `MeasureTheory.MeasurePreserving.aestronglyMeasurable_comp_iff` `MeasureTheory.MeasurePreserving.restrict_image_emb` `MeasureTheory.measurePreserving_vadd`
`covolume_eq_volume` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`MeasureTheory.addCovolume` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike`	—	`MeasureTheory.HasAddFundamentalDomain.ExistsIsAddFundamentalDomain` `hasAddFundamentalDomain` `measure_eq`
`essSup_measure_restrict` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `HVAdd.hVAdd` `instHVAdd`	`essSup` `ENNReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `MeasureTheory.Measure.restrict`	—	`le_antisymm` `essSup_mono_measure'` `MeasureTheory.Measure.restrict_le_self` `essSup_eq_sInf` `sInf_le_sInf` `measure_zero_of_invariant` `Set.ext` `Set.mem_vadd_set_iff_neg_vadd_mem` `MeasureTheory.Measure.restrict_apply₀'` `nullMeasurableSet`
`exists_ne_zero_vadd_eq` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `MeasureTheory.NullMeasurableSet` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike`	`Set` `Set.instMembership` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_exists` `Mathlib.Tactic.Push.not_and_eq` `not_lt` `measure_le_of_pairwise_disjoint` `Pairwise.aedisjoint` `Disjoint.inf_right` `Disjoint.inf_left` `Set.disjoint_left` `neg_add_eq_zero` `AddSemigroupAction.add_vadd` `neg_vadd_vadd`
`hasAddFundamentalDomain` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`MeasureTheory.HasAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	—
`hasFiniteIntegral_on_iff` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `HVAdd.hVAdd` `instHVAdd`	`MeasureTheory.HasFiniteIntegral` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `MeasureTheory.Measure.restrict`	—	`setLIntegral_eq`
`iUnion_vadd_ae_eq` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `Set.iUnion` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `Set.univ`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Filter.eventuallyEq_univ` `Filter.Eventually.mono` `ae_covers` `Set.mem_iUnion` `neg_vadd_vadd`
`image_of_equiv` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `MeasureTheory.Measure.QuasiMeasurePreserving` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `Function.Semiconj` `HVAdd.hVAdd` `instHVAdd`	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `Set.image` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`Equiv.image_eq_preimage_symm` `preimage_of_equiv` `Equiv.bijective` `Equiv.surjective` `Equiv.symm_apply_apply` `Equiv.apply_symm_apply`
`integrableOn_iff` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `HVAdd.hVAdd` `instHVAdd`	`MeasureTheory.IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`aestronglyMeasurable_on_iff` `PseudoEMetricSpace.pseudoMetrizableSpace` `hasFiniteIntegral_on_iff`
`integral_eq_tsum` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`MeasureTheory.integral` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `MeasureTheory.Measure.restrict` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `SummationFilter.unconditional`	—	`integral_eq_tsum_of_ac` `MeasureTheory.Measure.AbsolutelyContinuous.refl`
`integral_eq_tsum'` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`MeasureTheory.integral` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `MeasureTheory.Measure.restrict` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `SummationFilter.unconditional`	—	`integral_eq_tsum` `Equiv.tsum_eq` `tsum_congr` `MeasureTheory.MeasurePreserving.setIntegral_image_emb` `MeasureTheory.measurePreserving_vadd` `measurableEmbedding_const_vadd`
`integral_eq_tsum''` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`MeasureTheory.integral` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `MeasureTheory.Measure.restrict` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `SummationFilter.unconditional`	—	`integral_eq_tsum'` `Equiv.tsum_eq`
`integral_eq_tsum_of_ac` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `MeasureTheory.Measure.AbsolutelyContinuous` `MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`MeasureTheory.integral` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `MeasureTheory.Measure.restrict` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `SummationFilter.unconditional`	—	`MeasureTheory.integral_sum_measure` `sum_restrict_of_ac`
`lintegral_eq_tsum` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`MeasureTheory.lintegral` `tsum` `ENNReal` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `MeasureTheory.Measure.restrict` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `SummationFilter.unconditional`	—	`lintegral_eq_tsum_of_ac` `refl` `MeasureTheory.Measure.AbsolutelyContinuous.instRefl`
`lintegral_eq_tsum'` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`MeasureTheory.lintegral` `tsum` `ENNReal` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `MeasureTheory.Measure.restrict` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `SummationFilter.unconditional`	—	`lintegral_eq_tsum` `Equiv.tsum_eq` `tsum_congr` `MeasureTheory.MeasurePreserving.setLIntegral_comp_emb` `MeasureTheory.measurePreserving_vadd` `measurableEmbedding_const_vadd`
`lintegral_eq_tsum''` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`MeasureTheory.lintegral` `tsum` `ENNReal` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `MeasureTheory.Measure.restrict` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `SummationFilter.unconditional`	—	`lintegral_eq_tsum'` `Equiv.tsum_eq`
`lintegral_eq_tsum_of_ac` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `MeasureTheory.Measure.AbsolutelyContinuous`	`MeasureTheory.lintegral` `tsum` `ENNReal` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `MeasureTheory.Measure.restrict` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `SummationFilter.unconditional`	—	`MeasureTheory.lintegral_sum_measure` `sum_restrict_of_ac`
`measurePreserving_add_quotient_mk` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`MeasureTheory.MeasurePreserving` `AddAction.orbitRel` `Quotient.instMeasurableSpace` `MeasureTheory.Measure.restrict`	—	`measurable_quotient_mk'` `addProjection_respects_measure`
`measure_addFundamentalFrontier` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.addFundamentalFrontier` `instZeroENNReal`	—	`Set.inter_comm` `Set.iUnion₂_inter` `MeasureTheory.measure_iUnion_null_iff` `MeasureTheory.Measure.instOuterMeasureClass` `Prop.countable` `zero_vadd` `aedisjoint`
`measure_addFundamentalInterior` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.addFundamentalInterior`	—	`MeasureTheory.measure_diff_null'` `measure_addFundamentalFrontier`
`measure_eq` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike`	—	`MeasureTheory.setLIntegral_one` `setLIntegral_eq`
`measure_eq_card_smul_of_vadd_ae_eq_self` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `AddMonoid.toNSMul` `ESeminormedAddMonoid.toAddMonoid` `ENNReal.instTopologicalSpace` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `instENormedAddCommMonoidENNReal` `Nat.card` `Set.instInter`	—	`MeasureTheory.Measure.instOuterMeasureClass` `measure_eq_tsum` `MeasureTheory.ae_eq_set_inter` `MeasureTheory.ae_eq_refl` `MeasureTheory.measure_congr` `tsum_fintype` `SummationFilter.instLeAtTopUnconditional` `Finset.sum_const` `Nat.card_eq_fintype_card`
`measure_eq_tsum` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `Set.instInter` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `SummationFilter.unconditional`	—	`MeasureTheory.setLIntegral_one` `setLIntegral_eq_tsum'`
`measure_eq_tsum'` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `Set.instInter` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `SummationFilter.unconditional`	—	`measure_eq_tsum_of_ac` `MeasureTheory.Measure.AbsolutelyContinuous.rfl`
`measure_eq_tsum_of_ac` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `MeasureTheory.Measure.AbsolutelyContinuous`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `Set.instInter` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `SummationFilter.unconditional`	—	`MeasureTheory.Measure.AbsolutelyContinuous.trans` `LE.le.absolutelyContinuous` `MeasureTheory.Measure.restrict_le_self` `MeasureTheory.setLIntegral_one` `MeasureTheory.Measure.restrict_apply₀` `MeasureTheory.NullMeasurableSet.mono_ac` `nullMeasurableSet_vadd` `Set.inter_comm` `lintegral_eq_tsum_of_ac`
`measure_le_of_pairwise_disjoint` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `MeasureTheory.NullMeasurableSet` `Pairwise` `Function.onFun` `Set` `MeasureTheory.AEDisjoint` `Set.instInter` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike`	—	`measure_eq_tsum` `MeasureTheory.measure_iUnion₀` `MeasureTheory.NullMeasurableSet.inter` `MeasureTheory.NullMeasurableSet.vadd` `nullMeasurableSet` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Set.iUnion_subset` `Set.inter_subset_right`
`measure_ne_zero` 📖	—	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	—	`MeasureTheory.Measure.measure_univ_pos` `Mathlib.Tactic.Contrapose.contrapose₃` `not_lt` `MeasureTheory.measure_congr` `MeasureTheory.Measure.instOuterMeasureClass` `iUnion_vadd_ae_eq` `le_trans` `MeasureTheory.measure_iUnion_le` `MeasureTheory.measure_vadd` `tsum_zero` `le_refl`
`measure_set_eq` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `MeasurableSet` `Set.preimage` `HVAdd.hVAdd` `instHVAdd`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `Set.instInter`	—	`setLIntegral_eq` `Set.indicator_comp_right` `MeasureTheory.lintegral_indicator` `MeasureTheory.lintegral_const` `MeasureTheory.Measure.restrict_apply` `MeasurableSet.univ` `Set.univ_inter` `one_mul`
`measure_zero_of_invariant` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `DFunLike.coe` `MeasureTheory.Measure` `ENNReal` `MeasureTheory.Measure.instFunLike` `Set.instInter` `instZeroENNReal`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `instZeroENNReal`	—	`measure_eq_tsum` `tsum_zero`
`mk'` 📖	mathematical	`MeasureTheory.NullMeasurableSet` `ExistsUnique` `Set` `Set.instMembership` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`Filter.Eventually.of_forall` `MeasureTheory.Measure.instOuterMeasureClass` `ExistsUnique.exists` `Disjoint.aedisjoint` `Set.disjoint_left` `neg_injective` `ExistsUnique.unique` `Set.mem_vadd_set_iff_neg_vadd_mem`
`mk''` 📖	mathematical	`MeasureTheory.NullMeasurableSet` `Filter.Eventually` `Set` `Set.instMembership` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.AEDisjoint` `Set.vaddSet` `MeasureTheory.Measure.QuasiMeasurePreserving`	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.pairwise_aedisjoint_of_aedisjoint_forall_ne_zero`
`mk_of_measure_univ_le` 📖	mathematical	`MeasureTheory.NullMeasurableSet` `MeasureTheory.AEDisjoint` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `MeasureTheory.Measure.QuasiMeasurePreserving` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `Set.univ` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `SummationFilter.unconditional`	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`MeasureTheory.Measure.pairwise_aedisjoint_of_aedisjoint_forall_ne_zero` `neg_neg` `Set.preimage_vadd` `MeasureTheory.NullMeasurableSet.preimage` `Set.iUnion_vadd_eq_setOf_exists` `MeasureTheory.NullMeasurableSet.iUnion` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ae_iff_measure_eq` `le_antisymm` `MeasureTheory.measure_mono` `Set.subset_univ` `MeasureTheory.measure_iUnion₀`
`mono` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `MeasureTheory.Measure.AbsolutelyContinuous`	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`MeasureTheory.NullMeasurableSet.mono_ac` `nullMeasurableSet` `ae_covers` `Pairwise.mono` `aedisjoint`
`nullMeasurableSet` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain`	`MeasureTheory.NullMeasurableSet`	—	—
`nullMeasurableSet_vadd` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`MeasureTheory.NullMeasurableSet` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`MeasureTheory.NullMeasurableSet.vadd` `nullMeasurableSet`
`pairwise_aedisjoint_of_ac` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `MeasureTheory.Measure.AbsolutelyContinuous`	`Pairwise` `MeasureTheory.AEDisjoint` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`Pairwise.mono` `aedisjoint`
`preimage_of_equiv` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `MeasureTheory.Measure.QuasiMeasurePreserving` `Function.Bijective` `Function.Semiconj` `HVAdd.hVAdd` `instHVAdd`	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `Set.preimage`	—	`MeasureTheory.NullMeasurableSet.preimage` `nullMeasurableSet` `Filter.Eventually.mono` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.QuasiMeasurePreserving.ae` `ae_covers` `Set.mem_preimage` `CanLift.prf` `Equiv.instCanLiftForallCoeBijective` `EmbeddingLike.apply_eq_iff_eq` `EquivLike.toEmbeddingLike` `MeasureTheory.AEDisjoint.preimage` `aedisjoint` `Set.preimage_vadd_neg` `Set.preimage_preimage` `neg_neg` `Equiv.apply_symm_apply`
`restrict_restrict` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`MeasureTheory.Measure.restrict` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `Set.instInter`	—	`MeasureTheory.Measure.restrict_restrict₀` `MeasureTheory.NullMeasurableSet.mono` `nullMeasurableSet_vadd` `MeasureTheory.Measure.restrict_le_self`
`setIntegral_eq` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `HVAdd.hVAdd` `instHVAdd`	`MeasureTheory.integral` `MeasureTheory.Measure.restrict`	—	`integrableOn_iff` `setIntegral_eq_tsum` `Set.inter_comm` `setIntegral_eq_tsum'` `MeasureTheory.integral_undef`
`setIntegral_eq_tsum` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `MeasureTheory.IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`MeasureTheory.integral` `MeasureTheory.Measure.restrict` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Set` `Set.instInter` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `SummationFilter.unconditional`	—	`integral_eq_tsum_of_ac` `LE.le.absolutelyContinuous` `MeasureTheory.Measure.restrict_le_self` `restrict_restrict` `Set.inter_comm`
`setIntegral_eq_tsum'` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `MeasureTheory.IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`MeasureTheory.integral` `MeasureTheory.Measure.restrict` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Set` `Set.instInter` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `SummationFilter.unconditional`	—	`setIntegral_eq_tsum` `Equiv.tsum_eq` `Set.vadd_set_inter` `neg_vadd_vadd` `tsum_congr` `MeasureTheory.MeasurePreserving.setIntegral_image_emb` `MeasureTheory.measurePreserving_vadd` `measurableEmbedding_const_vadd`
`setLIntegral_eq` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `HVAdd.hVAdd` `instHVAdd`	`MeasureTheory.lintegral` `MeasureTheory.Measure.restrict`	—	`setLIntegral_eq_tsum` `Set.inter_comm` `setLIntegral_eq_tsum'`
`setLIntegral_eq_tsum` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`MeasureTheory.lintegral` `MeasureTheory.Measure.restrict` `tsum` `ENNReal` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `Set` `Set.instInter` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `SummationFilter.unconditional`	—	`lintegral_eq_tsum_of_ac` `LE.le.absolutelyContinuous` `MeasureTheory.Measure.restrict_le_self` `restrict_restrict` `Set.inter_comm`
`setLIntegral_eq_tsum'` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`MeasureTheory.lintegral` `MeasureTheory.Measure.restrict` `tsum` `ENNReal` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `Set` `Set.instInter` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `SummationFilter.unconditional`	—	`setLIntegral_eq_tsum` `Equiv.tsum_eq` `Set.vadd_set_inter` `neg_vadd_vadd` `tsum_congr` `MeasureTheory.MeasurePreserving.setLIntegral_comp_emb` `MeasureTheory.measurePreserving_vadd` `measurableEmbedding_const_vadd`
`sum_restrict` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`MeasureTheory.Measure.sum` `MeasureTheory.Measure.restrict` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`sum_restrict_of_ac` `refl` `MeasureTheory.Measure.AbsolutelyContinuous.instRefl`
`sum_restrict_of_ac` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `MeasureTheory.Measure.AbsolutelyContinuous`	`MeasureTheory.Measure.sum` `MeasureTheory.Measure.restrict` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`MeasureTheory.Measure.restrict_iUnion_ae` `Pairwise.mono` `aedisjoint` `MeasureTheory.NullMeasurableSet.mono_ac` `nullMeasurableSet_vadd` `MeasureTheory.Measure.restrict_congr_set` `iUnion_vadd_ae_eq` `MeasureTheory.Measure.restrict_univ`
`vadd` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet`	—	`image_of_equiv` `MeasureTheory.MeasurePreserving.quasiMeasurePreserving` `MeasureTheory.measurePreserving_vadd` `add_assoc` `add_neg_cancel_left` `add_neg_cancel` `add_zero` `neg_add_cancel_left` `neg_add_cancel` `vadd_vadd`
`vadd_of_comm` 📖	mathematical	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`MeasureTheory.IsAddFundamentalDomain` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet`	—	`image_of_equiv` `MeasureTheory.MeasurePreserving.quasiMeasurePreserving` `MeasureTheory.measurePreserving_vadd` `VAddCommClass.vadd_comm`

MeasureTheory.IsFundamentalDomain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_covers` 📖	mathematical	`MeasureTheory.IsFundamentalDomain`	`Filter.Eventually` `Set` `Set.instMembership` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	—
`aedisjoint` 📖	mathematical	`MeasureTheory.IsFundamentalDomain`	`Pairwise` `Function.onFun` `Set` `MeasureTheory.AEDisjoint` `Set.smulSet`	—	—
`aestronglyMeasurable_on_iff` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`MeasureTheory.AEStronglyMeasurable` `MeasureTheory.Measure.restrict`	—	`restrict_restrict` `sum_restrict_of_ac` `LE.le.absolutelyContinuous` `MeasureTheory.Measure.restrict_le_self` `Set.inter_comm` `Set.smul_set_inter` `smul_inv_smul` `Function.Surjective.forall` `inv_surjective` `inv_inv` `measurableEmbedding_const_smul` `Set.image_smul` `MeasureTheory.MeasurePreserving.aestronglyMeasurable_comp_iff` `MeasureTheory.MeasurePreserving.restrict_image_emb` `MeasureTheory.measurePreserving_smul`
`covolume_eq_volume` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`MeasureTheory.covolume` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike`	—	`MeasureTheory.HasFundamentalDomain.ExistsIsFundamentalDomain` `hasFundamentalDomain` `measure_eq`
`essSup_measure_restrict` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`essSup` `ENNReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `MeasureTheory.Measure.restrict`	—	`le_antisymm` `essSup_mono_measure'` `MeasureTheory.Measure.restrict_le_self` `essSup_eq_sInf` `sInf_le_sInf` `measure_zero_of_invariant` `Set.ext` `Set.mem_smul_set_iff_inv_smul_mem` `MeasureTheory.Measure.restrict_apply₀'` `nullMeasurableSet`
`exists_ne_one_smul_eq` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `MeasureTheory.NullMeasurableSet` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike`	`Set` `Set.instMembership` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_and_eq` `measure_le_of_pairwise_disjoint` `Pairwise.aedisjoint` `Disjoint.inf_right` `Disjoint.inf_left` `Set.disjoint_left` `inv_mul_eq_one` `SemigroupAction.mul_smul` `inv_smul_smul`
`fundamentalInterior` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `MeasureTheory.fundamentalInterior`	—	`MeasureTheory.NullMeasurableSet.fundamentalInterior` `nullMeasurableSet` `MeasureTheory.Measure.instOuterMeasureClass` `Set.setOf_forall` `Set.smul_set_union` `MeasureTheory.fundamentalFrontier_union_fundamentalInterior` `subset_refl` `Set.instReflSubset` `eq_bot_mono` `MeasureTheory.OuterMeasure.mono` `Set.compl_subset_compl` `Set.iUnion_inv_smul` `Set.iUnion_smul_eq_setOf_exists` `compl_sdiff` `himp_eq` `MeasureTheory.measure_union_null` `MeasureTheory.measure_iUnion_null` `MeasureTheory.measure_smul_null` `measure_fundamentalFrontier` `ae_covers` `Pairwise.mono` `MeasureTheory.pairwise_disjoint_fundamentalInterior` `Disjoint.aedisjoint`
`hasFiniteIntegral_on_iff` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`MeasureTheory.HasFiniteIntegral` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `MeasureTheory.Measure.restrict`	—	`setLIntegral_eq`
`hasFundamentalDomain` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`MeasureTheory.HasFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	—
`iUnion_smul_ae_eq` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `Set.iUnion` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Set.univ`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Filter.eventuallyEq_univ` `Filter.Eventually.mono` `ae_covers` `Set.mem_iUnion` `inv_smul_smul`
`image_of_equiv` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `MeasureTheory.Measure.QuasiMeasurePreserving` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `Function.Semiconj`	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Set.image` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`Equiv.image_eq_preimage_symm` `preimage_of_equiv` `Equiv.bijective` `Equiv.surjective` `Equiv.symm_apply_apply` `Equiv.apply_symm_apply`
`integrableOn_iff` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`MeasureTheory.IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`aestronglyMeasurable_on_iff` `PseudoEMetricSpace.pseudoMetrizableSpace` `hasFiniteIntegral_on_iff`
`integral_eq_tsum` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`MeasureTheory.integral` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `MeasureTheory.Measure.restrict` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `SummationFilter.unconditional`	—	`integral_eq_tsum_of_ac` `MeasureTheory.Measure.AbsolutelyContinuous.refl`
`integral_eq_tsum'` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`MeasureTheory.integral` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `MeasureTheory.Measure.restrict` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SummationFilter.unconditional`	—	`integral_eq_tsum` `Equiv.tsum_eq` `tsum_congr` `MeasureTheory.MeasurePreserving.setIntegral_image_emb` `MeasureTheory.measurePreserving_smul` `measurableEmbedding_const_smul`
`integral_eq_tsum''` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`MeasureTheory.integral` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `MeasureTheory.Measure.restrict` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `SummationFilter.unconditional`	—	`integral_eq_tsum'` `Equiv.tsum_eq`
`integral_eq_tsum_of_ac` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `MeasureTheory.Measure.AbsolutelyContinuous` `MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`MeasureTheory.integral` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `MeasureTheory.Measure.restrict` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `SummationFilter.unconditional`	—	`MeasureTheory.integral_sum_measure` `sum_restrict_of_ac`
`lintegral_eq_tsum` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`MeasureTheory.lintegral` `tsum` `ENNReal` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `MeasureTheory.Measure.restrict` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `SummationFilter.unconditional`	—	`lintegral_eq_tsum_of_ac` `refl` `MeasureTheory.Measure.AbsolutelyContinuous.instRefl`
`lintegral_eq_tsum'` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`MeasureTheory.lintegral` `tsum` `ENNReal` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `MeasureTheory.Measure.restrict` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SummationFilter.unconditional`	—	`lintegral_eq_tsum` `Equiv.tsum_eq` `tsum_congr` `MeasureTheory.MeasurePreserving.setLIntegral_comp_emb` `MeasureTheory.measurePreserving_smul` `measurableEmbedding_const_smul`
`lintegral_eq_tsum''` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`MeasureTheory.lintegral` `tsum` `ENNReal` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `MeasureTheory.Measure.restrict` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `SummationFilter.unconditional`	—	`lintegral_eq_tsum'` `Equiv.tsum_eq`
`lintegral_eq_tsum_of_ac` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `MeasureTheory.Measure.AbsolutelyContinuous`	`MeasureTheory.lintegral` `tsum` `ENNReal` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `MeasureTheory.Measure.restrict` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `SummationFilter.unconditional`	—	`MeasureTheory.lintegral_sum_measure` `sum_restrict_of_ac`
`measurePreserving_quotient_mk` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`MeasureTheory.MeasurePreserving` `MulAction.orbitRel` `Quotient.instMeasurableSpace` `MeasureTheory.Measure.restrict`	—	`measurable_quotient_mk'` `projection_respects_measure`
`measure_eq` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike`	—	`MeasureTheory.setLIntegral_one` `setLIntegral_eq`
`measure_eq_card_smul_of_smul_ae_eq_self` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `Set` `Set.smulSet`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `AddMonoid.toNSMul` `ESeminormedAddMonoid.toAddMonoid` `ENNReal.instTopologicalSpace` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `instENormedAddCommMonoidENNReal` `Nat.card` `Set.instInter`	—	`MeasureTheory.Measure.instOuterMeasureClass` `measure_eq_tsum` `MeasureTheory.ae_eq_set_inter` `MeasureTheory.ae_eq_refl` `MeasureTheory.measure_congr` `tsum_fintype` `SummationFilter.instLeAtTopUnconditional` `Finset.sum_const` `Nat.card_eq_fintype_card`
`measure_eq_tsum` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `Set.instInter` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `SummationFilter.unconditional`	—	`MeasureTheory.setLIntegral_one` `setLIntegral_eq_tsum'`
`measure_eq_tsum'` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `Set.instInter` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `SummationFilter.unconditional`	—	`measure_eq_tsum_of_ac` `MeasureTheory.Measure.AbsolutelyContinuous.rfl`
`measure_eq_tsum_of_ac` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `MeasureTheory.Measure.AbsolutelyContinuous`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `Set.instInter` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `SummationFilter.unconditional`	—	`MeasureTheory.Measure.AbsolutelyContinuous.trans` `LE.le.absolutelyContinuous` `MeasureTheory.Measure.restrict_le_self` `MeasureTheory.setLIntegral_one` `MeasureTheory.Measure.restrict_apply₀` `MeasureTheory.NullMeasurableSet.mono_ac` `nullMeasurableSet_smul` `Set.inter_comm` `lintegral_eq_tsum_of_ac`
`measure_fundamentalFrontier` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.fundamentalFrontier` `instZeroENNReal`	—	`Set.inter_comm` `Set.iUnion₂_inter` `MeasureTheory.Measure.instOuterMeasureClass` `Prop.countable` `one_smul` `aedisjoint`
`measure_fundamentalInterior` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.fundamentalInterior`	—	`MeasureTheory.measure_diff_null'` `measure_fundamentalFrontier`
`measure_le_of_pairwise_disjoint` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `MeasureTheory.NullMeasurableSet` `Pairwise` `Function.onFun` `Set` `MeasureTheory.AEDisjoint` `Set.instInter` `Set.smulSet`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike`	—	`measure_eq_tsum` `MeasureTheory.measure_iUnion₀` `MeasureTheory.NullMeasurableSet.inter` `MeasureTheory.NullMeasurableSet.smul` `nullMeasurableSet` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Set.iUnion_subset` `Set.inter_subset_right`
`measure_ne_zero` 📖	—	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	—	`MeasureTheory.Measure.measure_univ_pos` `Mathlib.Tactic.Contrapose.contrapose₃` `MeasureTheory.measure_congr` `MeasureTheory.Measure.instOuterMeasureClass` `iUnion_smul_ae_eq` `le_trans` `MeasureTheory.measure_iUnion_le` `MeasureTheory.measure_smul` `tsum_zero`
`measure_set_eq` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `MeasurableSet` `Set.preimage`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `Set.instInter`	—	`setLIntegral_eq` `Set.indicator_comp_right` `MeasureTheory.lintegral_indicator` `MeasureTheory.lintegral_const` `MeasureTheory.Measure.restrict_apply` `Set.univ_inter` `one_mul`
`measure_zero_of_invariant` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Set` `Set.smulSet` `DFunLike.coe` `MeasureTheory.Measure` `ENNReal` `MeasureTheory.Measure.instFunLike` `Set.instInter` `instZeroENNReal`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `instZeroENNReal`	—	`measure_eq_tsum` `tsum_zero`
`mk'` 📖	mathematical	`MeasureTheory.NullMeasurableSet` `ExistsUnique` `Set` `Set.instMembership` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`Filter.Eventually.of_forall` `MeasureTheory.Measure.instOuterMeasureClass` `ExistsUnique.exists` `Disjoint.aedisjoint` `Set.disjoint_left` `inv_injective` `ExistsUnique.unique` `Set.mem_smul_set_iff_inv_smul_mem`
`mk''` 📖	mathematical	`MeasureTheory.NullMeasurableSet` `Filter.Eventually` `Set` `Set.instMembership` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.AEDisjoint` `Set.smulSet` `MeasureTheory.Measure.QuasiMeasurePreserving`	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.pairwise_aedisjoint_of_aedisjoint_forall_ne_one`
`mk_of_measure_univ_le` 📖	mathematical	`MeasureTheory.NullMeasurableSet` `MeasureTheory.AEDisjoint` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `MeasureTheory.Measure.QuasiMeasurePreserving` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `Set.univ` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `SummationFilter.unconditional`	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`MeasureTheory.Measure.pairwise_aedisjoint_of_aedisjoint_forall_ne_one` `inv_inv` `Set.preimage_smul` `MeasureTheory.NullMeasurableSet.preimage` `Set.iUnion_smul_eq_setOf_exists` `MeasureTheory.NullMeasurableSet.iUnion` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ae_iff_measure_eq` `le_antisymm` `MeasureTheory.measure_mono` `Set.subset_univ` `MeasureTheory.measure_iUnion₀`
`mono` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `MeasureTheory.Measure.AbsolutelyContinuous`	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`MeasureTheory.NullMeasurableSet.mono_ac` `nullMeasurableSet` `ae_covers` `Pairwise.mono` `aedisjoint`
`nullMeasurableSet` 📖	mathematical	`MeasureTheory.IsFundamentalDomain`	`MeasureTheory.NullMeasurableSet`	—	—
`nullMeasurableSet_smul` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`MeasureTheory.NullMeasurableSet` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`MeasureTheory.NullMeasurableSet.smul` `nullMeasurableSet`
`pairwise_aedisjoint_of_ac` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `MeasureTheory.Measure.AbsolutelyContinuous`	`Pairwise` `MeasureTheory.AEDisjoint` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`Pairwise.mono` `aedisjoint`
`preimage_of_equiv` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `MeasureTheory.Measure.QuasiMeasurePreserving` `Function.Bijective` `Function.Semiconj`	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Set.preimage`	—	`MeasureTheory.NullMeasurableSet.preimage` `nullMeasurableSet` `Filter.Eventually.mono` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.QuasiMeasurePreserving.ae` `ae_covers` `Set.mem_preimage` `CanLift.prf` `Equiv.instCanLiftForallCoeBijective` `EquivLike.toEmbeddingLike` `MeasureTheory.AEDisjoint.preimage` `aedisjoint` `Set.preimage_preimage` `inv_inv` `Equiv.apply_symm_apply`
`projection_respects_measure` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`MeasureTheory.Measure.map` `MulAction.orbitRel` `Quotient.instMeasurableSpace` `MeasureTheory.Measure.restrict`	—	`MeasureTheory.QuotientMeasureEqMeasurePreimage.projection_respects_measure'`
`projection_respects_measure_apply` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `MeasurableSet` `MulAction.orbitRel` `Quotient.instMeasurableSpace`	`DFunLike.coe` `MeasureTheory.Measure` `MulAction.orbitRel` `Quotient.instMeasurableSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `Set.instInter` `Set.preimage`	—	`projection_respects_measure` `MeasureTheory.measure_map_restrict_apply`
`quotientMeasureEqMeasurePreimage` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `MeasureTheory.Measure.map` `MulAction.orbitRel` `Quotient.instMeasurableSpace` `MeasureTheory.Measure.restrict`	`MeasureTheory.QuotientMeasureEqMeasurePreimage`	—	`quotientMeasureEqMeasurePreimage_quotientMeasure`
`quotientMeasureEqMeasurePreimage_of_zero` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `instZeroENNReal`	`MeasureTheory.QuotientMeasureEqMeasurePreimage` `MeasureTheory.Measure` `MulAction.orbitRel` `Quotient.instMeasurableSpace` `MeasureTheory.Measure.instZero`	—	`quotientMeasureEqMeasurePreimage` `MeasureTheory.Measure.ext` `MeasureTheory.measure_map_restrict_apply` `MeasureTheory.measure_inter_null_of_null_right`
`quotientMeasureEqMeasurePreimage_quotientMeasure` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`MeasureTheory.QuotientMeasureEqMeasurePreimage` `MeasureTheory.Measure.map` `MulAction.orbitRel` `Quotient.instMeasurableSpace` `MeasureTheory.Measure.restrict`	—	`quotientMeasure_eq`
`quotientMeasure_eq` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`MeasureTheory.Measure.map` `MulAction.orbitRel` `Quotient.instMeasurableSpace` `MeasureTheory.Measure.restrict`	—	`MeasureTheory.Measure.ext` `MeasureTheory.measure_map_restrict_apply` `measure_set_eq` `measurableSet_quotient` `Set.ext`
`restrict_restrict` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`MeasureTheory.Measure.restrict` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Set.instInter`	—	`MeasureTheory.Measure.restrict_restrict₀` `MeasureTheory.NullMeasurableSet.mono` `nullMeasurableSet_smul` `MeasureTheory.Measure.restrict_le_self`
`setIntegral_eq` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`MeasureTheory.integral` `MeasureTheory.Measure.restrict`	—	`integrableOn_iff` `setIntegral_eq_tsum` `Set.inter_comm` `setIntegral_eq_tsum'` `MeasureTheory.integral_undef`
`setIntegral_eq_tsum` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `MeasureTheory.IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`MeasureTheory.integral` `MeasureTheory.Measure.restrict` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Set` `Set.instInter` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `SummationFilter.unconditional`	—	`integral_eq_tsum_of_ac` `LE.le.absolutelyContinuous` `MeasureTheory.Measure.restrict_le_self` `restrict_restrict` `Set.inter_comm`
`setIntegral_eq_tsum'` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `MeasureTheory.IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`MeasureTheory.integral` `MeasureTheory.Measure.restrict` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Set` `Set.instInter` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SummationFilter.unconditional`	—	`setIntegral_eq_tsum` `Equiv.tsum_eq` `Set.smul_set_inter` `inv_smul_smul` `tsum_congr` `MeasureTheory.MeasurePreserving.setIntegral_image_emb` `MeasureTheory.measurePreserving_smul` `measurableEmbedding_const_smul`
`setLIntegral_eq` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`MeasureTheory.lintegral` `MeasureTheory.Measure.restrict`	—	`setLIntegral_eq_tsum` `Set.inter_comm` `setLIntegral_eq_tsum'`
`setLIntegral_eq_tsum` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`MeasureTheory.lintegral` `MeasureTheory.Measure.restrict` `tsum` `ENNReal` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `Set` `Set.instInter` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `SummationFilter.unconditional`	—	`lintegral_eq_tsum_of_ac` `LE.le.absolutelyContinuous` `MeasureTheory.Measure.restrict_le_self` `restrict_restrict` `Set.inter_comm`
`setLIntegral_eq_tsum'` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`MeasureTheory.lintegral` `MeasureTheory.Measure.restrict` `tsum` `ENNReal` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `Set` `Set.instInter` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SummationFilter.unconditional`	—	`setLIntegral_eq_tsum` `Equiv.tsum_eq` `Set.smul_set_inter` `inv_smul_smul` `tsum_congr` `MeasureTheory.MeasurePreserving.setLIntegral_comp_emb` `MeasureTheory.measurePreserving_smul` `measurableEmbedding_const_smul`
`smul` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Set` `Set.smulSet`	—	`image_of_equiv` `MeasureTheory.MeasurePreserving.quasiMeasurePreserving` `MeasureTheory.measurePreserving_smul` `mul_assoc` `mul_inv_cancel_left` `mul_inv_cancel` `mul_one` `inv_mul_cancel_left` `inv_mul_cancel` `smul_smul`
`smul_of_comm` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Set` `Set.smulSet`	—	`image_of_equiv` `MeasureTheory.MeasurePreserving.quasiMeasurePreserving` `MeasureTheory.measurePreserving_smul` `SMulCommClass.smul_comm`
`sum_restrict` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`MeasureTheory.Measure.sum` `MeasureTheory.Measure.restrict` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`sum_restrict_of_ac` `refl` `MeasureTheory.Measure.AbsolutelyContinuous.instRefl`
`sum_restrict_of_ac` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `MeasureTheory.Measure.AbsolutelyContinuous`	`MeasureTheory.Measure.sum` `MeasureTheory.Measure.restrict` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`MeasureTheory.Measure.restrict_iUnion_ae` `Pairwise.mono` `aedisjoint` `MeasureTheory.NullMeasurableSet.mono_ac` `nullMeasurableSet_smul` `MeasureTheory.Measure.restrict_congr_set` `iUnion_smul_ae_eq` `MeasureTheory.Measure.restrict_univ`

MeasureTheory.NullMeasurableSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addFundamentalFrontier` 📖	mathematical	`MeasureTheory.NullMeasurableSet`	`MeasureTheory.NullMeasurableSet` `MeasureTheory.addFundamentalFrontier`	—	`inter` `iUnion` `Prop.countable` `vadd`
`addFundamentalInterior` 📖	mathematical	`MeasureTheory.NullMeasurableSet`	`MeasureTheory.NullMeasurableSet` `MeasureTheory.addFundamentalInterior`	—	`diff` `iUnion` `Prop.countable` `vadd`
`fundamentalFrontier` 📖	mathematical	`MeasureTheory.NullMeasurableSet`	`MeasureTheory.NullMeasurableSet` `MeasureTheory.fundamentalFrontier`	—	`inter` `iUnion` `Prop.countable` `smul`
`fundamentalInterior` 📖	mathematical	`MeasureTheory.NullMeasurableSet`	`MeasureTheory.NullMeasurableSet` `MeasureTheory.fundamentalInterior`	—	`diff` `iUnion` `Prop.countable` `smul`

MeasureTheory.QuotientMeasureEqMeasurePreimage

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`covolume_ne_top` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `MeasureTheory.covolume` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Top.top` `instTopENNReal`	—	`MeasureTheory.HasFundamentalDomain.ExistsIsFundamentalDomain` `MeasureTheory.IsFiniteMeasure.measure_univ_lt_top` `MeasureTheory.IsFundamentalDomain.covolume_eq_volume` `Set.univ_inter` `MeasureTheory.IsFundamentalDomain.projection_respects_measure_apply` `MeasurableSet.univ`
`isFiniteMeasure_quotient` 📖	mathematical	—	`MeasureTheory.IsFiniteMeasure` `MulAction.orbitRel` `Quotient.instMeasurableSpace`	—	`MeasureTheory.HasFundamentalDomain.ExistsIsFundamentalDomain` `MeasureTheory.IsFundamentalDomain.projection_respects_measure` `MeasureTheory.IsFundamentalDomain.covolume_eq_volume` `Ne.lt_top` `MeasureTheory.Measure.isFiniteMeasure_map` `MeasureTheory.Restrict.isFiniteMeasure`
`projection_respects_measure'` 📖	mathematical	`MeasureTheory.IsFundamentalDomain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`MeasureTheory.Measure.map` `MulAction.orbitRel` `Quotient.instMeasurableSpace` `MeasureTheory.Measure.restrict`	—	—
`sigmaFiniteQuotient` 📖	mathematical	—	`MeasureTheory.SigmaFinite` `MulAction.orbitRel` `Quotient.instMeasurableSpace`	—	`MeasureTheory.sigmaFinite_iff` `MulAction.quotient_preimage_image_eq_union_mul` `measurableSet_quotient` `MeasurableSet.iUnion` `MeasurableSet.const_smul` `MeasureTheory.IsFundamentalDomain.projection_respects_measure_apply` `Set.iUnion_inter` `lt_of_le_of_lt` `MeasureTheory.IsFundamentalDomain.measure_eq_tsum` `MeasureTheory.measure_iUnion_le` `MeasureTheory.Measure.instOuterMeasureClass` `Set.image_iUnion` `Set.image_univ_of_surjective` `Quotient.mk'_surjective`
`unique` 📖	—	—	—	—	`MeasureTheory.HasFundamentalDomain.ExistsIsFundamentalDomain` `MeasureTheory.IsFundamentalDomain.projection_respects_measure`

---

← Back to Index