Documentation Verification Report

Integrability

📁 Source: Mathlib/Analysis/BoxIntegral/Integrability.lean

Statistics

Metric	Count
Definitions	0
Theorems `congr_ae`, `of_aeEq_zero`, `hasIntegralIndicatorConst`, `hasBoxIntegral`, `hasBoxIntegral`, `hasBoxIntegral`, `box_integral_eq_integral`, `hasBoxIntegral`	8
Total	8

BoxIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasIntegralIndicatorConst` 📖	bridging (sound)	`IntegrationParams.bRiemann` `MeasurableSet` `MeasurableSpace.pi` `Real` `Real.measurableSpace`	`HasIntegral` `Set.indicator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `BoxAdditiveMap.toSMul` `Top.top` `WithTop` `Box` `WithTop.top` `MeasureTheory.Measure.toBoxAdditive` `Finite.of_fintype` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `MeasureTheory.Measure.real` `Set` `Set.instInter` `Box.toSet`	`IntegrationParams.bRiemann`	`HasIntegral.of_mul` `Finite.of_fintype` `CanLift.prf` `NNReal.canLift` `LT.lt.le` `LT.lt.ne` `LE.le.trans_lt` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Set.inter_subset_right` `Box.measure_Icc_lt_top` `Box.measure_coe_lt_top` `MeasurableSet.exists_isClosed_diff_lt` `Pi.opensMeasurableSpace` `Finite.to_countable` `instSecondCountableTopologyReal` `BorelSpace.opensMeasurable` `Real.borelSpace` `MeasureTheory.Measure.WeaklyRegular.of_pseudoMetrizableSpace_secondCountable_of_locallyFinite` `TopologicalSpace.pseudoMetrizableSpace_pi` `PseudoEMetricSpace.pseudoMetrizableSpace` `TopologicalSpace.instSecondCountableTopologyForallOfCountable` `Pi.borelSpace` `MeasurableSet.inter` `Box.measurableSet_Icc` `LT.lt.ne'` `ENNReal.coe_pos` `NNReal.coe_pos` `MeasurableSet.exists_isOpen_diff_lt` `MeasureTheory.Measure.WeaklyRegular.toOuterRegular` `Filter.HasBasis.mem_iff` `Metric.nhds_basis_closedBall` `IsOpen.mem_nhds` `IsClosed.isOpen_compl` `IntegrationParams.rCond_of_bRiemann_eq_false` `mul_comm` `Finset.sum_congr` `Finset.sum_indicator_eq_sum_filter` `dist_eq_norm` `norm_smul` `NormedSpace.toNormSMulClass` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `Set.iUnion_congr_Prop` `TaggedPrepartition.tag_mem_Icc` `Set.piecewise_eq_of_mem` `IntegrationParams.MemBaseSet.isSubordinate` `Box.coe_subset_Icc` `Prepartition.le_of_mem'` `abs_sub_le_iff` `Real.instIsOrderedAddMonoid` `LE.le.trans` `ENNReal.le_toReal_sub` `ENNReal.toReal_le_coe_of_le_coe` `tsub_le_tsub` `ENNReal.instOrderedSub` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `le_rfl` `MeasureTheory.le_measure_diff` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.inter_subset_left` `Mathlib.Tactic.Contrapose.contrapose₁` `Set.piecewise_eq_of_notMem` `norm_nonneg` `Set.nonempty_Ioi_subtype` `instNoMaxOrderOfNontrivial` `Real.instNontrivial` `Function.sometimes_spec`

