Basic

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

Statistics

Metric	Count
Definitions `regionBetween`	1
Theorems `volume_pos_of_nhds_real`, `isFiniteMeasure_restrict_Icc`, `isFiniteMeasure_restrict_Ico`, `isFiniteMeasure_restrict_Ioc`, `isFiniteMeasure_restrict_Ioo`, `locallyFinite_volume`, `map_linearMap_volume_pi_eq_smul_volume_pi`, `map_matrix_volume_pi_eq_smul_volume_pi`, `map_volume_mul_left`, `map_volume_mul_right`, `noAtoms_volume`, `smul_map_diagonal_volume_pi`, `smul_map_volume_mul_left`, `smul_map_volume_mul_right`, `volume_Icc`, `volume_Icc_pi`, `volume_Icc_pi_toReal`, `volume_Ici`, `volume_Ico`, `volume_Iic`, `volume_Iio`, `volume_Ioc`, `volume_Ioi`, `volume_Ioo`, `volume_ball`, `volume_closedBall`, `volume_closedEBall`, `volume_eball`, `volume_emetric_ball`, `volume_emetric_closedBall`, `volume_eq_stieltjes_id`, `volume_interval`, `volume_le_diam`, `volume_pi_Ico`, `volume_pi_Ico_toReal`, `volume_pi_Ioc`, `volume_pi_Ioc_toReal`, `volume_pi_Ioo`, `volume_pi_Ioo_toReal`, `volume_pi_ball`, `volume_pi_closedBall`, `volume_pi_le_diam_pow`, `volume_pi_le_prod_diam`, `volume_preimage_mul_left`, `volume_preimage_mul_right`, `volume_preserving_transvectionStruct`, `volume_real_Icc`, `volume_real_Icc_of_le`, `volume_real_Ico`, `volume_real_Ico_of_le`, `volume_real_Ioc`, `volume_real_Ioc_of_le`, `volume_real_Ioo`, `volume_real_Ioo_of_le`, `volume_real_ball`, `volume_real_closedBall`, `volume_real_interval`, `volume_singleton`, `volume_uIoc`, `volume_uIoo`, `volume_univ`, `volume_val`, `ae_of_mem_of_ae_of_mem_inter_Ioo`, `ae_restrict_of_ae_restrict_inter_Ioo`, `measurableSet_graph`, `measurableSet_regionBetween`, `measurableSet_region_between_cc`, `measurableSet_region_between_co`, `measurableSet_region_between_oc`, `nullMeasurableSet_regionBetween`, `nullMeasurableSet_region_between_cc`, `nullMeasurableSet_region_between_co`, `nullMeasurableSet_region_between_oc`, `regionBetween_subset`, `volume_regionBetween_eq_lintegral`, `volume_regionBetween_eq_lintegral'`	76
Total	77

