Pi

📁 Source: Mathlib/MeasureTheory/Constructions/Pi.lean

Statistics

Metric	Count
Definitions `pi`, `pi`, `pi'`, `tprod`, `pi`, `pi`, `piPremeasure`	7
Theorems `pi`, `volume_pi`, `ae_eq_pi`, `ae_eq_set_pi`, `ae_eval_ne`, `ae_le_pi`, `ae_le_set_pi`, `ae_pi_le_pi`, `instIsAddHaarMeasureForallVolumeOfMeasurableAddOfSigmaFinite`, `instIsAddLeftInvariantForallVolumeOfMeasurableAddOfSigmaFinite`, `instIsAddRightInvariantForallVolumeOfMeasurableAddOfSigmaFinite`, `instIsFiniteMeasureForallVolume`, `instIsFiniteMeasureOnCompactsForallVolumeOfSigmaFinite`, `instIsHaarMeasureForallVolumeOfMeasurableMulOfSigmaFinite`, `instIsInvInvariantForallVolumeOfMeasurableInvOfSigmaFinite`, `instIsLocallyFiniteMeasureForallVolumeOfSigmaFinite`, `instIsMulLeftInvariantForallVolumeOfMeasurableMulOfSigmaFinite`, `instIsMulRightInvariantForallVolumeOfMeasurableMulOfSigmaFinite`, `instIsNegInvariantForallVolumeOfMeasurableNegOfSigmaFinite`, `instIsOpenPosMeasureForallVolumeOfSigmaFinite`, `instIsProbabilityMeasureForallVolume`, `instNoAtomsForallVolumeOfNonemptyOfSigmaFinite`, `instSigmaFiniteForallVolume`, `pi'_eq_pi`, `pi'_pi`, `instIsFiniteMeasure`, `instIsProbabilityMeasure`, `isAddHaarMeasure`, `isAddLeftInvariant`, `isAddRightInvariant`, `isFiniteMeasureOnCompacts`, `isHaarMeasure`, `isInvInvariant`, `isLocallyFiniteMeasure`, `isMulLeftInvariant`, `isMulRightInvariant`, `isNegInvariant`, `isOpenPosMeasure`, `sigmaFinite`, `pi_Ico_ae_eq_pi_Icc`, `pi_Iio_ae_eq_pi_Iic`, `pi_Ioc_ae_eq_pi_Icc`, `pi_Ioi_ae_eq_pi_Ici`, `pi_Ioo_ae_eq_pi_Icc`, `pi_Ioo_ae_eq_pi_Ioc`, `pi_ball`, `pi_caratheodory`, `pi_closedBall`, `pi_def`, `pi_empty_univ`, `pi_eq`, `pi_eq_generateFrom`, `pi_eval_preimage_null`, `pi_hyperplane`, `pi_map_eval`, `pi_map_pi`, `pi_map_piCongrLeft`, `pi_map_piOptionEquivProd`, `pi_noAtoms`, `pi_noAtoms'`, `pi_of_empty`, `pi_pi`, `pi_pi_aux`, `pi_singleton`, `pi_univ`, `quasiMeasurePreserving_eval`, `restrict_pi_pi`, `sigmaFinite_tprod`, `tendsto_eval_ae_ae`, `tprod_cons`, `tprod_nil`, `tprod_tprod`, `univ_pi_Ico_ae_eq_Icc`, `univ_pi_Iio_ae_eq_Iic`, `univ_pi_Ioc_ae_eq_Icc`, `univ_pi_Ioi_ae_eq_Ici`, `univ_pi_Ioo_ae_eq_Icc`, `volume_pi_eq_dirac`, `le_pi`, `pi_pi_le`, `isAddLeftInvariant_volume`, `isInvInvariant_volume`, `isMulLeftInvariant_volume`, `isNegInvariant_volume`, `measurePreserving_arrowCongr'`, `measurePreserving_arrowProdEquivProdArrow`, `measurePreserving_eval`, `measurePreserving_finTwoArrow`, `measurePreserving_finTwoArrow_vec`, `measurePreserving_funUnique`, `measurePreserving_pi`, `measurePreserving_piCongrLeft`, `measurePreserving_piEquivPiSubtypeProd`, `measurePreserving_piFinSuccAbove`, `measurePreserving_piFinTwo`, `measurePreserving_piFinsetUnion`, `measurePreserving_piUnique`, `measurePreserving_pi_empty`, `measurePreserving_sumPiEquivProdPi`, `measurePreserving_sumPiEquivProdPi_symm`, `piPremeasure_pi`, `piPremeasure_pi'`, `piPremeasure_pi_eval`, `piPremeasure_pi_mono`, `volume_measurePreserving_arrowProdEquivProdArrow`, `volume_measurePreserving_piCongrLeft`, `volume_measurePreserving_sumPiEquivProdPi`, `volume_measurePreserving_sumPiEquivProdPi_symm`, `volume_pi`, `volume_pi_ball`, `volume_pi_closedBall`, `volume_pi_pi`, `volume_preserving_arrowCongr'`, `volume_preserving_finTwoArrow`, `volume_preserving_funUnique`, `volume_preserving_pi`, `volume_preserving_piEquivPiSubtypeProd`, `volume_preserving_piFinSuccAbove`, `volume_preserving_piFinTwo`, `volume_preserving_piFinsetUnion`, `volume_preserving_piUnique`, `volume_preserving_pi_empty`	122
Total	129

IsUnifLocDoublingMeasure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pi` 📖	mathematical	`MeasureTheory.SigmaFinite` `IsUnifLocDoublingMeasure`	`pseudoMetricSpacePi` `MeasurableSpace.pi` `MeasureTheory.Measure.pi`	—	`Nat.instAtLeastTwoHAddOfNat` `Filter.mp_mem` `eventually_mem_nhdsWithin` `Filter.eventually_all` `Finite.of_fintype` `eventually_measure_le_doublingConstant_mul` `Filter.univ_mem'` `closedBall_pi` `le_of_lt` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `MeasureTheory.Measure.pi_pi` `ENNReal.coe_finset_prod` `Finset.prod_congr` `Finset.prod_mul_distrib` `Fintype.prod_mono'` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid`

MeasureTheory

Definitions