BoxIntegral.HasIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`congr_ae` 📖	bridging (sound)	`BoxIntegral.HasIntegral` `BoxIntegral.BoxAdditiveMap.toSMul` `Top.top` `WithTop` `BoxIntegral.Box` `WithTop.top` `MeasureTheory.Measure.toBoxAdditive` `Finite.of_fintype` `Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasurableSpace.pi` `Real` `Real.measurableSpace` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.restrict` `BoxIntegral.Box.toSet` `BoxIntegral.IntegrationParams.bRiemann`	—	`BoxIntegral.IntegrationParams.bRiemann`	`Finite.of_fintype` `MeasureTheory.Measure.instOuterMeasureClass` `Filter.Eventually.mono` `sub_eq_zero` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `add_sub_cancel` `add_zero` `add` `of_aeEq_zero`
`of_aeEq_zero` 📖	bridging (sound)	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasurableSpace.pi` `Real` `Real.measurableSpace` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.restrict` `BoxIntegral.Box.toSet` `Pi.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `BoxIntegral.IntegrationParams.bRiemann`	`BoxIntegral.HasIntegral` `BoxIntegral.BoxAdditiveMap.toSMul` `Top.top` `WithTop` `BoxIntegral.Box` `WithTop.top` `MeasureTheory.Measure.toBoxAdditive` `Finite.of_fintype`	`BoxIntegral.IntegrationParams.bRiemann`	`MeasureTheory.Measure.instOuterMeasureClass` `Finite.of_fintype` `BoxIntegral.hasIntegral_iff` `CanLift.prf` `NNReal.canLift` `LT.lt.le` `GT.gt.lt` `NNReal.exists_pos_sum_of_countable` `LT.lt.ne'` `NNReal.coe_pos` `instCountableNat` `Real.instIsStrictOrderedRing` `Set.exists_isOpen_lt_of_lt` `MeasureTheory.Measure.WeaklyRegular.toOuterRegular` `MeasureTheory.Measure.WeaklyRegular.of_pseudoMetrizableSpace_secondCountable_of_locallyFinite` `TopologicalSpace.pseudoMetrizableSpace_pi` `PseudoEMetricSpace.pseudoMetrizableSpace` `TopologicalSpace.instSecondCountableTopologyForallOfCountable` `Finite.to_countable` `instSecondCountableTopologyReal` `Pi.borelSpace` `Real.borelSpace` `MeasureTheory.isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts` `instWeaklyLocallyCompactSpaceForallOfFinite` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `instProperSpaceReal` `MeasureTheory.instIsFiniteMeasureOnCompactsRestrict` `MeasureTheory.Measure.Regular.toIsFiniteMeasureOnCompacts` `MeasureTheory.Measure.Regular.of_sigmaCompactSpace_of_isLocallyFiniteMeasure` `instSigmaCompactSpaceForallOfFinite` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `instIsTopologicalAddGroupReal` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `CharP.cast_eq_zero` `CharP.ofCharZero` `ENNReal.instCharZero` `ENNReal.div_zero` `ENNReal.coe_pos` `MeasureTheory.Restrict.isFiniteMeasure` `BoxIntegral.Box.measure_coe_lt_top` `LE.le.trans_lt` `Eq.le` `MeasureTheory.measure_mono_null` `Nat.cast_add` `Nat.cast_one` `Filter.HasBasis.mem_iff` `Metric.nhds_basis_closedBall` `IsOpen.mem_nhds` `BoxIntegral.IntegrationParams.rCond_of_bRiemann_eq_false` `dist_eq_norm` `sub_zero` `BoxIntegral.integralSum_fiberwise` `le_imp_le_of_le_of_le` `le_refl` `le_of_lt` `sum_le_hasSum` `Real.instIsOrderedAddMonoid` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `SummationFilter.instNeBotUnconditional` `SummationFilter.instLeAtTopUnconditional` `NNReal.hasSum_coe` `norm_sum_le_of_le` `norm_smul` `NormedSpace.toNormSMulClass` `Real.norm_eq_abs` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `MeasureTheory.measureReal_nonneg` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `Nat.le_ceil` `BoxIntegral.TaggedPrepartition.mem_filter` `LE.le.trans` `Finset.sum_mul` `BoxIntegral.Prepartition.measure_iUnion_toReal` `MeasureTheory.measure_mono` `BoxIntegral.IntegrationParams.MemBaseSet.isSubordinate` `BoxIntegral.Box.coe_subset_Icc` `BoxIntegral.Prepartition.le_of_mem'` `MeasureTheory.Measure.restrict_apply` `IsOpen.measurableSet` `Pi.opensMeasurableSpace` `BorelSpace.opensMeasurable` `ENNReal.canLift` `ne_top_of_lt` `ENNReal.coe_toReal` `NNReal.coe_natCast` `NNReal.coe_mul` `NNReal.coe_le_coe` `ENNReal.coe_le_coe` `ENNReal.coe_mul` `ENNReal.coe_natCast` `mul_comm` `mul_le_mul_right` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `ENNReal.mul_div_le`