Filter.Eventually

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`volume_pos_of_nhds_real` 📖	mathematical	`Filter.Eventually` `Real` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `Set` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `setOf`	—	`exists_Ioo_subset` `instOrderTopologyReal` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `instNoMinOrderOfNontrivial` `lt_imp_lt_of_le_of_le` `le_refl` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Real.volume_Ioo` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `LT.lt.trans`

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isFiniteMeasure_restrict_Icc` 📖	mathematical	—	`MeasureTheory.IsFiniteMeasure` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `MeasureTheory.Measure.restrict` `MeasureTheory.MeasureSpace.volume` `Set.Icc` `instPreorder`	—	`MeasureTheory.Measure.restrict_apply` `Set.univ_inter` `volume_Icc`
`isFiniteMeasure_restrict_Ico` 📖	mathematical	—	`MeasureTheory.IsFiniteMeasure` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `MeasureTheory.Measure.restrict` `MeasureTheory.MeasureSpace.volume` `Set.Ico` `instPreorder`	—	`MeasureTheory.Measure.restrict_apply` `Set.univ_inter` `volume_Ico`
`isFiniteMeasure_restrict_Ioc` 📖	mathematical	—	`MeasureTheory.IsFiniteMeasure` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `MeasureTheory.Measure.restrict` `MeasureTheory.MeasureSpace.volume` `Set.Ioc` `instPreorder`	—	`MeasureTheory.Measure.restrict_apply` `Set.univ_inter` `volume_Ioc`
`isFiniteMeasure_restrict_Ioo` 📖	mathematical	—	`MeasureTheory.IsFiniteMeasure` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `MeasureTheory.Measure.restrict` `MeasureTheory.MeasureSpace.volume` `Set.Ioo` `instPreorder`	—	`MeasureTheory.Measure.restrict_apply` `Set.univ_inter` `volume_Ioo`
`locallyFinite_volume` 📖	mathematical	—	`MeasureTheory.IsLocallyFiniteMeasure` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `MeasureTheory.MeasureSpace.volume`	—	`IsOpen.mem_nhds` `isOpen_Ioo` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `instIsOrderedAddMonoid` `sub_lt_self` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `zero_lt_one` `instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `lt_add_of_pos_right` `volume_Ioo`
`map_linearMap_volume_pi_eq_smul_volume_pi` 📖	mathematical	—	`MeasureTheory.Measure.map` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.MeasureSpace.pi` `Real` `measureSpace` `MeasurableSpace.pi` `measurableSpace` `DFunLike.coe` `LinearMap` `semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `instAddCommMonoid` `Pi.Function.module` `NormedSpace.toModule` `normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `InnerProductSpace.toNormedSpace` `instRCLike` `RCLike.toInnerProductSpaceReal` `LinearMap.instFunLike` `MeasureTheory.MeasureSpace.volume` `ENNReal` `MeasureTheory.Measure` `MeasureTheory.Measure.instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right` `ENNReal.ofReal` `abs` `lattice` `instAddGroup` `instInv` `MonoidHom` `CommRing.toCommSemiring` `commRing` `AddCommGroup.toAddCommMonoid` `Pi.addCommGroup` `instAddCommGroup` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring` `MonoidHom.instFunLike` `LinearMap.det`	—	`RingHomInvPair.ids` `Function.smulCommClass` `Algebra.to_smulCommClass` `LinearMap.det_toMatrix'` `Matrix.toLin'_toMatrix'` `IsScalarTower.right` `map_matrix_volume_pi_eq_smul_volume_pi`
`map_matrix_volume_pi_eq_smul_volume_pi` 📖	mathematical	—	`MeasureTheory.Measure.map` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.MeasureSpace.pi` `Real` `measureSpace` `MeasurableSpace.pi` `measurableSpace` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `instCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Pi.Function.module` `Semiring.toModule` `LinearMap.instFunLike` `LinearEquiv` `RingHomInvPair.ids` `Matrix` `Matrix.addCommMonoid` `LinearMap.addCommMonoid` `Matrix.module` `LinearMap.module` `Function.smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Algebra.to_smulCommClass` `Algebra.id` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Matrix.toLin'` `MeasureTheory.MeasureSpace.volume` `ENNReal` `MeasureTheory.Measure` `MeasureTheory.Measure.instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `IsScalarTower.right` `ENNReal.ofReal` `abs` `lattice` `instAddGroup` `instInv` `Matrix.det` `commRing`	—	`Matrix.diagonal_transvection_induction_of_det_ne_zero` `RingHomInvPair.ids` `Function.smulCommClass` `Algebra.to_smulCommClass` `IsScalarTower.right` `smul_map_diagonal_volume_pi` `smul_smul` `ENNReal.ofReal_mul` `abs_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `abs_mul` `instIsOrderedRing` `inv_mul_cancel₀` `abs_one` `ENNReal.ofReal_one` `one_smul` `Matrix.TransvectionStruct.det` `inv_one` `MeasureTheory.MeasurePreserving.map_eq` `volume_preserving_transvectionStruct` `RingHomCompTriple.ids` `Matrix.toLin'_mul` `Matrix.det_mul` `LinearMap.coe_comp` `MeasureTheory.Measure.map_map` `Continuous.measurable` `Pi.opensMeasurableSpace` `Finite.to_countable` `Finite.of_fintype` `instSecondCountableTopologyReal` `BorelSpace.opensMeasurable` `borelSpace` `Pi.borelSpace` `LinearMap.continuous_on_pi` `instContinuousAddForallOfIsTopologicalSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousSMulForall` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `MeasureTheory.Measure.map_smul` `mul_comm` `mul_inv`
`map_volume_mul_left` 📖	mathematical	—	`MeasureTheory.Measure.map` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `measurableSpace` `instMul` `MeasureTheory.MeasureSpace.volume` `ENNReal` `MeasureTheory.Measure` `MeasureTheory.Measure.instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right` `ENNReal.ofReal` `abs` `lattice` `instAddGroup` `instInv`	—	`IsScalarTower.right` `smul_map_volume_mul_left` `smul_smul` `ENNReal.ofReal_mul` `abs_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `abs_mul` `instIsOrderedRing` `inv_mul_cancel₀` `abs_one` `ENNReal.ofReal_one` `one_smul`
`map_volume_mul_right` 📖	mathematical	—	`MeasureTheory.Measure.map` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `measurableSpace` `instMul` `MeasureTheory.MeasureSpace.volume` `ENNReal` `MeasureTheory.Measure` `MeasureTheory.Measure.instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right` `ENNReal.ofReal` `abs` `lattice` `instAddGroup` `instInv`	—	`IsScalarTower.right` `mul_comm` `map_volume_mul_left`
`noAtoms_volume` 📖	mathematical	—	`MeasureTheory.NoAtoms` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `MeasureTheory.MeasureSpace.volume`	—	`volume_singleton`
`smul_map_diagonal_volume_pi` 📖	mathematical	—	`ENNReal` `MeasureTheory.Measure` `MeasurableSpace.pi` `Real` `measurableSpace` `MeasureTheory.Measure.instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right` `ENNReal.ofReal` `abs` `lattice` `instAddGroup` `Matrix.det` `commRing` `Matrix.diagonal` `instZero` `MeasureTheory.Measure.map` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.MeasureSpace.pi` `measureSpace` `DFunLike.coe` `LinearMap` `instCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Pi.Function.module` `Semiring.toModule` `LinearMap.instFunLike` `LinearEquiv` `RingHomInvPair.ids` `Matrix` `Matrix.addCommMonoid` `LinearMap.addCommMonoid` `Matrix.module` `LinearMap.module` `Function.smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Algebra.to_smulCommClass` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Matrix.toLin'` `MeasureTheory.MeasureSpace.volume`	—	`IsScalarTower.right` `RingHomInvPair.ids` `Function.smulCommClass` `Algebra.to_smulCommClass` `MeasureTheory.Measure.pi_eq` `MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite` `instIsAddHaarMeasureVolume` `FiniteDimensional.rclike_to_real` `borelSpace` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `instIsTopologicalAddGroupReal` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instSecondCountableTopologyReal` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `instProperSpaceReal` `Matrix.det_diagonal` `Finset.prod_congr` `MeasureTheory.Measure.map_apply` `Continuous.measurable` `Pi.opensMeasurableSpace` `Finite.to_countable` `Finite.of_fintype` `BorelSpace.opensMeasurable` `Pi.borelSpace` `LinearMap.continuous_on_pi` `instContinuousAddForallOfIsTopologicalSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousSMulForall` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `MeasurableSet.univ_pi` `Set.ext` `Matrix.diagonal_toLin'` `Finset.prod_ne_zero_iff` `instNontrivial` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Finset.mem_univ` `volume_preimage_mul_left` `mul_assoc` `ENNReal.ofReal_mul` `abs_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `abs_mul` `instIsOrderedRing` `mul_inv_cancel₀` `abs_one` `ENNReal.ofReal_one` `one_mul` `MeasureTheory.volume_pi_pi` `Finset.abs_prod` `instIsStrictOrderedRing` `ENNReal.ofReal_prod_of_nonneg` `Finset.prod_mul_distrib`
`smul_map_volume_mul_left` 📖	mathematical	—	`ENNReal` `MeasureTheory.Measure` `Real` `measurableSpace` `MeasureTheory.Measure.instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right` `ENNReal.ofReal` `abs` `lattice` `instAddGroup` `MeasureTheory.Measure.map` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `instMul` `MeasureTheory.MeasureSpace.volume`	—	`IsScalarTower.right` `measure_ext_Ioo_rat` `locallyFinite_volume` `lt_or_gt_of_ne` `volume_Ioo` `abs_of_neg` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `MeasureTheory.Measure.map_apply` `MeasurableMul.measurable_const_mul` `ContinuousMul.measurableMul` `borelSpace` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `measurableSet_Ioo` `BorelSpace.opensMeasurable` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Set.preimage_const_mul_Ioo_of_neg` `instIsStrictOrderedRing` `ENNReal.ofReal_mul` `le_of_lt` `neg_pos` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `mul_sub` `neg_mul` `mul_div_cancel₀` `ne_of_lt` `neg_sub_neg` `abs_of_pos` `Set.preimage_const_mul_Ioo₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `ne_of_gt`
`smul_map_volume_mul_right` 📖	mathematical	—	`ENNReal` `MeasureTheory.Measure` `Real` `measurableSpace` `MeasureTheory.Measure.instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right` `ENNReal.ofReal` `abs` `lattice` `instAddGroup` `MeasureTheory.Measure.map` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `instMul` `MeasureTheory.MeasureSpace.volume`	—	`IsScalarTower.right` `mul_comm` `smul_map_volume_mul_left`
`volume_Icc` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Set.Icc` `instPreorder` `ENNReal.ofReal` `instSub`	—	`instOrderTopologyReal` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `borelSpace` `instSecondCountableTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `volume_val` `StieltjesFunction.measure_Icc` `StieltjesFunction.id_leftLim`
`volume_Icc_pi` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.MeasureSpace.pi` `Real` `measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Set.Icc` `Pi.preorder` `instPreorder` `Finset.prod` `CommSemiring.toCommMonoid` `ENNReal.instCommSemiring` `Finset.univ` `ENNReal.ofReal` `instSub`	—	`Set.pi_univ_Icc` `MeasureTheory.volume_pi_pi` `MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite` `instIsAddHaarMeasureVolume` `FiniteDimensional.rclike_to_real` `borelSpace` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `instIsTopologicalAddGroupReal` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instSecondCountableTopologyReal` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `instProperSpaceReal` `Finset.prod_congr` `volume_Icc`
`volume_Icc_pi_toReal` 📖	mathematical	`Pi.hasLe` `Real` `instLE`	`ENNReal.toReal` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.MeasureSpace.pi` `measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Set.Icc` `Pi.preorder` `instPreorder` `Finset.prod` `instCommMonoid` `Finset.univ` `instSub`	—	`volume_Icc_pi` `ENNReal.toReal_prod` `Finset.prod_congr` `ENNReal.toReal_ofReal` `sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid`
`volume_Ici` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Set.Ici` `instPreorder` `Top.top` `instTopENNReal`	—	`MeasureTheory.measure_congr` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Ioi_ae_eq_Ici` `noAtoms_volume` `volume_Ioi`
`volume_Ico` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Set.Ico` `instPreorder` `ENNReal.ofReal` `instSub`	—	`instOrderTopologyReal` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `borelSpace` `instSecondCountableTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `volume_val` `StieltjesFunction.measure_Ico` `StieltjesFunction.id_leftLim`
`volume_Iic` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Set.Iic` `instPreorder` `Top.top` `instTopENNReal`	—	`MeasureTheory.measure_congr` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Iio_ae_eq_Iic` `noAtoms_volume` `volume_Iio`
`volume_Iio` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Set.Iio` `instPreorder` `Top.top` `instTopENNReal`	—	`top_unique` `le_of_tendsto'` `instClosedIicTopology` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `ENNReal.tendsto_nat_nhds_top` `volume_Ioo` `sub_sub_cancel` `ENNReal.ofReal_natCast` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Set.Ioo_subset_Iio_self`
`volume_Ioc` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Set.Ioc` `instPreorder` `ENNReal.ofReal` `instSub`	—	`instOrderTopologyReal` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `borelSpace` `instSecondCountableTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `volume_val` `StieltjesFunction.measure_Ioc`
`volume_Ioi` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Set.Ioi` `instPreorder` `Top.top` `instTopENNReal`	—	`top_unique` `le_of_tendsto'` `instClosedIicTopology` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `ENNReal.tendsto_nat_nhds_top` `volume_Ioo` `add_sub_cancel_left` `ENNReal.ofReal_natCast` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Set.Ioo_subset_Ioi_self`
`volume_Ioo` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Set.Ioo` `instPreorder` `ENNReal.ofReal` `instSub`	—	`instOrderTopologyReal` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `borelSpace` `instSecondCountableTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `volume_val` `StieltjesFunction.measure_Ioo` `StieltjesFunction.id_leftLim`
`volume_ball` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Metric.ball` `pseudoMetricSpace` `ENNReal.ofReal` `instMul` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `ball_eq_Ioo` `volume_Ioo` `sub_add` `add_sub_cancel_left` `two_mul`
`volume_closedBall` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Metric.closedBall` `pseudoMetricSpace` `ENNReal.ofReal` `instMul` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `closedBall_eq_Icc` `volume_Icc` `sub_add` `add_sub_cancel_left` `two_mul`
`volume_closedEBall` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Metric.closedEBall` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `metricSpace` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `eq_or_ne` `Metric.closedEBall_top` `volume_univ` `two_mul` `top_add` `CanLift.prf` `ENNReal.canLift` `Metric.closedEBall_coe` `volume_closedBall` `NNReal.coe_add` `ENNReal.ofReal_coe_nnreal` `ENNReal.coe_add`
`volume_eball` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `metricSpace` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `eq_or_ne` `Metric.eball_top` `volume_univ` `two_mul` `top_add` `CanLift.prf` `ENNReal.canLift` `Metric.eball_coe` `volume_ball` `NNReal.coe_add` `ENNReal.ofReal_coe_nnreal` `ENNReal.coe_add`
`volume_emetric_ball` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `metricSpace` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat`	—	`volume_eball`
`volume_emetric_closedBall` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Metric.closedEBall` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `metricSpace` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat`	—	`volume_closedEBall`
`volume_eq_stieltjes_id` 📖	mathematical	—	`MeasureTheory.MeasureSpace.volume` `Real` `measureSpace` `StieltjesFunction.measure` `linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `StieltjesFunction.id` `instOrderTopologyReal` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `instConditionallyCompleteLinearOrder` `measurableSpace` `borelSpace` `instSecondCountableTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `Field.toSemifield` `instField` `partialOrder` `PosMulReflectLE.toPosMulReflectLT` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `normedCommRing` `PosMulStrictMono.toPosMulReflectLE` `MulZeroClass.toMul` `MulZeroClass.toZero` `IsStrictOrderedRing.toPosMulStrictMono` `semiring` `instIsStrictOrderedRing`	—	`instOrderTopologyReal` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `borelSpace` `instSecondCountableTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `FiniteDimensional.rclike_to_real` `parallelepiped_orthonormalBasis_one_dim` `StieltjesFunction.measure_Icc` `StieltjesFunction.id_leftLim` `tsub_zero` `AddGroup.toOrderedSub` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `ENNReal.ofReal_one` `sub_neg_eq_add` `zero_add` `IsScalarTower.right` `instIsTopologicalAddGroupReal` `MeasureTheory.Measure.addHaarMeasure_unique` `MeasureTheory.sigmaFinite_of_locallyFinite` `StieltjesFunction.instIsLocallyFiniteMeasure` `measure_ext_Ioo_rat` `StieltjesFunction.measure_Ioo` `MeasureTheory.Measure.map_apply` `MeasurableAdd.measurable_const_add` `ContinuousAdd.measurableAdd` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `measurableSet_Ioo` `BorelSpace.opensMeasurable` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Set.preimage_const_add_Ioo` `sub_sub_sub_cancel_right` `Module.Basis.addHaar_def` `one_smul`
`volume_interval` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Set.uIcc` `lattice` `ENNReal.ofReal` `abs` `instAddGroup` `instSub`	—	`Set.Icc_min_max` `volume_Icc` `max_sub_min_eq_abs` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add`
`volume_le_diam` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `Set` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Metric.ediam` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `metricSpace`	—	`ediam_eq` `volume_Icc` `MeasureTheory.OuterMeasure.mono` `Bornology.IsBounded.subset_Icc_sInf_sSup` `instIsOrderBornology` `Metric.ediam_of_unbounded` `le_top`
`volume_pi_Ico` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.MeasureSpace.pi` `Real` `measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Set.pi` `Set.univ` `Set.Ico` `instPreorder` `Finset.prod` `CommSemiring.toCommMonoid` `ENNReal.instCommSemiring` `Finset.univ` `ENNReal.ofReal` `instSub`	—	`MeasureTheory.measure_congr` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.univ_pi_Ico_ae_eq_Icc` `MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite` `instIsAddHaarMeasureVolume` `FiniteDimensional.rclike_to_real` `borelSpace` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `instIsTopologicalAddGroupReal` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instSecondCountableTopologyReal` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `instProperSpaceReal` `noAtoms_volume` `volume_Icc_pi`
`volume_pi_Ico_toReal` 📖	mathematical	`Pi.hasLe` `Real` `instLE`	`ENNReal.toReal` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.MeasureSpace.pi` `measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Set.pi` `Set.univ` `Set.Ico` `instPreorder` `Finset.prod` `instCommMonoid` `Finset.univ` `instSub`	—	`volume_pi_Ico` `ENNReal.toReal_prod` `Finset.prod_congr` `ENNReal.toReal_ofReal` `sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid`
`volume_pi_Ioc` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.MeasureSpace.pi` `Real` `measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Set.pi` `Set.univ` `Set.Ioc` `instPreorder` `Finset.prod` `CommSemiring.toCommMonoid` `ENNReal.instCommSemiring` `Finset.univ` `ENNReal.ofReal` `instSub`	—	`MeasureTheory.measure_congr` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.univ_pi_Ioc_ae_eq_Icc` `MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite` `instIsAddHaarMeasureVolume` `FiniteDimensional.rclike_to_real` `borelSpace` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `instIsTopologicalAddGroupReal` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instSecondCountableTopologyReal` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `instProperSpaceReal` `noAtoms_volume` `volume_Icc_pi`
`volume_pi_Ioc_toReal` 📖	mathematical	`Pi.hasLe` `Real` `instLE`	`ENNReal.toReal` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.MeasureSpace.pi` `measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Set.pi` `Set.univ` `Set.Ioc` `instPreorder` `Finset.prod` `instCommMonoid` `Finset.univ` `instSub`	—	`volume_pi_Ioc` `ENNReal.toReal_prod` `Finset.prod_congr` `ENNReal.toReal_ofReal` `sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid`
`volume_pi_Ioo` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.MeasureSpace.pi` `Real` `measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Set.pi` `Set.univ` `Set.Ioo` `instPreorder` `Finset.prod` `CommSemiring.toCommMonoid` `ENNReal.instCommSemiring` `Finset.univ` `ENNReal.ofReal` `instSub`	—	`MeasureTheory.measure_congr` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.univ_pi_Ioo_ae_eq_Icc` `MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite` `instIsAddHaarMeasureVolume` `FiniteDimensional.rclike_to_real` `borelSpace` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `instIsTopologicalAddGroupReal` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instSecondCountableTopologyReal` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `instProperSpaceReal` `noAtoms_volume` `volume_Icc_pi`
`volume_pi_Ioo_toReal` 📖	mathematical	`Pi.hasLe` `Real` `instLE`	`ENNReal.toReal` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.MeasureSpace.pi` `measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Set.pi` `Set.univ` `Set.Ioo` `instPreorder` `Finset.prod` `instCommMonoid` `Finset.univ` `instSub`	—	`volume_pi_Ioo` `ENNReal.toReal_prod` `Finset.prod_congr` `ENNReal.toReal_ofReal` `sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid`
`volume_pi_ball` 📖	mathematical	`Real` `instLT` `instZero`	`DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.MeasureSpace.pi` `measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Metric.ball` `pseudoMetricSpacePi` `pseudoMetricSpace` `ENNReal.ofReal` `Monoid.toNatPow` `instMonoid` `instMul` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Fintype.card`	—	`Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.volume_pi_ball` `MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite` `instIsAddHaarMeasureVolume` `FiniteDimensional.rclike_to_real` `borelSpace` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `instIsTopologicalAddGroupReal` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instSecondCountableTopologyReal` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `instProperSpaceReal` `Finset.prod_congr` `volume_ball` `Finset.prod_const` `ENNReal.ofReal_pow` `mul_nonneg` `IsOrderedRing.toPosMulMono` `instIsOrderedRing` `zero_le_two` `instZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `LT.lt.le`
`volume_pi_closedBall` 📖	mathematical	`Real` `instLE` `instZero`	`DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.MeasureSpace.pi` `measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Metric.closedBall` `pseudoMetricSpacePi` `pseudoMetricSpace` `ENNReal.ofReal` `Monoid.toNatPow` `instMonoid` `instMul` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Fintype.card`	—	`Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.volume_pi_closedBall` `MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite` `instIsAddHaarMeasureVolume` `FiniteDimensional.rclike_to_real` `borelSpace` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `instIsTopologicalAddGroupReal` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instSecondCountableTopologyReal` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `instProperSpaceReal` `Finset.prod_congr` `volume_closedBall` `Finset.prod_const` `ENNReal.ofReal_pow` `mul_nonneg` `IsOrderedRing.toPosMulMono` `instIsOrderedRing` `zero_le_two` `instZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid`
`volume_pi_le_diam_pow` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.MeasureSpace.pi` `Real` `measureSpace` `Set` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Metric.ediam` `pseudoEMetricSpacePi` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `metricSpace` `Fintype.card`	—	`volume_pi_le_prod_diam` `Finset.prod_le_prod'` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `LipschitzWith.ediam_image_le` `LipschitzWith.eval` `Finset.prod_congr` `one_mul` `Finset.prod_const`
`volume_pi_le_prod_diam` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.MeasureSpace.pi` `Real` `measureSpace` `Set` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Finset.prod` `CommSemiring.toCommMonoid` `ENNReal.instCommSemiring` `Finset.univ` `Metric.ediam` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `metricSpace` `Set.image` `Function.eval`	—	`MeasureTheory.OuterMeasure.mono` `Set.Subset.trans` `Set.subset_pi_eval_image` `Set.pi_mono` `subset_closure` `MeasureTheory.volume_pi_pi` `MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite` `instIsAddHaarMeasureVolume` `FiniteDimensional.rclike_to_real` `borelSpace` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `instIsTopologicalAddGroupReal` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instSecondCountableTopologyReal` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `instProperSpaceReal` `Finset.prod_le_prod'` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `LE.le.trans_eq` `volume_le_diam` `Metric.ediam_closure`
`volume_preimage_mul_left` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Set.preimage` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofReal` `abs` `lattice` `instAddGroup` `instInv`	—	`borelSpace` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `MeasurableEquiv.map_apply` `IsScalarTower.right` `map_volume_mul_left`
`volume_preimage_mul_right` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Set.preimage` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofReal` `abs` `lattice` `instAddGroup` `instInv`	—	`borelSpace` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `MeasurableEquiv.map_apply` `IsScalarTower.right` `map_volume_mul_right`
`volume_preserving_transvectionStruct` 📖	mathematical	—	`MeasureTheory.MeasurePreserving` `MeasurableSpace.pi` `Real` `measurableSpace` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `instCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Pi.Function.module` `Semiring.toModule` `LinearMap.instFunLike` `LinearEquiv` `RingHomInvPair.ids` `Matrix` `Matrix.addCommMonoid` `LinearMap.addCommMonoid` `Matrix.module` `LinearMap.module` `Function.smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Algebra.to_smulCommClass` `Algebra.id` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Matrix.toLin'` `Matrix.TransvectionStruct.toMatrix` `commRing` `MeasureTheory.MeasureSpace.volume` `MeasureTheory.MeasureSpace.pi` `measureSpace`	—	`RingHomInvPair.ids` `Function.smulCommClass` `Algebra.to_smulCommClass` `Continuous.measurable` `Pi.opensMeasurableSpace` `Finite.to_countable` `Finite.of_fintype` `instSecondCountableTopologyReal` `BorelSpace.opensMeasurable` `borelSpace` `Pi.borelSpace` `LinearMap.continuous_of_finiteDimensional` `Pi.topologicalAddGroup` `instIsTopologicalAddGroupReal` `instContinuousSMulForall` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instCompleteSpace` `Pi.t2Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `FiniteDimensional.finiteDimensional_pi'` `FiniteDimensional.rclike_to_real` `MeasureTheory.Measure.pi_eq` `MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite` `instIsAddHaarMeasureVolume` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `instProperSpaceReal` `MeasurableSet.pi` `Set.countable_univ` `Finset.prod_congr` `MeasureTheory.lintegral_indicator_one` `MeasureTheory.lintegral_map` `Measurable.indicator` `measurable_one` `MeasureTheory.volume_pi` `MeasureTheory.lintegral_eq_of_lmarginal_eq` `Measurable.comp` `MeasureTheory.lmarginal_singleton` `map_add` `SemilinearMapClass.toAddHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `Matrix.toLin'_one` `Matrix.single_mulVec` `Function.update_of_ne` `add_zero` `MeasureTheory.lintegral_add_right_eq_self` `ContinuousAdd.measurableAdd` `IsTopologicalSemiring.toContinuousAdd` `MeasureTheory.IsAddLeftInvariant.isAddRightInvariant` `MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant`
`volume_real_Icc` 📖	mathematical	—	`MeasureTheory.Measure.real` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `MeasureTheory.MeasureSpace.volume` `Set.Icc` `instPreorder` `instMax` `instSub` `instZero`	—	`volume_Icc`
`volume_real_Icc_of_le` 📖	mathematical	`Real` `instLE`	`MeasureTheory.Measure.real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `MeasureTheory.MeasureSpace.volume` `Set.Icc` `instPreorder` `instSub`	—	`volume_real_Icc` `sup_of_le_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid`
`volume_real_Ico` 📖	mathematical	—	`MeasureTheory.Measure.real` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `MeasureTheory.MeasureSpace.volume` `Set.Ico` `instPreorder` `instMax` `instSub` `instZero`	—	`volume_Ico`
`volume_real_Ico_of_le` 📖	mathematical	`Real` `instLE`	`MeasureTheory.Measure.real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `MeasureTheory.MeasureSpace.volume` `Set.Ico` `instPreorder` `instSub`	—	`volume_real_Ico` `sup_of_le_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid`
`volume_real_Ioc` 📖	mathematical	—	`MeasureTheory.Measure.real` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `MeasureTheory.MeasureSpace.volume` `Set.Ioc` `instPreorder` `instMax` `instSub` `instZero`	—	`volume_Ioc`
`volume_real_Ioc_of_le` 📖	mathematical	`Real` `instLE`	`MeasureTheory.Measure.real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `MeasureTheory.MeasureSpace.volume` `Set.Ioc` `instPreorder` `instSub`	—	`volume_real_Ioc` `sup_of_le_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid`
`volume_real_Ioo` 📖	mathematical	—	`MeasureTheory.Measure.real` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `MeasureTheory.MeasureSpace.volume` `Set.Ioo` `instPreorder` `instMax` `instSub` `instZero`	—	`volume_Ioo`
`volume_real_Ioo_of_le` 📖	mathematical	`Real` `instLE`	`MeasureTheory.Measure.real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `MeasureTheory.MeasureSpace.volume` `Set.Ioo` `instPreorder` `instSub`	—	`volume_real_Ioo` `sup_of_le_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid`
`volume_real_ball` 📖	mathematical	`Real` `instLE` `instZero`	`MeasureTheory.Measure.real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `MeasureTheory.MeasureSpace.volume` `Metric.ball` `pseudoMetricSpace` `instMul` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `volume_ball` `ENNReal.ofReal_mul` `instIsOrderedRing` `ENNReal.ofReal_ofNat` `ENNReal.toReal_mul` `ENNReal.toReal_ofNat` `ENNReal.toReal_ofReal`
`volume_real_closedBall` 📖	mathematical	`Real` `instLE` `instZero`	`MeasureTheory.Measure.real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `MeasureTheory.MeasureSpace.volume` `Metric.closedBall` `pseudoMetricSpace` `instMul` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `volume_closedBall` `ENNReal.ofReal_mul` `instIsOrderedRing` `ENNReal.ofReal_ofNat` `ENNReal.toReal_mul` `ENNReal.toReal_ofNat` `ENNReal.toReal_ofReal`
`volume_real_interval` 📖	mathematical	—	`MeasureTheory.Measure.real` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `MeasureTheory.MeasureSpace.volume` `Set.uIcc` `lattice` `abs` `instAddGroup` `instSub`	—	`volume_interval` `ENNReal.toReal_ofReal` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add`
`volume_singleton` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Set.instSingletonSet` `instZeroENNReal`	—	`MeasureTheory.NoAtoms.measure_singleton` `MeasureTheory.Measure.IsAddHaarMeasure.noAtoms` `instIsTopologicalAddGroupReal` `borelSpace` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `instProperSpaceReal` `punctured_nhds_module_neBot` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instNontrivial` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `instIsAddHaarMeasureVolume` `FiniteDimensional.rclike_to_real`
`volume_uIoc` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Set.uIoc` `linearOrder` `ENNReal.ofReal` `abs` `lattice` `instAddGroup` `instSub`	—	`volume_Ioc` `max_sub_min_eq_abs` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add`
`volume_uIoo` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Set.uIoo` `linearOrder` `ENNReal.ofReal` `abs` `lattice` `instAddGroup` `instSub`	—	`volume_Ioo` `max_sub_min_eq_abs` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add`
`volume_univ` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Set.univ` `Top.top` `instTopENNReal`	—	`ENNReal.eq_top_of_forall_nnreal_le` `volume_Icc` `sub_zero` `ENNReal.ofReal_coe_nnreal` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Set.subset_univ`
`volume_val` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `measurableSpace` `StieltjesFunction.measure` `linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `StieltjesFunction.id` `instOrderTopologyReal` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `instConditionallyCompleteLinearOrder` `borelSpace` `instSecondCountableTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `Field.toSemifield` `instField` `partialOrder` `PosMulReflectLE.toPosMulReflectLT` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `normedCommRing` `PosMulStrictMono.toPosMulReflectLE` `MulZeroClass.toMul` `MulZeroClass.toZero` `IsStrictOrderedRing.toPosMulStrictMono` `semiring` `instIsStrictOrderedRing`	—	`instOrderTopologyReal` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `borelSpace` `instSecondCountableTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `volume_eq_stieltjes_id`