Name	Category	Theorems
`piPremeasure` 📖	CompOp	4 math math: `piPremeasure_pi_mono`, `piPremeasure_pi'`, `piPremeasure_pi`, `piPremeasure_pi_eval`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`measurePreserving_arrowCongr'` 📖	mathematical	`SigmaFinite` `MeasurePreserving` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `Equiv` `Equiv.instEquivLike`	`MeasurableSpace.pi` `MeasurableEquiv.arrowCongr'` `Measure.pi`	—	`Equiv.symm_apply_apply` `MeasurePreserving.comp` `measurePreserving_piCongrLeft` `measurePreserving_pi`
`measurePreserving_arrowProdEquivProdArrow` 📖	mathematical	`SigmaFinite`	`MeasurePreserving` `MeasurableSpace.pi` `Prod.instMeasurableSpace` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.arrowProdEquivProdArrow` `Measure.pi` `Measure.prod`	—	`MeasurableEquiv.measurable` `Measure.FiniteSpanningSetsIn.ext` `generateFrom_eq_prod` `generateFrom_pi` `Finite.of_fintype` `Measure.FiniteSpanningSetsIn.isCountablySpanning` `IsPiSystem.prod` `isPiSystem_pi` `MeasurableEquiv.map_apply` `MeasurableEquiv.arrowProdEquivProdArrow.eq_1` `Set.ext` `Measure.pi_pi` `Measure.prod.instSigmaFinite` `Measure.prod_prod` `instSFiniteOfSigmaFinite` `Measure.pi.sigmaFinite` `Finset.prod_congr` `Finset.prod_mul_distrib`
`measurePreserving_eval` 📖	mathematical	`IsProbabilityMeasure`	`MeasurePreserving` `MeasurableSpace.pi` `Function.eval` `Measure.pi`	—	`measurable_pi_apply` `IsScalarTower.right` `Measure.pi_map_eval` `IsFiniteMeasure.toSigmaFinite` `IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `Finset.prod_eq_one` `IsProbabilityMeasure.measure_univ` `one_smul`
`measurePreserving_finTwoArrow` 📖	mathematical	—	`MeasurePreserving` `MeasurableSpace.pi` `Prod.instMeasurableSpace` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.finTwoArrow` `Measure.pi` `Fin.fintype` `Measure.prod`	—	`Matrix.vec_single_eq_const` `Matrix.vecCons_const` `measurePreserving_finTwoArrow_vec`
`measurePreserving_finTwoArrow_vec` 📖	mathematical	—	`MeasurePreserving` `MeasurableSpace.pi` `Prod.instMeasurableSpace` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.finTwoArrow` `Measure.pi` `Fin.fintype` `Matrix.vecCons` `Measure` `Matrix.vecEmpty` `Measure.prod`	—	`measurePreserving_piFinTwo`
`measurePreserving_funUnique` 📖	mathematical	—	`MeasurePreserving` `MeasurableSpace.pi` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.funUnique` `Measure.pi` `Unique.fintype`	—	`measurePreserving_piUnique`
`measurePreserving_pi` 📖	mathematical	`SigmaFinite` `MeasurePreserving`	`MeasurableSpace.pi` `Measure.pi`	—	`measurable_pi_iff` `Measurable.comp` `MeasurePreserving.measurable` `measurable_pi_apply` `MeasurePreserving.map_eq` `Measure.pi_map_pi` `MeasurePreserving.aemeasurable`
`measurePreserving_piCongrLeft` 📖	mathematical	`SigmaFinite`	`MeasurePreserving` `MeasurableSpace.pi` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `MeasurableEquiv` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.piCongrLeft` `Measure.pi`	—	`MeasurableEquiv.measurable` `Measure.pi_eq` `MeasurableEquiv.map_apply` `MeasurableEquiv.coe_piCongrLeft` `Equiv.piCongrLeft_preimage_univ_pi` `Measure.pi_pi` `Equiv.prod_comp`
`measurePreserving_piEquivPiSubtypeProd` 📖	mathematical	`SigmaFinite`	`MeasurePreserving` `MeasurableSpace.pi` `Prod.instMeasurableSpace` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.piEquivPiSubtypeProd` `Measure.pi` `Measure.prod` `Subtype.fintype`	—	`MeasurePreserving.symm` `MeasurableEquiv.measurable` `Measure.pi_eq` `Equiv.preimage_piEquivPiSubtypeProd_symm_pi` `MeasurableEquiv.map_apply` `Measure.prod_prod` `instSFiniteOfSigmaFinite` `Measure.pi.sigmaFinite` `Measure.pi_pi` `Fintype.prod_subtype_mul_prod_subtype`
`measurePreserving_piFinSuccAbove` 📖	mathematical	`SigmaFinite`	`MeasurePreserving` `MeasurableSpace.pi` `Prod.instMeasurableSpace` `Fin.succAbove` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.piFinSuccAbove` `Measure.pi` `Fin.fintype` `Measure.prod`	—	`MeasurePreserving.symm` `MeasurableEquiv.measurable` `Measure.pi_eq` `MeasurableEquiv.map_apply` `Fin.prod_univ_succAbove` `Measure.pi_pi` `Measure.prod_prod` `instSFiniteOfSigmaFinite` `Measure.pi.sigmaFinite` `Set.ext` `Fin.forall_iff_succAbove` `Fin.insertNth_apply_same` `Fin.insertNth_apply_succAbove`
`measurePreserving_piFinTwo` 📖	mathematical	`SigmaFinite`	`MeasurePreserving` `MeasurableSpace.pi` `Prod.instMeasurableSpace` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.piFinTwo` `Measure.pi` `Fin.fintype` `Measure.prod`	—	`MeasurableEquiv.measurable` `Measure.prod_eq` `MeasurableEquiv.map_apply` `MeasurableEquiv.piFinTwo_apply` `Fin.preimage_apply_01_prod` `Measure.pi_pi` `Fin.prod_univ_two`
`measurePreserving_piFinsetUnion` 📖	mathematical	`Disjoint` `Finset` `Finset.partialOrder` `Finset.instOrderBot` `SigmaFinite`	`MeasurePreserving` `Prod.instMeasurableSpace` `MeasurableSpace.pi` `SetLike.instMembership` `Finset.instSetLike` `Finset.instUnion` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.piFinsetUnion` `Measure.prod` `Measure.pi` `Finset.Subtype.fintype`	—	`MeasurePreserving.comp` `measurePreserving_piCongrLeft` `measurePreserving_sumPiEquivProdPi_symm`
`measurePreserving_piUnique` 📖	mathematical	—	`MeasurePreserving` `Unique.instInhabited` `MeasurableSpace.pi` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.piUnique` `Measure.pi`	—	`MeasurableEquiv.measurable` `piPremeasure.eq_1` `Fintype.prod_unique` `MeasurableEquiv.map_apply` `Measure.coe_toOuterMeasure` `Equiv.image_eq_preimage_symm` `Measure.pi_caratheodory` `Measure.pi_def` `OuterMeasure.toMeasure.congr_simp` `OuterMeasure.boundedBy_eq_self` `toOuterMeasure_toMeasure` `MeasurableEquiv.map_map_symm`
`measurePreserving_pi_empty` 📖	mathematical	—	`MeasurePreserving` `MeasurableSpace.pi` `PUnit.instMeasurableSpace` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.ofUniqueOfUnique` `Pi.uniqueOfIsEmpty` `PUnit.instUnique` `Measure.pi` `Measure.dirac`	—	`MeasurableEquiv.measurable` `Measure.pi_of_empty` `Measure.map_dirac`
`measurePreserving_sumPiEquivProdPi` 📖	mathematical	`SigmaFinite`	`MeasurePreserving` `MeasurableSpace.pi` `Prod.instMeasurableSpace` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.sumPiEquivProdPi` `Measure.pi` `instFintypeSum` `Measure.prod`	—	`MeasurePreserving.symm` `measurePreserving_sumPiEquivProdPi_symm`
`measurePreserving_sumPiEquivProdPi_symm` 📖	mathematical	`SigmaFinite`	`MeasurePreserving` `Prod.instMeasurableSpace` `MeasurableSpace.pi` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.symm` `MeasurableEquiv.sumPiEquivProdPi` `Measure.prod` `Measure.pi` `instFintypeSum`	—	`MeasurableEquiv.measurable` `Measure.pi_eq` `MeasurableEquiv.map_apply` `MeasurableEquiv.coe_sumPiEquivProdPi_symm` `Equiv.sumPiEquivProdPi_symm_preimage_univ_pi` `Measure.prod_prod` `instSFiniteOfSigmaFinite` `Measure.pi.sigmaFinite` `Measure.pi_pi` `Fintype.prod_sum_type`
`piPremeasure_pi` 📖	mathematical	`Set.Nonempty` `Set.pi` `Set.univ`	`piPremeasure` `Finset.prod` `ENNReal` `CommSemiring.toCommMonoid` `ENNReal.instCommSemiring` `Finset.univ` `DFunLike.coe` `OuterMeasure` `Set` `OuterMeasure.instFunLikeSetENNReal`	—	`Finset.prod_congr` `Set.image_congr` `Set.eval_image_univ_pi`
`piPremeasure_pi'` 📖	mathematical	—	`piPremeasure` `Set.pi` `Set.univ` `Finset.prod` `ENNReal` `CommSemiring.toCommMonoid` `ENNReal.instCommSemiring` `Finset.univ` `DFunLike.coe` `OuterMeasure` `Set` `OuterMeasure.instFunLikeSetENNReal`	—	`isEmpty_or_nonempty` `Finset.prod_congr` `Finset.univ_eq_empty` `Set.image_congr` `Set.eq_empty_or_nonempty` `Set.univ_pi_eq_empty_iff` `measure_empty` `OuterMeasure.instOuterMeasureClass` `Set.image_empty` `Finset.prod_const` `zero_pow` `Fintype.card_ne_zero` `ENNReal.instNoZeroDivisors` `Set.eval_image_univ_pi`
`piPremeasure_pi_eval` 📖	mathematical	—	`piPremeasure` `Set.pi` `Set.univ` `Set.image` `Function.eval`	—	`Set.image_congr` `piPremeasure_pi'`
`piPremeasure_pi_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `piPremeasure`	—	`Finset.prod_le_prod'` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `measure_mono` `OuterMeasure.instOuterMeasureClass` `Set.image_mono`
`volume_measurePreserving_arrowProdEquivProdArrow` 📖	mathematical	—	`MeasurePreserving` `MeasurableSpace.pi` `Prod.instMeasurableSpace` `MeasureSpace.toMeasurableSpace` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.arrowProdEquivProdArrow` `MeasureSpace.volume` `MeasureSpace.pi` `Measure.prod.measureSpace`	—	`measurePreserving_arrowProdEquivProdArrow`
`volume_measurePreserving_piCongrLeft` 📖	mathematical	`SigmaFinite` `MeasureSpace.toMeasurableSpace` `MeasureSpace.volume`	`MeasurePreserving` `MeasureSpace.pi` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `MeasurableEquiv` `MeasurableSpace.pi` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.piCongrLeft`	—	`measurePreserving_piCongrLeft`
`volume_measurePreserving_sumPiEquivProdPi` 📖	mathematical	`SigmaFinite` `MeasureSpace.toMeasurableSpace` `MeasureSpace.volume`	`MeasurePreserving` `MeasureSpace.pi` `instFintypeSum` `Measure.prod.measureSpace` `DFunLike.coe` `MeasurableEquiv` `MeasurableSpace.pi` `Prod.instMeasurableSpace` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.sumPiEquivProdPi`	—	`measurePreserving_sumPiEquivProdPi`
`volume_measurePreserving_sumPiEquivProdPi_symm` 📖	mathematical	`SigmaFinite` `MeasureSpace.toMeasurableSpace` `MeasureSpace.volume`	`MeasurePreserving` `Measure.prod.measureSpace` `MeasureSpace.pi` `instFintypeSum` `DFunLike.coe` `MeasurableEquiv` `Prod.instMeasurableSpace` `MeasurableSpace.pi` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.symm` `MeasurableEquiv.sumPiEquivProdPi`	—	`measurePreserving_sumPiEquivProdPi_symm`
`volume_pi` 📖	mathematical	—	`MeasureSpace.volume` `MeasureSpace.pi` `Measure.pi` `MeasureSpace.toMeasurableSpace`	—	—
`volume_pi_ball` 📖	mathematical	`SigmaFinite` `MeasureSpace.toMeasurableSpace` `MeasureSpace.volume` `Real` `Real.instLT` `Real.instZero`	`DFunLike.coe` `Measure` `MeasureSpace.pi` `Set` `ENNReal` `Measure.instFunLike` `Metric.ball` `pseudoMetricSpacePi` `MetricSpace.toPseudoMetricSpace` `Finset.prod` `CommSemiring.toCommMonoid` `ENNReal.instCommSemiring` `Finset.univ`	—	`Measure.pi_ball`
`volume_pi_closedBall` 📖	mathematical	`SigmaFinite` `MeasureSpace.toMeasurableSpace` `MeasureSpace.volume` `Real` `Real.instLE` `Real.instZero`	`DFunLike.coe` `Measure` `MeasureSpace.pi` `Set` `ENNReal` `Measure.instFunLike` `Metric.closedBall` `pseudoMetricSpacePi` `MetricSpace.toPseudoMetricSpace` `Finset.prod` `CommSemiring.toCommMonoid` `ENNReal.instCommSemiring` `Finset.univ`	—	`Measure.pi_closedBall`
`volume_pi_pi` 📖	mathematical	`SigmaFinite` `MeasureSpace.toMeasurableSpace` `MeasureSpace.volume`	`DFunLike.coe` `Measure` `MeasureSpace.pi` `Set` `ENNReal` `Measure.instFunLike` `Set.pi` `Set.univ` `Finset.prod` `CommSemiring.toCommMonoid` `ENNReal.instCommSemiring` `Finset.univ`	—	`Measure.pi_pi`
`volume_preserving_arrowCongr'` 📖	mathematical	`MeasurePreserving` `MeasureSpace.toMeasurableSpace` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasureSpace.volume`	`MeasurableSpace.pi` `MeasurableEquiv.arrowCongr'` `MeasureSpace.pi`	—	`measurePreserving_arrowCongr'`
`volume_preserving_finTwoArrow` 📖	mathematical	—	`MeasurePreserving` `MeasureSpace.toMeasurableSpace` `MeasureSpace.pi` `Fin.fintype` `Measure.prod.measureSpace` `DFunLike.coe` `MeasurableEquiv` `MeasurableSpace.pi` `Prod.instMeasurableSpace` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.finTwoArrow` `MeasureSpace.volume`	—	`measurePreserving_finTwoArrow`
`volume_preserving_funUnique` 📖	mathematical	—	`MeasurePreserving` `MeasureSpace.toMeasurableSpace` `MeasureSpace.pi` `Unique.fintype` `DFunLike.coe` `MeasurableEquiv` `MeasurableSpace.pi` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.funUnique` `MeasureSpace.volume`	—	`measurePreserving_funUnique`
`volume_preserving_pi` 📖	mathematical	`SigmaFinite` `MeasureSpace.toMeasurableSpace` `MeasureSpace.volume` `MeasurePreserving`	`MeasurableSpace.pi` `MeasureSpace.pi`	—	`measurePreserving_pi`
`volume_preserving_piEquivPiSubtypeProd` 📖	mathematical	`SigmaFinite` `MeasureSpace.toMeasurableSpace` `MeasureSpace.volume`	`MeasurePreserving` `MeasurableSpace.pi` `Prod.instMeasurableSpace` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.piEquivPiSubtypeProd` `MeasureSpace.pi` `Measure.prod.measureSpace` `Subtype.fintype`	—	`measurePreserving_piEquivPiSubtypeProd`
`volume_preserving_piFinSuccAbove` 📖	mathematical	`SigmaFinite` `MeasureSpace.toMeasurableSpace` `MeasureSpace.volume`	`MeasurePreserving` `MeasurableSpace.pi` `Prod.instMeasurableSpace` `Fin.succAbove` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.piFinSuccAbove` `MeasureSpace.pi` `Fin.fintype` `Measure.prod.measureSpace`	—	`measurePreserving_piFinSuccAbove`
`volume_preserving_piFinTwo` 📖	mathematical	`SigmaFinite` `MeasureSpace.toMeasurableSpace` `MeasureSpace.volume`	`MeasurePreserving` `MeasureSpace.pi` `Fin.fintype` `Measure.prod.measureSpace` `DFunLike.coe` `MeasurableEquiv` `MeasurableSpace.pi` `Prod.instMeasurableSpace` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.piFinTwo`	—	`measurePreserving_piFinTwo`
`volume_preserving_piFinsetUnion` 📖	mathematical	`Disjoint` `Finset` `Finset.partialOrder` `Finset.instOrderBot` `SigmaFinite` `MeasureSpace.toMeasurableSpace` `MeasureSpace.volume`	`MeasurePreserving` `Measure.prod.measureSpace` `MeasureSpace.pi` `SetLike.instMembership` `Finset.instSetLike` `Finset.Subtype.fintype` `Finset.instUnion` `DFunLike.coe` `MeasurableEquiv` `Prod.instMeasurableSpace` `MeasurableSpace.pi` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.piFinsetUnion`	—	`measurePreserving_piFinsetUnion`
`volume_preserving_piUnique` 📖	mathematical	—	`MeasurePreserving` `Unique.instInhabited` `MeasureSpace.toMeasurableSpace` `MeasureSpace.pi` `DFunLike.coe` `MeasurableEquiv` `MeasurableSpace.pi` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.piUnique` `MeasureSpace.volume`	—	`measurePreserving_piUnique`
`volume_preserving_pi_empty` 📖	mathematical	—	`MeasurePreserving` `MeasureSpace.toMeasurableSpace` `MeasureSpace.pi` `Measure.instMeasureSpacePUnit` `DFunLike.coe` `MeasurableEquiv` `MeasurableSpace.pi` `PUnit.instMeasurableSpace` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.ofUniqueOfUnique` `Pi.uniqueOfIsEmpty` `PUnit.instUnique` `MeasureSpace.volume`	—	`measurePreserving_pi_empty`

MeasureTheory.Measure

Definitions

Name	Category	Theorems
`pi` 📖	CompOp	113 math math: `univ_pi_Ioc_ae_eq_Icc`, `MeasureTheory.Integrable.fin_nat_prod`, `MeasureTheory.lmarginal_univ`, `MeasureTheory.volume_pi`, `MeasureTheory.measurePreserving_funUnique`, `pi_Ioc_ae_eq_pi_Icc`, `MeasureTheory.integral_fintype_prod_eq_prod`, `ae_le_set_pi`, `pi_map_piCongrLeft`, `pi.isInvInvariant`, `MeasureTheory.lintegral_prod_lintegral_pow_le`, `MeasureTheory.lintegral_le_of_lmarginal_le`, `pi_of_empty`, `pi_eval_preimage_null`, `pi.sigmaFinite`, `MeasureTheory.integral_infinitePi_of_piFinset`, `MeasureTheory.measurePreserving_pi`, `MeasureTheory.lintegral_restrict_infinitePi`, `pi_hyperplane`, `univ_pi_Ioo_ae_eq_Icc`, `isProjectiveLimit_infinitePi`, `MeasureTheory.integral_fintype_prod_eq_pow`, `pi_noAtoms`, `MeasureTheory.measurePreserving_finTwoArrow_vec`, `MeasureTheory.piContent_cylinder`, `MeasureTheory.integrable_comp_eval`, `MeasureTheory.charFunDual_pi'`, `pi_pi_aux`, `MeasureTheory.lintegral_eq_lmarginal_univ`, `pi_eq`, `ProbabilityTheory.iIndepFun_pi`, `map_piSingleton`, `MeasureTheory.integral_comp_eval`, `pi_prod_map_IocProdIoc`, `MeasureTheory.lintegral_mul_prod_lintegral_pow_le`, `MeasureTheory.isProjectiveMeasureFamily_pi`, `pi.isLocallyFiniteMeasure`, `MeasureTheory.measurePreserving_eval`, `pi_ball`, `MeasureTheory.measurePreserving_piCongrLeft`, `MeasureTheory.measurePreserving_arrowCongr'`, `pi.isHaarMeasure`, `MeasureTheory.measurePreserving_arrowProdEquivProdArrow`, `pi_map_eval`, `restrict_pi_pi`, `MeasureTheory.charFun_pi`, `pi_Ico_ae_eq_pi_Icc`, `pi.isAddRightInvariant`, `pi_singleton`, `MeasureTheory.Integrable.fintype_prod_dep`, `MeasureTheory.piContent_eq_measure_pi`, `pi'_eq_pi`, `MeasureTheory.measurePreserving_piFinTwo`, `pi_prod_map_IicProdIoc`, `pi_univ`, `pi_Ioi_ae_eq_pi_Ici`, `MeasureTheory.ProbabilityMeasure.toMeasure_pi`, `pi_map_pi`, `univ_pi_Ico_ae_eq_Icc`, `MeasureTheory.partialTraj_const`, `pi_Ioo_ae_eq_pi_Icc`, `univ_pi_Ioi_ae_eq_Ici`, `pi.isMulRightInvariant`, `MeasureTheory.measurePreserving_piFinSuccAbove`, `pi_eq_generateFrom`, `MeasureTheory.measurePreserving_piUnique`, `pi.isMulLeftInvariant`, `pi_Ioo_ae_eq_pi_Ioc`, `pi_closedBall`, `quasiMeasurePreserving_eval`, `MeasureTheory.integral_fin_nat_prod_eq_prod`, `MeasureTheory.charFunDual_eq_pi_iff`, `isProjectiveLimit_infinitePiNat`, `ae_le_pi`, `univ_pi_Iio_ae_eq_Iic`, `MeasureTheory.measurePreserving_piFinsetUnion`, `pi.isNegInvariant`, `MeasureTheory.charFunDual_eq_pi_iff'`, `infinitePiNat_map_restrict`, `infinitePi_cylinder`, `MeasureTheory.partialTraj_const_restrict₂`, `IsUnifLocDoublingMeasure.pi`, `pi_def`, `ae_eq_pi`, `MeasureTheory.Integrable.fintype_prod`, `pi.isAddHaarMeasure`, `infinitePi_map_restrict`, `MeasureTheory.charFunDual_pi`, `ProbabilityTheory.iIndepFun_iff_map_fun_eq_pi_map`, `tendsto_eval_ae_ae`, `MeasureTheory.measurePreserving_sumPiEquivProdPi_symm`, `pi_empty_univ`, `MeasureTheory.measurePreserving_piEquivPiSubtypeProd`, `MeasureTheory.GridLines.T_univ`, `pi_map_piOptionEquivProd`, `MeasureTheory.FiniteMeasure.toMeasure_pi`, `MeasureTheory.measurePreserving_pi_empty`, `ae_pi_le_pi`, `ae_eq_set_pi`, `pi_Iio_ae_eq_pi_Iic`, `pi.instIsFiniteMeasure`, `MeasureTheory.measurePreserving_finTwoArrow`, `pi_pi`, `pi.isAddLeftInvariant`, `MeasureTheory.charFun_eq_pi_iff`, `pi.isOpenPosMeasure`, `pi.instIsProbabilityMeasure`, `ae_eval_ne`, `MeasureTheory.measurePreserving_sumPiEquivProdPi`, `MeasureTheory.lintegral_eq_of_lmarginal_eq`, `infinitePi_eq_pi`, `pi.isFiniteMeasureOnCompacts`, `pi_noAtoms'`
`pi'` 📖	CompOp	2 math math: `pi'_pi`, `pi'_eq_pi`
`tprod` 📖	CompOp	4 math math: `sigmaFinite_tprod`, `tprod_cons`, `tprod_tprod`, `tprod_nil`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_eq_pi` 📖	mathematical	`MeasureTheory.SigmaFinite` `Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass`	`MeasurableSpace.pi` `pi`	—	`instOuterMeasureClass` `Filter.Eventually.mono` `Filter.eventually_all` `Finite.of_fintype` `Filter.Tendsto.eventually` `tendsto_eval_ae_ae`
`ae_eq_set_pi` 📖	mathematical	`MeasureTheory.SigmaFinite` `Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass`	`MeasurableSpace.pi` `pi` `Set.pi`	—	`instOuterMeasureClass` `Filter.EventuallyLE.antisymm` `ae_le_set_pi` `Filter.EventuallyEq.le` `Filter.EventuallyEq.symm`
`ae_eval_ne` 📖	mathematical	`MeasureTheory.SigmaFinite`	`Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasurableSpace.pi` `instFunLike` `instOuterMeasureClass` `pi`	—	`instOuterMeasureClass` `MeasureTheory.compl_mem_ae_iff` `pi_hyperplane`
`ae_le_pi` 📖	mathematical	`MeasureTheory.SigmaFinite` `Filter.EventuallyLE` `Preorder.toLE` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass`	`Pi.hasLe` `MeasurableSpace.pi` `pi`	—	`instOuterMeasureClass` `Filter.Eventually.mono` `Filter.eventually_all` `Finite.of_fintype` `Filter.Tendsto.eventually` `tendsto_eval_ae_ae`
`ae_le_set_pi` 📖	mathematical	`MeasureTheory.SigmaFinite` `Filter.EventuallyLE` `Prop.le` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass`	`MeasurableSpace.pi` `pi` `Set.pi`	—	`instOuterMeasureClass` `Filter.Eventually.mono` `Filter.eventually_all_finite` `Set.toFinite` `Subtype.finite` `Finite.of_fintype` `Filter.Tendsto.eventually` `tendsto_eval_ae_ae`
`ae_pi_le_pi` 📖	mathematical	`MeasureTheory.SigmaFinite`	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasurableSpace.pi` `instFunLike` `instOuterMeasureClass` `pi` `Filter.pi`	—	`le_iInf` `instOuterMeasureClass` `Filter.Tendsto.le_comap` `tendsto_eval_ae_ae`
`instIsAddHaarMeasureForallVolumeOfMeasurableAddOfSigmaFinite` 📖	mathematical	`MeasurableAdd` `MeasureTheory.MeasureSpace.toMeasurableSpace` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `MeasureTheory.SigmaFinite` `MeasureTheory.MeasureSpace.volume` `IsAddHaarMeasure`	`Pi.addGroup` `Pi.topologicalSpace` `MeasureTheory.MeasureSpace.pi`	—	`pi.isAddHaarMeasure`
`instIsAddLeftInvariantForallVolumeOfMeasurableAddOfSigmaFinite` 📖	mathematical	`MeasurableAdd` `MeasureTheory.MeasureSpace.toMeasurableSpace` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `MeasureTheory.SigmaFinite` `MeasureTheory.MeasureSpace.volume` `IsAddLeftInvariant`	`MeasureTheory.MeasureSpace.pi` `Pi.instAdd`	—	`pi.isAddLeftInvariant`
`instIsAddRightInvariantForallVolumeOfMeasurableAddOfSigmaFinite` 📖	mathematical	`MeasurableAdd` `MeasureTheory.MeasureSpace.toMeasurableSpace` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `MeasureTheory.SigmaFinite` `MeasureTheory.MeasureSpace.volume` `IsAddRightInvariant`	`MeasureTheory.MeasureSpace.pi` `Pi.instAdd`	—	`pi.isAddRightInvariant`
`instIsFiniteMeasureForallVolume` 📖	mathematical	`MeasureTheory.IsFiniteMeasure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.MeasureSpace.volume`	`MeasureTheory.MeasureSpace.pi`	—	`pi.instIsFiniteMeasure`
`instIsFiniteMeasureOnCompactsForallVolumeOfSigmaFinite` 📖	mathematical	`MeasureTheory.SigmaFinite` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.MeasureSpace.volume` `MeasureTheory.IsFiniteMeasureOnCompacts`	`MeasureTheory.MeasureSpace.pi` `Pi.topologicalSpace`	—	`pi.isFiniteMeasureOnCompacts`
`instIsHaarMeasureForallVolumeOfMeasurableMulOfSigmaFinite` 📖	mathematical	`MeasurableMul` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MeasureTheory.SigmaFinite` `MeasureTheory.MeasureSpace.volume` `IsHaarMeasure`	`Pi.group` `Pi.topologicalSpace` `MeasureTheory.MeasureSpace.pi`	—	`pi.isHaarMeasure`
`instIsInvInvariantForallVolumeOfMeasurableInvOfSigmaFinite` 📖	mathematical	`MeasurableInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.SigmaFinite` `MeasureTheory.MeasureSpace.volume` `IsInvInvariant`	`MeasureTheory.MeasureSpace.pi` `Pi.instInv`	—	`pi.isInvInvariant`
`instIsLocallyFiniteMeasureForallVolumeOfSigmaFinite` 📖	mathematical	`MeasureTheory.SigmaFinite` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.MeasureSpace.volume` `MeasureTheory.IsLocallyFiniteMeasure`	`MeasureTheory.MeasureSpace.pi` `Pi.topologicalSpace`	—	`pi.isLocallyFiniteMeasure`
`instIsMulLeftInvariantForallVolumeOfMeasurableMulOfSigmaFinite` 📖	mathematical	`MeasurableMul` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MeasureTheory.SigmaFinite` `MeasureTheory.MeasureSpace.volume` `IsMulLeftInvariant`	`MeasureTheory.MeasureSpace.pi` `Pi.instMul`	—	`pi.isMulLeftInvariant`
`instIsMulRightInvariantForallVolumeOfMeasurableMulOfSigmaFinite` 📖	mathematical	`MeasurableMul` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MeasureTheory.SigmaFinite` `MeasureTheory.MeasureSpace.volume` `IsMulRightInvariant`	`MeasureTheory.MeasureSpace.pi` `Pi.instMul`	—	`pi.isMulRightInvariant`
`instIsNegInvariantForallVolumeOfMeasurableNegOfSigmaFinite` 📖	mathematical	`MeasurableNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.SigmaFinite` `MeasureTheory.MeasureSpace.volume` `IsNegInvariant`	`MeasureTheory.MeasureSpace.pi` `Pi.instNeg`	—	`pi.isNegInvariant`
`instIsOpenPosMeasureForallVolumeOfSigmaFinite` 📖	mathematical	`IsOpenPosMeasure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.MeasureSpace.volume` `MeasureTheory.SigmaFinite`	`Pi.topologicalSpace` `MeasureTheory.MeasureSpace.pi`	—	`pi.isOpenPosMeasure`
`instIsProbabilityMeasureForallVolume` 📖	mathematical	`MeasureTheory.IsProbabilityMeasure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.MeasureSpace.volume`	`MeasureTheory.MeasureSpace.pi`	—	`pi.instIsProbabilityMeasure`
`instNoAtomsForallVolumeOfNonemptyOfSigmaFinite` 📖	mathematical	`MeasureTheory.SigmaFinite` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.MeasureSpace.volume` `MeasureTheory.NoAtoms`	`MeasureTheory.MeasureSpace.pi`	—	`pi_noAtoms'`
`instSigmaFiniteForallVolume` 📖	mathematical	`MeasureTheory.SigmaFinite` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.MeasureSpace.volume`	`MeasureTheory.MeasureSpace.pi`	—	`pi.sigmaFinite`
`pi'_eq_pi` 📖	mathematical	`MeasureTheory.SigmaFinite`	`pi'` `pi`	—	`pi_eq` `pi'_pi`
`pi'_pi` 📖	mathematical	`MeasureTheory.SigmaFinite`	`DFunLike.coe` `MeasureTheory.Measure` `MeasurableSpace.pi` `Set` `ENNReal` `instFunLike` `pi'` `Set.pi` `Set.univ` `Finset.prod` `CommSemiring.toCommMonoid` `ENNReal.instCommSemiring` `Finset.univ`	—	`Encodable.mem_sortedUniv` `pi'.eq_1` `Encodable.sortedUniv_nodup` `MeasurableEquiv.piMeasurableEquivTProd_symm_apply` `MeasurableEquiv.map_apply` `Set.elim_preimage_pi` `tprod_tprod` `List.prod_toFinset` `Encodable.sortedUniv_toFinset`
`pi_Ico_ae_eq_pi_Icc` 📖	mathematical	`MeasureTheory.SigmaFinite` `MeasureTheory.NoAtoms`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasurableSpace.pi` `instFunLike` `instOuterMeasureClass` `pi` `Set.pi` `Set.Ico` `PartialOrder.toPreorder` `Set.Icc`	—	`ae_eq_set_pi` `MeasureTheory.Ico_ae_eq_Icc`
`pi_Iio_ae_eq_pi_Iic` 📖	mathematical	`MeasureTheory.SigmaFinite` `MeasureTheory.NoAtoms`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasurableSpace.pi` `instFunLike` `instOuterMeasureClass` `pi` `Set.pi` `Set.Iio` `PartialOrder.toPreorder` `Set.Iic`	—	`ae_eq_set_pi` `MeasureTheory.Iio_ae_eq_Iic`
`pi_Ioc_ae_eq_pi_Icc` 📖	mathematical	`MeasureTheory.SigmaFinite` `MeasureTheory.NoAtoms`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasurableSpace.pi` `instFunLike` `instOuterMeasureClass` `pi` `Set.pi` `Set.Ioc` `PartialOrder.toPreorder` `Set.Icc`	—	`ae_eq_set_pi` `MeasureTheory.Ioc_ae_eq_Icc`
`pi_Ioi_ae_eq_pi_Ici` 📖	mathematical	`MeasureTheory.SigmaFinite` `MeasureTheory.NoAtoms`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasurableSpace.pi` `instFunLike` `instOuterMeasureClass` `pi` `Set.pi` `Set.Ioi` `PartialOrder.toPreorder` `Set.Ici`	—	`ae_eq_set_pi` `MeasureTheory.Ioi_ae_eq_Ici`
`pi_Ioo_ae_eq_pi_Icc` 📖	mathematical	`MeasureTheory.SigmaFinite` `MeasureTheory.NoAtoms`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasurableSpace.pi` `instFunLike` `instOuterMeasureClass` `pi` `Set.pi` `Set.Ioo` `PartialOrder.toPreorder` `Set.Icc`	—	`ae_eq_set_pi` `MeasureTheory.Ioo_ae_eq_Icc`
`pi_Ioo_ae_eq_pi_Ioc` 📖	mathematical	`MeasureTheory.SigmaFinite` `MeasureTheory.NoAtoms`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasurableSpace.pi` `instFunLike` `instOuterMeasureClass` `pi` `Set.pi` `Set.Ioo` `PartialOrder.toPreorder` `Set.Ioc`	—	`ae_eq_set_pi` `MeasureTheory.Ioo_ae_eq_Ioc`
`pi_ball` 📖	mathematical	`MeasureTheory.SigmaFinite` `Real` `Real.instLT` `Real.instZero`	`DFunLike.coe` `MeasureTheory.Measure` `MeasurableSpace.pi` `Set` `ENNReal` `instFunLike` `pi` `Metric.ball` `pseudoMetricSpacePi` `MetricSpace.toPseudoMetricSpace` `Finset.prod` `CommSemiring.toCommMonoid` `ENNReal.instCommSemiring` `Finset.univ`	—	`ball_pi` `pi_pi`
`pi_caratheodory` 📖	mathematical	—	`MeasurableSpace` `MeasurableSpace.instLE` `MeasurableSpace.pi` `MeasureTheory.OuterMeasure.caratheodory` `MeasureTheory.OuterMeasure.pi` `toOuterMeasure`	—	`iSup_le` `MeasurableSpace.comap.eq_1` `MeasureTheory.OuterMeasure.boundedBy_caratheodory` `Finset.prod_congr` `Finset.prod_add_prod_le'` `ENNReal.instCanonicallyOrderedAdd` `Finset.mem_univ` `Set.image_congr` `Set.image_inter_preimage` `Set.image_diff_preimage` `MeasureTheory.measure_inter_add_diff` `MeasureTheory.measure_mono` `MeasureTheory.OuterMeasure.instOuterMeasureClass` `Set.image_mono` `Set.inter_subset_left` `Set.diff_subset`
`pi_closedBall` 📖	mathematical	`MeasureTheory.SigmaFinite` `Real` `Real.instLE` `Real.instZero`	`DFunLike.coe` `MeasureTheory.Measure` `MeasurableSpace.pi` `Set` `ENNReal` `instFunLike` `pi` `Metric.closedBall` `pseudoMetricSpacePi` `MetricSpace.toPseudoMetricSpace` `Finset.prod` `CommSemiring.toCommMonoid` `ENNReal.instCommSemiring` `Finset.univ`	—	`closedBall_pi` `pi_pi`
`pi_def` 📖	mathematical	—	`pi` `MeasureTheory.OuterMeasure.toMeasure` `MeasurableSpace.pi` `MeasureTheory.OuterMeasure.pi` `toOuterMeasure` `pi_caratheodory`	—	`pi_caratheodory`
`pi_empty_univ` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `MeasurableSpace.pi` `Set` `ENNReal` `instFunLike` `pi` `Set.univ` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`pi_of_empty` `MeasureTheory.IsProbabilityMeasure.measure_univ` `dirac.isProbabilityMeasure`
`pi_eq` 📖	mathematical	`MeasureTheory.SigmaFinite` `DFunLike.coe` `MeasureTheory.Measure` `MeasurableSpace.pi` `Set` `ENNReal` `instFunLike` `Set.pi` `Set.univ` `Finset.prod` `CommSemiring.toCommMonoid` `ENNReal.instCommSemiring` `Finset.univ`	`pi`	—	`pi_eq_generateFrom` `MeasurableSpace.generateFrom_measurableSet` `MeasurableSpace.isPiSystem_measurableSet`
`pi_eq_generateFrom` 📖	mathematical	`MeasurableSpace.generateFrom` `IsPiSystem` `DFunLike.coe` `MeasureTheory.Measure` `MeasurableSpace.pi` `Set` `ENNReal` `instFunLike` `Set.pi` `Set.univ` `Finset.prod` `CommSemiring.toCommMonoid` `ENNReal.instCommSemiring` `Finset.univ`	`pi`	—	`MeasurableSpace.measurableSet_generateFrom` `FiniteSpanningSetsIn.ext` `generateFrom_eq_pi` `Finite.of_fintype` `FiniteSpanningSetsIn.isCountablySpanning` `IsPiSystem.pi` `Set.mem_univ_pi` `pi_pi_aux` `FiniteSpanningSetsIn.sigmaFinite`
`pi_eval_preimage_null` 📖	mathematical	`MeasureTheory.SigmaFinite` `DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `instZeroENNReal`	`MeasurableSpace.pi` `pi` `Set.preimage` `Function.eval`	—	`MeasureTheory.exists_measurable_superset_of_null` `Set.univ_pi_update_univ` `pi_pi` `Finset.prod_eq_zero` `Finset.mem_univ` `Function.update_self` `MeasureTheory.measure_mono_null` `instOuterMeasureClass` `Set.preimage_mono`
`pi_hyperplane` 📖	mathematical	`MeasureTheory.SigmaFinite`	`DFunLike.coe` `MeasureTheory.Measure` `MeasurableSpace.pi` `Set` `ENNReal` `instFunLike` `pi` `setOf` `instZeroENNReal`	—	`pi_eval_preimage_null` `MeasureTheory.NoAtoms.measure_singleton`
`pi_map_eval` 📖	mathematical	`MeasureTheory.SigmaFinite`	`map` `MeasurableSpace.pi` `Function.eval` `pi` `ENNReal` `MeasureTheory.Measure` `instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right` `Finset.prod` `CommSemiring.toCommMonoid` `Finset.erase` `Finset.univ` `DFunLike.coe` `Set` `instFunLike` `Set.univ`	—	`ext` `IsScalarTower.right` `map_apply` `measurable_pi_apply` `Set.univ_pi_update_univ` `pi_pi` `smul_apply` `smul_eq_mul` `Finset.prod_erase_mul` `Finset.prod_congr` `Finset.ne_of_mem_erase` `Function.update_self`
`pi_map_pi` 📖	mathematical	`MeasureTheory.SigmaFinite` `map` `AEMeasurable`	`MeasurableSpace.pi` `pi`	—	`MeasureTheory.SigmaFinite.of_map` `pi_eq` `map_apply_of_aemeasurable` `aemeasurable_pi_lambda` `Finite.to_countable` `Finite.of_fintype` `AEMeasurable.comp_quasiMeasurePreserving` `quasiMeasurePreserving_eval` `MeasurableSet.univ_pi` `Set.ext` `pi_pi`
`pi_map_piCongrLeft` 📖	mathematical	`MeasureTheory.SigmaFinite`	`map` `MeasurableSpace.pi` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `MeasurableEquiv` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.piCongrLeft` `pi`	—	`pi_eq` `MeasurableEmbedding.map_apply` `MeasurableEquiv.measurableEmbedding` `Set.ext` `Equiv.forall_congr` `MeasurableEquiv.piCongrLeft_apply_apply` `pi_pi` `Fintype.prod_equiv`
`pi_map_piOptionEquivProd` 📖	mathematical	`MeasureTheory.SigmaFinite`	`map` `Prod.instMeasurableSpace` `MeasurableSpace.pi` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.symm` `MeasurableEquiv.piOptionEquivProd` `prod` `pi` `instFintypeOption`	—	`pi_eq` `MeasurableEquiv.measurableEmbedding` `Set.ext` `MeasurableEmbedding.map_apply` `prod_prod` `MeasureTheory.instSFiniteOfSigmaFinite` `pi_pi` `mul_comm` `Finset.prod_insertNone`
`pi_noAtoms` 📖	mathematical	`MeasureTheory.SigmaFinite`	`MeasureTheory.NoAtoms` `MeasurableSpace.pi` `pi`	—	`MeasureTheory.measure_mono_null` `instOuterMeasureClass` `pi_hyperplane` `Set.singleton_subset_iff`
`pi_noAtoms'` 📖	mathematical	`MeasureTheory.SigmaFinite` `MeasureTheory.NoAtoms`	`MeasurableSpace.pi` `pi`	—	`pi_noAtoms`
`pi_of_empty` 📖	mathematical	—	`pi` `dirac` `isEmptyElim` `MeasurableSpace.pi`	—	`pi_eq` `Fintype.prod_empty` `dirac_apply_of_mem`
`pi_pi` 📖	mathematical	`MeasureTheory.SigmaFinite`	`DFunLike.coe` `MeasureTheory.Measure` `MeasurableSpace.pi` `Set` `ENNReal` `instFunLike` `pi` `Set.pi` `Set.univ` `Finset.prod` `CommSemiring.toCommMonoid` `ENNReal.instCommSemiring` `Finset.univ`	—	`pi'_eq_pi` `pi'_pi`
`pi_pi_aux` 📖	mathematical	`MeasureTheory.SigmaFinite` `MeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `MeasurableSpace.pi` `Set` `ENNReal` `instFunLike` `pi` `Set.pi` `Set.univ` `Finset.prod` `CommSemiring.toCommMonoid` `ENNReal.instCommSemiring` `Finset.univ`	—	`le_antisymm` `pi_caratheodory` `pi_def` `MeasureTheory.toMeasure_apply` `MeasurableSet.pi` `Set.countable_univ` `Finite.to_countable` `Finite.of_fintype` `MeasureTheory.OuterMeasure.pi_pi_le` `pi'_pi` `Encodable.countable` `MeasureTheory.OuterMeasure.le_pi` `Eq.le`
`pi_singleton` 📖	mathematical	`MeasureTheory.SigmaFinite`	`DFunLike.coe` `MeasureTheory.Measure` `MeasurableSpace.pi` `Set` `ENNReal` `instFunLike` `pi` `Set.instSingletonSet` `Finset.prod` `CommSemiring.toCommMonoid` `ENNReal.instCommSemiring` `Finset.univ`	—	`Set.univ_pi_singleton` `pi_pi`
`pi_univ` 📖	mathematical	`MeasureTheory.SigmaFinite`	`DFunLike.coe` `MeasureTheory.Measure` `MeasurableSpace.pi` `Set` `ENNReal` `instFunLike` `pi` `Set.univ` `Finset.prod` `CommSemiring.toCommMonoid` `ENNReal.instCommSemiring` `Finset.univ`	—	`Set.pi_univ` `pi_pi`
`quasiMeasurePreserving_eval` 📖	mathematical	`MeasureTheory.SigmaFinite`	`QuasiMeasurePreserving` `MeasurableSpace.pi` `Function.eval` `pi`	—	`measurable_pi_apply` `map_apply` `pi_eval_preimage_null`
`restrict_pi_pi` 📖	mathematical	`MeasureTheory.SigmaFinite`	`restrict` `MeasurableSpace.pi` `pi` `Set.pi` `Set.univ`	—	`pi_eq` `MeasureTheory.Restrict.sigmaFinite` `restrict_apply` `MeasurableSet.univ_pi` `Finite.to_countable` `Finite.of_fintype` `Finset.prod_congr` `pi_pi`
`sigmaFinite_tprod` 📖	mathematical	`MeasureTheory.SigmaFinite`	`List.TProd` `TProd.instMeasurableSpace` `tprod`	—	`tprod_nil` `dirac.instSigmaFinite` `tprod_cons` `prod.instSigmaFinite`
`tendsto_eval_ae_ae` 📖	mathematical	`MeasureTheory.SigmaFinite`	`Filter.Tendsto` `Function.eval` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasurableSpace.pi` `instFunLike` `instOuterMeasureClass` `pi`	—	`instOuterMeasureClass` `pi_eval_preimage_null`
`tprod_cons` 📖	mathematical	—	`tprod` `prod` `List.TProd` `TProd.instMeasurableSpace`	—	—
`tprod_nil` 📖	mathematical	—	`tprod` `dirac` `PUnit.instMeasurableSpace`	—	—
`tprod_tprod` 📖	mathematical	`MeasureTheory.SigmaFinite`	`DFunLike.coe` `MeasureTheory.Measure` `List.TProd` `TProd.instMeasurableSpace` `Set` `ENNReal` `instFunLike` `tprod` `Set.tprod` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`MeasureTheory.IsProbabilityMeasure.measure_univ` `dirac.isProbabilityMeasure` `tprod_cons` `Set.tprod.eq_2` `prod_prod` `MeasureTheory.instSFiniteOfSigmaFinite` `sigmaFinite_tprod`
`univ_pi_Ico_ae_eq_Icc` 📖	mathematical	`MeasureTheory.SigmaFinite` `MeasureTheory.NoAtoms`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasurableSpace.pi` `instFunLike` `instOuterMeasureClass` `pi` `Set.pi` `Set.univ` `Set.Ico` `PartialOrder.toPreorder` `Set.Icc` `Pi.preorder`	—	`instOuterMeasureClass` `Set.pi_univ_Icc` `pi_Ico_ae_eq_pi_Icc`
`univ_pi_Iio_ae_eq_Iic` 📖	mathematical	`MeasureTheory.SigmaFinite` `MeasureTheory.NoAtoms`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasurableSpace.pi` `instFunLike` `instOuterMeasureClass` `pi` `Set.pi` `Set.univ` `Set.Iio` `PartialOrder.toPreorder` `Set.Iic` `Pi.preorder`	—	`instOuterMeasureClass` `Set.pi_univ_Iic` `pi_Iio_ae_eq_pi_Iic`
`univ_pi_Ioc_ae_eq_Icc` 📖	mathematical	`MeasureTheory.SigmaFinite` `MeasureTheory.NoAtoms`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasurableSpace.pi` `instFunLike` `instOuterMeasureClass` `pi` `Set.pi` `Set.univ` `Set.Ioc` `PartialOrder.toPreorder` `Set.Icc` `Pi.preorder`	—	`instOuterMeasureClass` `Set.pi_univ_Icc` `pi_Ioc_ae_eq_pi_Icc`
`univ_pi_Ioi_ae_eq_Ici` 📖	mathematical	`MeasureTheory.SigmaFinite` `MeasureTheory.NoAtoms`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasurableSpace.pi` `instFunLike` `instOuterMeasureClass` `pi` `Set.pi` `Set.univ` `Set.Ioi` `PartialOrder.toPreorder` `Set.Ici` `Pi.preorder`	—	`instOuterMeasureClass` `Set.pi_univ_Ici` `pi_Ioi_ae_eq_pi_Ici`
`univ_pi_Ioo_ae_eq_Icc` 📖	mathematical	`MeasureTheory.SigmaFinite` `MeasureTheory.NoAtoms`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasurableSpace.pi` `instFunLike` `instOuterMeasureClass` `pi` `Set.pi` `Set.univ` `Set.Ioo` `PartialOrder.toPreorder` `Set.Icc` `Pi.preorder`	—	`instOuterMeasureClass` `Set.pi_univ_Icc` `pi_Ioo_ae_eq_pi_Icc`
`volume_pi_eq_dirac` 📖	mathematical	—	`MeasureTheory.MeasureSpace.volume` `MeasureTheory.MeasureSpace.pi` `dirac` `isEmptyElim` `MeasurableSpace.pi` `MeasureTheory.MeasureSpace.toMeasurableSpace`	—	`pi_of_empty`