MeasureTheory.AEContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasBoxIntegral` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `Filter.Eventually` `ContinuousAt` `Pi.topologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasurableSpace.pi` `Real.measurableSpace` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	`BoxIntegral.HasIntegral` `BoxIntegral.BoxAdditiveMap.toSMul` `Top.top` `WithTop` `BoxIntegral.Box` `WithTop.top` `MeasureTheory.Measure.toBoxAdditive` `Finite.of_fintype` `MeasureTheory.integral` `MeasureTheory.Measure.restrict` `BoxIntegral.Box.toSet`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Finite.of_fintype` `BoxIntegral.integrable_of_bounded_and_ae_continuous` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `BoxIntegral.HasIntegral.unique` `MeasureTheory.IntegrableOn.hasBoxIntegral` `ContinuousOn.aestronglyMeasurable` `secondCountableTopologyEither_of_left` `TopologicalSpace.instSecondCountableTopologyForallOfCountable` `Finite.to_countable` `instSecondCountableTopologyReal` `Pi.opensMeasurableSpace` `BorelSpace.opensMeasurable` `Real.borelSpace` `PseudoEMetricSpace.pseudoMetrizableSpace` `continuousOn_of_forall_continuousAt` `measurableSet_of_continuousAt` `MeasureTheory.AEStronglyMeasurable.mono_measure` `MeasureTheory.Measure.le_iff` `MeasureTheory.Measure.restrict_apply` `MeasureTheory.OuterMeasure.mono` `Set.inter_subset_left` `MeasureTheory.measure_eq_measure_of_null_diff` `Set.diff_self_inter` `Set.diff_eq` `le_antisymm` `zero_le` `ENNReal.instCanonicallyOrderedAdd` `le_trans` `Set.inter_subset_right` `nonpos_iff_eq_zero` `Set.univ_inter` `IsCompact.measure_lt_top` `MeasureTheory.Measure.Regular.toIsFiniteMeasureOnCompacts` `MeasureTheory.Measure.Regular.of_sigmaCompactSpace_of_isLocallyFiniteMeasure` `TopologicalSpace.pseudoMetrizableSpace_pi` `instSigmaCompactSpaceForallOfFinite` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `instIsTopologicalAddGroupReal` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `instProperSpaceReal` `Pi.borelSpace` `BoxIntegral.Box.isCompact_Icc` `MeasureTheory.isFiniteMeasure_of_le` `MeasureTheory.Measure.restrict_mono` `BoxIntegral.Box.coe_subset_Icc` `le_refl` `MeasureTheory.HasFiniteIntegral.of_bounded` `Filter.eventually_iff_exists_mem` `MeasureTheory.self_mem_ae_restrict` `BoxIntegral.Box.measurableSet_coe` `BoxIntegral.HasIntegral.mono` `bot_le`