(root)

Definitions

Name	Category	Theorems
`regionBetween` 📖	CompOp	6 math math: `volume_regionBetween_eq_lintegral'`, `regionBetween_subset`, `measurableSet_regionBetween`, `volume_regionBetween_eq_integral'`, `volume_regionBetween_eq_integral`, `volume_regionBetween_eq_lintegral`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_of_mem_of_ae_of_mem_inter_Ioo` 📖	—	`Filter.Eventually` `Real` `MeasureTheory.ae` `MeasureTheory.Measure` `Real.measurableSpace` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	—	`MeasureTheory.Measure.instOuterMeasureClass` `Set.finite_diff_iUnion_Ioo'` `TopologicalSpace.isOpen_iUnion_countable` `instSecondCountableTopologyReal` `isOpen_Ioo` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Set.Countable.ae_notMem` `Set.Finite.countable` `MeasureTheory.ae_ball_iff` `le_or_gt` `Set.Ioo_eq_empty_of_le` `Set.inter_empty` `instIsEmptyFalse` `Filter.mp_mem` `Filter.univ_mem'`
`ae_restrict_of_ae_restrict_inter_Ioo` 📖	—	`Filter.Eventually` `Real` `MeasureTheory.ae` `MeasureTheory.Measure` `Real.measurableSpace` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.restrict` `Set` `Set.instInter` `Set.Ioo` `Real.instPreorder`	—	—	`MeasureTheory.Measure.instOuterMeasureClass` `Set.finite_diff_iUnion_Ioo'` `TopologicalSpace.isOpen_iUnion_countable` `instSecondCountableTopologyReal` `isOpen_Ioo` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Set.mem_biUnion` `MeasureTheory.ae_restrict_of_ae_restrict_of_subset` `MeasureTheory.ae_restrict_union_iff` `MeasureTheory.ae_restrict_biUnion_iff` `Set.Finite.measure_zero` `MeasureTheory.ae.congr_simp` `MeasureTheory.ae_zero` `le_or_gt` `Set.Ioo_eq_empty_of_le` `Set.inter_empty` `MeasureTheory.Measure.restrict_empty`
`measurableSet_graph` 📖	mathematical	`Measurable` `Real` `Real.measurableSpace`	`MeasurableSet` `Prod.instMeasurableSpace` `setOf`	—	`Set.Icc_self` `measurableSet_region_between_cc` `MeasurableSet.univ`
`measurableSet_regionBetween` 📖	mathematical	`Measurable` `Real` `Real.measurableSpace` `MeasurableSet`	`Prod.instMeasurableSpace` `regionBetween`	—	`MeasurableSet.inter` `measurable_fst` `measurableSet_lt` `BorelSpace.opensMeasurable` `Real.borelSpace` `instSecondCountableTopologyReal` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Measurable.comp` `measurable_snd`
`measurableSet_region_between_cc` 📖	mathematical	`Measurable` `Real` `Real.measurableSpace` `MeasurableSet`	`Prod.instMeasurableSpace` `setOf` `Set` `Set.instMembership` `Set.Icc` `Real.instPreorder`	—	`MeasurableSet.inter` `measurable_fst` `measurableSet_le` `BorelSpace.opensMeasurable` `Real.borelSpace` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `instSecondCountableTopologyReal` `Measurable.comp` `measurable_snd`
`measurableSet_region_between_co` 📖	mathematical	`Measurable` `Real` `Real.measurableSpace` `MeasurableSet`	`Prod.instMeasurableSpace` `setOf` `Set` `Set.instMembership` `Set.Ico` `Real.instPreorder`	—	`MeasurableSet.inter` `measurable_fst` `measurableSet_le` `BorelSpace.opensMeasurable` `Real.borelSpace` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `instSecondCountableTopologyReal` `Measurable.comp` `measurable_snd` `measurableSet_lt`
`measurableSet_region_between_oc` 📖	mathematical	`Measurable` `Real` `Real.measurableSpace` `MeasurableSet`	`Prod.instMeasurableSpace` `setOf` `Set` `Set.instMembership` `Set.Ioc` `Real.instPreorder`	—	`MeasurableSet.inter` `measurable_fst` `measurableSet_lt` `BorelSpace.opensMeasurable` `Real.borelSpace` `instSecondCountableTopologyReal` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Measurable.comp` `measurable_snd` `measurableSet_le`
`nullMeasurableSet_regionBetween` 📖	mathematical	`AEMeasurable` `Real` `Real.measurableSpace` `MeasureTheory.NullMeasurableSet`	`Prod.instMeasurableSpace` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `setOf` `Set` `Set.instMembership` `Set.Ioo` `Real.instPreorder` `MeasureTheory.Measure.prod` `MeasureTheory.MeasureSpace.volume`	—	`MeasureTheory.NullMeasurableSet.inter` `MeasureTheory.NullMeasurableSet.preimage` `MeasureTheory.Measure.quasiMeasurePreserving_fst` `nullMeasurableSet_lt` `BorelSpace.opensMeasurable` `Real.borelSpace` `instSecondCountableTopologyReal` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `AEMeasurable.comp_quasiMeasurePreserving` `MeasureTheory.QuasiMeasurePreserving.fst` `MeasureTheory.Measure.QuasiMeasurePreserving.id` `Measurable.aemeasurable` `measurable_snd`
`nullMeasurableSet_region_between_cc` 📖	mathematical	`AEMeasurable` `Real` `Real.measurableSpace` `MeasureTheory.NullMeasurableSet`	`Prod.instMeasurableSpace` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `setOf` `Set` `Set.instMembership` `Set.Icc` `Real.instPreorder` `MeasureTheory.Measure.prod` `MeasureTheory.MeasureSpace.volume`	—	`MeasureTheory.NullMeasurableSet.inter` `MeasureTheory.NullMeasurableSet.preimage` `MeasureTheory.Measure.quasiMeasurePreserving_fst` `Set.ext` `MeasureTheory.NullMeasurableSet.compl` `nullMeasurableSet_lt` `BorelSpace.opensMeasurable` `Real.borelSpace` `instSecondCountableTopologyReal` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Measurable.aemeasurable` `measurable_snd` `AEMeasurable.comp_quasiMeasurePreserving` `MeasureTheory.QuasiMeasurePreserving.fst` `MeasureTheory.Measure.QuasiMeasurePreserving.id`
`nullMeasurableSet_region_between_co` 📖	mathematical	`AEMeasurable` `Real` `Real.measurableSpace` `MeasureTheory.NullMeasurableSet`	`Prod.instMeasurableSpace` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `setOf` `Set` `Set.instMembership` `Set.Ico` `Real.instPreorder` `MeasureTheory.Measure.prod` `MeasureTheory.MeasureSpace.volume`	—	`MeasureTheory.NullMeasurableSet.inter` `MeasureTheory.NullMeasurableSet.preimage` `MeasureTheory.Measure.quasiMeasurePreserving_fst` `Set.ext` `MeasureTheory.NullMeasurableSet.compl` `nullMeasurableSet_lt` `BorelSpace.opensMeasurable` `Real.borelSpace` `instSecondCountableTopologyReal` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Measurable.aemeasurable` `measurable_snd` `AEMeasurable.comp_quasiMeasurePreserving` `MeasureTheory.QuasiMeasurePreserving.fst` `MeasureTheory.Measure.QuasiMeasurePreserving.id`
`nullMeasurableSet_region_between_oc` 📖	mathematical	`AEMeasurable` `Real` `Real.measurableSpace` `MeasureTheory.NullMeasurableSet`	`Prod.instMeasurableSpace` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `setOf` `Set` `Set.instMembership` `Set.Ioc` `Real.instPreorder` `MeasureTheory.Measure.prod` `MeasureTheory.MeasureSpace.volume`	—	`MeasureTheory.NullMeasurableSet.inter` `MeasureTheory.NullMeasurableSet.preimage` `MeasureTheory.Measure.quasiMeasurePreserving_fst` `nullMeasurableSet_lt` `BorelSpace.opensMeasurable` `Real.borelSpace` `instSecondCountableTopologyReal` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `AEMeasurable.comp_quasiMeasurePreserving` `MeasureTheory.QuasiMeasurePreserving.fst` `MeasureTheory.Measure.QuasiMeasurePreserving.id` `Measurable.aemeasurable` `measurable_snd` `Set.ext` `MeasureTheory.NullMeasurableSet.compl`
`regionBetween_subset` 📖	mathematical	—	`Set` `Real` `Set.instHasSubset` `regionBetween` `SProd.sprod` `Set.instSProd` `Set.univ`	—	`Set.prod_univ`
`volume_regionBetween_eq_lintegral` 📖	mathematical	`AEMeasurable` `Real` `Real.measurableSpace` `MeasureTheory.Measure.restrict` `MeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.prod` `MeasureTheory.MeasureSpace.volume` `regionBetween` `MeasureTheory.lintegral` `ENNReal.ofReal` `Pi.instSub` `Real.instSub`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Filter.EventuallyEq.fun_comp` `Filter.EventuallyEq.sub` `MeasureTheory.measure_congr` `Filter.EventuallyEq.inter` `Filter.EventuallyEq.rfl` `Filter.EventuallyEq.comp₂` `MeasureTheory.Measure.QuasiMeasurePreserving.ae_eq_comp` `MeasureTheory.Measure.quasiMeasurePreserving_fst` `MeasureTheory.lintegral_congr_ae` `volume_regionBetween_eq_lintegral'` `MeasureTheory.Measure.restrict_prod_eq_prod_univ` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite` `instIsAddHaarMeasureVolume` `FiniteDimensional.rclike_to_real` `Real.borelSpace` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `instIsTopologicalAddGroupReal` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instSecondCountableTopologyReal` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `instProperSpaceReal` `MeasureTheory.Measure.restrict_eq_self` `regionBetween_subset`
`volume_regionBetween_eq_lintegral'` 📖	mathematical	`Measurable` `Real` `Real.measurableSpace` `MeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.prod` `MeasureTheory.MeasureSpace.volume` `regionBetween` `MeasureTheory.lintegral` `MeasureTheory.Measure.restrict` `ENNReal.ofReal` `Pi.instSub` `Real.instSub`	—	`MeasureTheory.Measure.prod_apply` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite` `instIsAddHaarMeasureVolume` `FiniteDimensional.rclike_to_real` `Real.borelSpace` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `instIsTopologicalAddGroupReal` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instSecondCountableTopologyReal` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `instProperSpaceReal` `measurableSet_regionBetween` `Set.indicator_apply` `Real.volume_Ioo` `MeasureTheory.measure_empty` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.lintegral_indicator`

---

← Back to Index