MeasureTheory.Measure.FiniteSpanningSetsIn

Definitions

Name	Category	Theorems
`pi` 📖	CompOp	—

MeasureTheory.Measure.IsUnifLocDoublingMeasure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`volume_pi` 📖	mathematical	`MeasureTheory.SigmaFinite` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.MeasureSpace.volume` `IsUnifLocDoublingMeasure`	`pseudoMetricSpacePi` `MeasureTheory.MeasureSpace.pi`	—	`IsUnifLocDoublingMeasure.pi`

MeasureTheory.Measure.pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsFiniteMeasure` 📖	mathematical	`MeasureTheory.IsFiniteMeasure`	`MeasurableSpace.pi` `MeasureTheory.Measure.pi`	—	`ENNReal.prod_lt_top` `MeasureTheory.measure_lt_top` `MeasureTheory.Measure.pi_univ` `MeasureTheory.IsFiniteMeasure.toSigmaFinite`
`instIsProbabilityMeasure` 📖	mathematical	`MeasureTheory.IsProbabilityMeasure`	`MeasurableSpace.pi` `MeasureTheory.Measure.pi`	—	`MeasureTheory.Measure.pi_univ` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `Finset.prod_congr` `MeasureTheory.IsProbabilityMeasure.measure_univ` `Finset.prod_const_one`
`isAddHaarMeasure` 📖	mathematical	`MeasureTheory.SigmaFinite` `MeasureTheory.Measure.IsAddHaarMeasure` `MeasurableAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	`Pi.addGroup` `Pi.topologicalSpace` `MeasurableSpace.pi` `MeasureTheory.Measure.pi`	—	`isFiniteMeasureOnCompacts` `MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `isAddLeftInvariant` `MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant` `isOpenPosMeasure` `MeasureTheory.Measure.IsAddHaarMeasure.toIsOpenPosMeasure`
`isAddLeftInvariant` 📖	mathematical	`MeasureTheory.SigmaFinite` `MeasurableAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `MeasureTheory.Measure.IsAddLeftInvariant`	`MeasurableSpace.pi` `Pi.instAdd` `MeasureTheory.Measure.pi`	—	`MeasureTheory.Measure.pi_eq` `MeasureTheory.Measure.map_apply` `MeasurableAdd.measurable_const_add` `Pi.measurableAdd` `MeasurableSet.univ_pi` `Finite.to_countable` `Finite.of_fintype` `MeasureTheory.Measure.pi_pi` `Finset.prod_congr` `MeasureTheory.measure_preimage_add`
`isAddRightInvariant` 📖	mathematical	`MeasureTheory.SigmaFinite` `MeasurableAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `MeasureTheory.Measure.IsAddRightInvariant`	`MeasurableSpace.pi` `Pi.instAdd` `MeasureTheory.Measure.pi`	—	`MeasureTheory.Measure.pi_eq` `MeasureTheory.Measure.map_apply` `MeasurableAdd.measurable_add_const` `Pi.measurableAdd` `MeasurableSet.univ_pi` `Finite.to_countable` `Finite.of_fintype` `MeasureTheory.Measure.pi_pi` `Finset.prod_congr` `MeasureTheory.measure_preimage_add_right`
`isFiniteMeasureOnCompacts` 📖	mathematical	`MeasureTheory.SigmaFinite` `MeasureTheory.IsFiniteMeasureOnCompacts`	`MeasurableSpace.pi` `Pi.topologicalSpace` `MeasureTheory.Measure.pi`	—	`MeasureTheory.Measure.pi_pi` `WithTop.prod_lt_top` `NNReal.instNoZeroDivisors` `IsCompact.measure_lt_top` `IsCompact.image` `continuous_apply` `lt_of_le_of_lt` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Set.subset_pi_eval_image`
`isHaarMeasure` 📖	mathematical	`MeasureTheory.SigmaFinite` `MeasureTheory.Measure.IsHaarMeasure` `MeasurableMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	`Pi.group` `Pi.topologicalSpace` `MeasurableSpace.pi` `MeasureTheory.Measure.pi`	—	`isFiniteMeasureOnCompacts` `MeasureTheory.Measure.IsHaarMeasure.toIsFiniteMeasureOnCompacts` `isMulLeftInvariant` `MeasureTheory.Measure.IsHaarMeasure.toIsMulLeftInvariant` `isOpenPosMeasure` `MeasureTheory.Measure.IsHaarMeasure.toIsOpenPosMeasure`
`isInvInvariant` 📖	mathematical	`MeasureTheory.SigmaFinite` `MeasurableInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `MeasureTheory.Measure.IsInvInvariant`	`MeasurableSpace.pi` `Pi.instInv` `MeasureTheory.Measure.pi`	—	`MeasureTheory.Measure.pi_eq` `Set.ext` `Set.inv_pi` `MeasureTheory.Measure.map_apply` `MeasurableInv.measurable_inv` `Pi.measurableInv` `MeasurableSet.univ_pi` `Finite.to_countable` `Finite.of_fintype` `MeasureTheory.Measure.pi_pi` `Finset.prod_congr` `MeasureTheory.Measure.measure_preimage_inv`
`isLocallyFiniteMeasure` 📖	mathematical	`MeasureTheory.SigmaFinite` `MeasureTheory.IsLocallyFiniteMeasure`	`MeasurableSpace.pi` `Pi.topologicalSpace` `MeasureTheory.Measure.pi`	—	`set_pi_mem_nhds` `Set.finite_univ` `Finite.of_fintype` `IsOpen.mem_nhds` `MeasureTheory.Measure.pi_pi` `ENNReal.prod_lt_top` `MeasureTheory.Measure.exists_isOpen_measure_lt_top`
`isMulLeftInvariant` 📖	mathematical	`MeasureTheory.SigmaFinite` `MeasurableMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MeasureTheory.Measure.IsMulLeftInvariant`	`MeasurableSpace.pi` `Pi.instMul` `MeasureTheory.Measure.pi`	—	`MeasureTheory.Measure.pi_eq` `MeasureTheory.Measure.map_apply` `MeasurableMul.measurable_const_mul` `Pi.measurableMul` `MeasurableSet.univ_pi` `Finite.to_countable` `Finite.of_fintype` `MeasureTheory.Measure.pi_pi` `Finset.prod_congr` `MeasureTheory.measure_preimage_mul`
`isMulRightInvariant` 📖	mathematical	`MeasureTheory.SigmaFinite` `MeasurableMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MeasureTheory.Measure.IsMulRightInvariant`	`MeasurableSpace.pi` `Pi.instMul` `MeasureTheory.Measure.pi`	—	`MeasureTheory.Measure.pi_eq` `MeasureTheory.Measure.map_apply` `MeasurableMul.measurable_mul_const` `Pi.measurableMul` `MeasurableSet.univ_pi` `Finite.to_countable` `Finite.of_fintype` `MeasureTheory.Measure.pi_pi` `Finset.prod_congr` `MeasureTheory.measure_preimage_mul_right`
`isNegInvariant` 📖	mathematical	`MeasureTheory.SigmaFinite` `MeasurableNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `MeasureTheory.Measure.IsNegInvariant`	`MeasurableSpace.pi` `Pi.instNeg` `MeasureTheory.Measure.pi`	—	`MeasureTheory.Measure.pi_eq` `Set.ext` `Set.neg_pi` `Set.mem_pi` `Set.mem_univ` `Set.mem_neg` `MeasureTheory.Measure.map_apply` `MeasurableNeg.measurable_neg` `Pi.measurableNeg` `MeasurableSet.univ_pi` `Finite.to_countable` `Finite.of_fintype` `MeasureTheory.Measure.pi_pi` `Finset.prod_congr` `MeasureTheory.Measure.measure_preimage_neg`
`isOpenPosMeasure` 📖	mathematical	`MeasureTheory.SigmaFinite` `MeasureTheory.Measure.IsOpenPosMeasure`	`Pi.topologicalSpace` `MeasurableSpace.pi` `MeasureTheory.Measure.pi`	—	`isOpen_pi_iff'` `Finite.of_fintype` `ne_of_gt` `lt_of_lt_of_le` `MeasureTheory.Measure.pi_pi` `CanonicallyOrderedAdd.prod_pos` `ENNReal.instCanonicallyOrderedAdd` `ENNReal.instNoZeroDivisors` `IsOpen.measure_pos` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass`
`sigmaFinite` 📖	mathematical	`MeasureTheory.SigmaFinite`	`MeasurableSpace.pi` `MeasureTheory.Measure.pi`	—	`MeasureTheory.Measure.FiniteSpanningSetsIn.sigmaFinite`

MeasureTheory.MeasureSpace

Definitions

Name	Category	Theorems
`pi` 📖	CompOp	151 math math: `MeasureTheory.volume_preserving_arrowCongr'`, `NumberField.mixedEmbedding.integral_comp_polarSpaceCoord_symm`, `NumberField.mixedEmbedding.fundamentalDomain_integerLattice`, `MeasureTheory.Measure.instNoAtomsForallVolumeOfNonemptyOfSigmaFinite`, `NumberField.mixedEmbedding.lintegral_comp_polarCoord_symm`, `MeasureTheory.volume_preserving_pi`, `UnitAddTorus.coe_mFourierBasis`, `ZSpan.volume_real_fundamentalDomain`, `MeasureTheory.volume_pi`, `MeasureTheory.Measure.instIsNegInvariantForallVolumeOfMeasurableNegOfSigmaFinite`, `Complex.integral_comp_pi_polarCoord_symm`, `ZLattice.covolume_eq_det_inv`, `MeasureTheory.integral_fintype_prod_volume_eq_pow`, `MeasureTheory.volume_measurePreserving_piCongrLeft`, `NumberField.mixedEmbedding.instIsAddHaarMeasureMixedSpaceVolume`, `Real.smul_map_diagonal_volume_pi`, `MeasureTheory.Measure.instIsAddLeftInvariantForallVolumeOfMeasurableAddOfSigmaFinite`, `NumberField.mixedEmbedding.instNoAtomsMixedSpaceVolume`, `MeasureTheory.volume_pi_pi`, `Real.volume_pi_ball`, `NumberField.mixedEmbedding.convexBodyLT_volume`, `Complex.volume_sum_rpow_le`, `MeasureTheory.volume_preserving_piFinsetUnion`, `Set.OrdConnected.nullMeasurableSet`, `NumberField.mixedEmbedding.fundamentalCone.volume_frontier_normLeOne`, `MeasureTheory.Measure.instIsAddRightInvariantForallVolumeOfMeasurableAddOfSigmaFinite`, `NumberField.mixedEmbedding.iUnion_negAt_plusPart_ae`, `BoxIntegral.unitPartition.integralSum_eq_tsum_div`, `MeasureTheory.integral_fin_nat_prod_volume_eq_prod`, `NumberField.mixedEmbedding.fundamentalCone.volume_interior_eq_volume_closure`, `UnitAddTorus.mFourierCoeff_toLp`, `NumberField.mixedEmbedding.convexBodySum_volume_eq_zero_of_le_zero`, `Real.volume_pi_Ico`, `Real.map_matrix_volume_pi_eq_smul_volume_pi`, `Real.volume_Icc_pi`, `PiLp.volume_preserving_toLp`, `lintegral_comp_pi_polarCoord_symm`, `NumberField.mixedEmbedding.fundamentalDomain_idealLattice`, `Real.volume_pi_Ioc`, `ZLattice.covolume_div_covolume_eq_relIndex`, `Real.volume_Icc_pi_toReal`, `MeasureTheory.volume_sum_rpow_lt`, `ZSpan.volume_fundamentalDomain`, `GaussianFourier.integrable_cexp_neg_mul_sum_add`, `MeasureTheory.hausdorffMeasure_pi_real`, `MeasureTheory.volume_preserving_piFinSuccAbove`, `Real.volume_pi_Ioc_toReal`, `BoxIntegral.Box.coe_ae_eq_Icc`, `BoxIntegral.Box.Ioo_ae_eq_Icc`, `MeasureTheory.Measure.instIsMulLeftInvariantForallVolumeOfMeasurableMulOfSigmaFinite`, `UnitAddTorus.coeFn_mFourierLp`, `MeasureTheory.volume_sum_rpow_le`, `MeasureTheory.Measure.instIsLocallyFiniteMeasureForallVolumeOfSigmaFinite`, `NumberField.mixedEmbedding.realSpace.volume_eq_zero`, `MeasureTheory.volume_preserving_pi_empty`, `MeasureTheory.Measure.instIsFiniteMeasureForallVolume`, `NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed`, `NumberField.mixedEmbedding.covolume_idealLattice`, `NumberField.mixedEmbedding.volume_preserving_negAt`, `Set.OrdConnected.null_frontier`, `MeasureTheory.Pi.isInvInvariant_volume`, `Real.volume_pi_le_prod_diam`, `NumberField.Units.regOfFamily_of_isMaxRank`, `MeasureTheory.Measure.instIsAddHaarMeasureForallVolumeOfMeasurableAddOfSigmaFinite`, `PiLp.volume_preserving_ofLp`, `UnitAddTorus.orthonormal_mFourier`, `BoxIntegral.Box.volume_apply'`, `NumberField.mixedEmbedding.volume_preserving_mixedSpaceToRealMixedSpace_symm`, `MeasureTheory.Measure.IsUnifLocDoublingMeasure.volume_pi`, `MeasureTheory.Measure.volume_pi_eq_dirac`, `MeasureTheory.Measure.instIsMulRightInvariantForallVolumeOfMeasurableMulOfSigmaFinite`, `Complex.volume_sum_rpow_lt`, `Real.volume_pi_Ioo`, `UnitAddTorus.instContinuousSMulComplexSubtypeAEEqFunVolumeMemAddSubgroupLp`, `UnitAddTorus.hasSum_mFourier_series_L2`, `Real.volume_pi_Ioo_toReal`, `NumberField.mixedEmbedding.covolume_integerLattice`, `MeasureTheory.Pi.isNegInvariant_volume`, `MeasureTheory.Measure.instIsHaarMeasureForallVolumeOfMeasurableMulOfSigmaFinite`, `NumberField.mixedEmbedding.fundamentalCone.setLIntegral_paramSet_exp`, `NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis`, `MeasureTheory.addHaarMeasure_eq_volume_pi`, `NumberField.mixedEmbedding.volume_negAt_plusPart`, `NumberField.mixedEmbedding.convexBodyLT'_volume`, `ZLattice.volume_image_eq_volume_div_covolume`, `Real.map_linearMap_volume_pi_eq_smul_volume_pi`, `MeasureTheory.volume_preserving_piFinTwo`, `EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp`, `MeasureTheory.volume_pi_ball`, `MeasureTheory.Measure.instSigmaFiniteForallVolume`, `NumberField.mixedEmbedding.volume_eq_two_pow_mul_two_pi_pow_mul_integral`, `Complex.volume_preserving_equiv_pi`, `NumberField.mixedEmbedding.volume_preserving_homeoRealMixedSpacePolarSpace`, `MeasureTheory.Measure.instIsProbabilityMeasureForallVolume`, `NumberField.mixedEmbedding.volume_eq_zero`, `MeasureTheory.Measure.instIsInvInvariantForallVolumeOfMeasurableInvOfSigmaFinite`, `MeasureTheory.volume_pi_closedBall`, `GaussianFourier.integral_cexp_neg_mul_sum_add`, `ZLattice.volume_image_eq_volume_div_covolume'`, `Real.volume_pi_Ico_toReal`, `Real.volume_pi_le_diam_pow`, `UnitAddTorus.hasSum_prod_mFourierCoeff`, `NumberField.mixedEmbedding.lintegral_comp_polarCoordReal_symm`, `MeasureTheory.lintegral_pow_le_pow_lintegral_fderiv_aux`, `MeasureTheory.volume_measurePreserving_arrowProdEquivProdArrow`, `IsUpperSet.null_frontier`, `MeasureTheory.isAddHaarMeasure_volume_pi`, `MeasureTheory.volume_preserving_piUnique`, `NumberField.mixedEmbedding.polarCoordReal_symm_target_ae_eq_univ`, `GaussianFourier.integral_cexp_neg_sum_mul_add`, `BoxIntegral.Box.volume_apply`, `UnitAddTorus.mFourierBasis_repr`, `MeasureTheory.integral_fintype_prod_volume_eq_prod`, `NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis`, `UnitAddTorus.hasSum_sq_mFourierCoeff`, `Complex.lintegral_comp_pi_polarCoord_symm`, `NumberField.mixedEmbedding.fundamentalCone.setLIntegral_expMapBasis_image`, `GaussianFourier.integrable_cexp_neg_sum_mul_add`, `NumberField.mixedEmbedding.fundamentalCone.compactSet_ae`, `NumberField.mixedEmbedding.instIsAddHaarMeasureRealMixedSpaceVolume`, `pi_polarCoord_symm_target_ae_eq_univ`, `BoxIntegral.unitPartition.volume_box`, `Complex.volume_sum_rpow_lt_one`, `NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm`, `NumberField.mixedEmbedding.fundamentalCone.volume_normLeOne`, `MeasureTheory.volume_preserving_finTwoArrow`, `MeasureTheory.Measure.instIsOpenPosMeasureForallVolumeOfSigmaFinite`, `TorusIntegrable.function_integrable`, `NumberField.mixedEmbedding.volume_eq_two_pi_pow_mul_integral`, `IsAntichain.volume_eq_zero`, `NumberField.mixedEmbedding.convexBodySum_volume`, `IsLowerSet.null_frontier`, `NumberField.mixedEmbedding.integral_comp_polarCoord_symm`, `Real.volume_pi_closedBall`, `UnitAddTorus.span_mFourierLp_closure_eq_top`, `MeasureTheory.volume_measurePreserving_sumPiEquivProdPi`, `MeasureTheory.Pi.isAddLeftInvariant_volume`, `MeasureTheory.volume_preserving_piEquivPiSubtypeProd`, `Real.volume_preserving_transvectionStruct`, `MeasureTheory.volume_measurePreserving_sumPiEquivProdPi_symm`, `MeasureTheory.Measure.instIsFiniteMeasureOnCompactsForallVolumeOfSigmaFinite`, `NumberField.mixedEmbedding.integral_comp_polarCoordReal_symm`, `integral_comp_pi_polarCoord_symm`, `MeasureTheory.volume_preserving_funUnique`, `MeasureTheory.volume_sum_rpow_lt_one`, `NumberField.mixedEmbedding.volume_fundamentalDomain_stdBasis`, `NumberField.mixedEmbedding.volume_eq_two_pow_mul_volume_plusPart`, `MeasureTheory.Pi.isMulLeftInvariant_volume`, `ZLattice.covolume_eq_det`, `NumberField.mixedEmbedding.fundamentalCone.closure_paramSet_ae_interior`, `NumberField.mixedEmbedding.lintegral_comp_polarSpaceCoord_symm`

MeasureTheory.OuterMeasure

Definitions

Name	Category	Theorems
`pi` 📖	CompOp	4 math math: `le_pi`, `MeasureTheory.Measure.pi_caratheodory`, `pi_pi_le`, `MeasureTheory.Measure.pi_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_pi` 📖	mathematical	—	`MeasureTheory.OuterMeasure` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `pi` `ENNReal` `ENNReal.instPartialOrder` `DFunLike.coe` `Set` `instFunLikeSetENNReal` `Set.pi` `Set.univ` `Finset.prod` `CommSemiring.toCommMonoid` `ENNReal.instCommSemiring` `Finset.univ`	—	`pi.eq_1` `le_boundedBy'` `LE.le.trans_eq` `MeasureTheory.piPremeasure_pi` `le_trans` `mono` `Set.subset_pi_eval_image` `Set.image_congr`
`pi_pi_le` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `instFunLikeSetENNReal` `pi` `Set.pi` `Set.univ` `Finset.prod` `CommSemiring.toCommMonoid` `ENNReal.instCommSemiring` `Finset.univ`	—	`Set.eq_empty_or_nonempty` `MeasureTheory.measure_empty` `instOuterMeasureClass` `ENNReal.instCanonicallyOrderedAdd` `LE.le.trans_eq` `boundedBy_le` `MeasureTheory.piPremeasure_pi`

MeasureTheory.Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAddLeftInvariant_volume` 📖	mathematical	—	`MeasureTheory.Measure.IsAddLeftInvariant` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.MeasureSpace.pi` `Pi.instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `MeasureTheory.MeasureSpace.volume`	—	`MeasureTheory.Measure.pi.isAddLeftInvariant`
`isInvInvariant_volume` 📖	mathematical	—	`MeasureTheory.Measure.IsInvInvariant` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.MeasureSpace.pi` `Pi.instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `MeasureTheory.MeasureSpace.volume`	—	`MeasureTheory.Measure.pi.isInvInvariant`
`isMulLeftInvariant_volume` 📖	mathematical	—	`MeasureTheory.Measure.IsMulLeftInvariant` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.MeasureSpace.pi` `Pi.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MeasureTheory.MeasureSpace.volume`	—	`MeasureTheory.Measure.pi.isMulLeftInvariant`
`isNegInvariant_volume` 📖	mathematical	—	`MeasureTheory.Measure.IsNegInvariant` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.MeasureSpace.pi` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `MeasureTheory.MeasureSpace.volume`	—	`MeasureTheory.Measure.pi.isNegInvariant`

---

← Back to Index