MeasureTheory.ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasBoxIntegral` 📖	mathematical	`ContinuousOn` `Pi.topologicalSpace` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `OrderEmbedding` `BoxIntegral.Box` `Set` `BoxIntegral.Box.instLE` `Set.instLE` `instFunLikeOrderEmbedding` `BoxIntegral.Box.Icc`	`BoxIntegral.HasIntegral` `BoxIntegral.BoxAdditiveMap.toSMul` `Top.top` `WithTop` `WithTop.top` `MeasureTheory.Measure.toBoxAdditive` `Finite.of_fintype` `MeasureTheory.integral` `MeasurableSpace.pi` `Real.measurableSpace` `MeasureTheory.Measure.restrict` `BoxIntegral.Box.toSet`	—	`Finite.of_fintype` `BoxIntegral.integrable_of_continuousOn` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.IntegrableOn.mono_set` `ContinuousOn.integrableOn_compact` `Pi.opensMeasurableSpace` `Finite.to_countable` `instSecondCountableTopologyReal` `BorelSpace.opensMeasurable` `Real.borelSpace` `MeasureTheory.Measure.Regular.toIsFiniteMeasureOnCompacts` `MeasureTheory.Measure.Regular.of_sigmaCompactSpace_of_isLocallyFiniteMeasure` `TopologicalSpace.pseudoMetrizableSpace_pi` `PseudoEMetricSpace.pseudoMetrizableSpace` `instSigmaCompactSpaceForallOfFinite` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `instIsTopologicalAddGroupReal` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `instProperSpaceReal` `Pi.borelSpace` `Pi.t2Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `BoxIntegral.Box.isCompact_Icc` `BoxIntegral.Box.coe_subset_Icc` `BoxIntegral.HasIntegral.unique` `MeasureTheory.IntegrableOn.hasBoxIntegral` `BoxIntegral.HasIntegral.mono` `bot_le`

MeasureTheory.IntegrableOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasBoxIntegral` 📖	bridging (sound)	`MeasureTheory.IntegrableOn` `MeasurableSpace.pi` `Real` `Real.measurableSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `BoxIntegral.Box.toSet` `BoxIntegral.IntegrationParams.bRiemann`	`BoxIntegral.HasIntegral` `BoxIntegral.BoxAdditiveMap.toSMul` `Top.top` `WithTop` `BoxIntegral.Box` `WithTop.top` `MeasureTheory.Measure.toBoxAdditive` `Finite.of_fintype` `MeasureTheory.integral` `MeasureTheory.Measure.restrict`	`BoxIntegral.IntegrationParams.bRiemann`	`MeasureTheory.Measure.instOuterMeasureClass` `Finite.of_fintype` `MeasureTheory.Integrable.aestronglyMeasurable` `MeasureTheory.integral_congr_ae` `MeasureTheory.integrable_congr` `BoxIntegral.HasIntegral.congr_ae` `BorelSpace.opensMeasurable` `MeasureTheory.StronglyMeasurable.measurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `Set.union_singleton` `MeasureTheory.StronglyMeasurable.separableSpace_range_union_singleton` `MeasureTheory.SimpleFunc.integrable_approxOn_range` `BoxIntegral.HasIntegral.integrable` `MeasureTheory.SimpleFunc.hasBoxIntegral` `dist_eq_norm` `dist_nndist` `NNReal.coe_le_coe` `ENNReal.coe_le_coe` `edist_nndist` `MeasureTheory.SimpleFunc.edist_approxOn_mono` `BoxIntegral.HasIntegral.of_mul` `CanLift.prf` `NNReal.canLift` `LT.lt.le` `ENNReal.coe_pos` `NNReal.coe_pos` `MeasureTheory.SimpleFunc.tendsto_approxOn_range_L1_enorm` `MeasureTheory.integral_coe_le_of_lintegral_coe_le` `Filter.Eventually.exists` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Filter.Tendsto.eventually` `ge_mem_nhds` `ENNReal.instOrderTopology` `MeasureTheory.SimpleFunc.tendsto_approxOn` `subset_closure` `Filter.Eventually.and` `Filter.eventually_ge_atTop` `Metric.closedBall_mem_nhds` `NNReal.exists_pos_sum_of_countable` `LT.lt.ne'` `instCountableNat` `BoxIntegral.IntegrationParams.rCond_of_bRiemann_eq_false` `LE.le.trans` `dist_triangle4` `add_mul` `Distrib.rightDistribClass` `one_mul` `add_le_add_three` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `BoxIntegral.Prepartition.IsPartition.iUnion_eq` `BoxIntegral.Prepartition.measure_iUnion_toReal` `Finset.sum_mul` `BoxIntegral.integralSum.eq_1` `dist_sum_sum_le_of_le` `smul_sub` `norm_smul` `NormedSpace.toNormSMulClass` `Real.norm_eq_abs` `abs_of_nonneg` `MeasureTheory.measureReal_nonneg` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `dist_eq_norm'` `BoxIntegral.Prepartition.sum_fiberwise` `le_imp_le_of_le_of_le` `le_refl` `le_of_lt` `BoxIntegral.TaggedPrepartition.mem_filter` `BoxIntegral.IntegrationParams.MemBaseSet.mono'` `le_rfl` `Eq.le` `BoxIntegral.IntegrationParams.MemBaseSet.filter` `Finset.sum_congr` `MeasureTheory.SimpleFunc.integral_eq_integral` `mono_set` `BoxIntegral.Prepartition.le_of_mem` `MeasureTheory.SimpleFunc.box_integral_eq_integral` `BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet` `sum_le_hasSum` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `SummationFilter.instNeBotUnconditional` `SummationFilter.instLeAtTopUnconditional` `NNReal.hasSum_coe` `le_trans` `BoxIntegral.Prepartition.le_of_mem'` `MeasureTheory.Integrable.norm` `MeasureTheory.Integrable.sub` `BoxIntegral.Prepartition.iUnion_def'` `MeasureTheory.integral_biUnion_finset` `BoxIntegral.Box.measurableSet_coe` `Finite.to_countable` `BoxIntegral.Prepartition.pairwiseDisjoint` `MeasureTheory.integral_sub` `MeasureTheory.norm_integral_le_of_norm_le` `Filter.Eventually.of_forall` `Filter.EventuallyEq.symm`

MeasureTheory.SimpleFunc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`box_integral_eq_integral` 📖	bridging (sound)	`BoxIntegral.IntegrationParams.bRiemann`	`BoxIntegral.integral` `DFunLike.coe` `MeasureTheory.SimpleFunc` `MeasurableSpace.pi` `Real` `Real.measurableSpace` `instFunLike` `BoxIntegral.BoxAdditiveMap.toSMul` `Top.top` `WithTop` `BoxIntegral.Box` `WithTop.top` `MeasureTheory.Measure.toBoxAdditive` `Finite.of_fintype` `integral` `MeasureTheory.Measure.restrict` `BoxIntegral.Box.toSet`	`BoxIntegral.IntegrationParams.bRiemann`	`BoxIntegral.HasIntegral.integral_eq` `Finite.of_fintype` `hasBoxIntegral`
`hasBoxIntegral` 📖	bridging (sound)	`BoxIntegral.IntegrationParams.bRiemann`	`BoxIntegral.HasIntegral` `DFunLike.coe` `MeasureTheory.SimpleFunc` `MeasurableSpace.pi` `Real` `Real.measurableSpace` `instFunLike` `BoxIntegral.BoxAdditiveMap.toSMul` `Top.top` `WithTop` `BoxIntegral.Box` `WithTop.top` `MeasureTheory.Measure.toBoxAdditive` `Finite.of_fintype` `integral` `MeasureTheory.Measure.restrict` `BoxIntegral.Box.toSet`	`BoxIntegral.IntegrationParams.bRiemann`	`induction` `Finite.of_fintype` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Set.piecewise_eq_indicator` `integral_piecewise_zero` `MeasureTheory.Measure.restrict_restrict` `integral_const` `MeasureTheory.measureReal_restrict_apply` `Set.univ_inter` `BoxIntegral.hasIntegralIndicatorConst` `integral_add` `integrable_iff` `MeasureTheory.measure_lt_top` `MeasureTheory.Restrict.isFiniteMeasure` `BoxIntegral.Box.measure_coe_lt_top` `BoxIntegral.HasIntegral.add`

---

← Back to Index