Basic

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

Statistics

Metric	Count
Definitions `HasIntegral`, `convergenceR`, `toBoxAdditive`, `integral`, `integralSum`	5
Theorems `add`, `integrable`, `integral_eq`, `mcShane_of_forall_isLittleO`, `mono`, `neg`, `of_bRiemann_eq_false_of_forall_isLittleO`, `of_le_Henstock_of_forall_isLittleO`, `of_mul`, `smul`, `sub`, `sum`, `tendsto`, `unique`, `add`, `cauchy_map_integralSum_toFilteriUnion`, `convergenceR_cond`, `dist_integralSum_integral_le_of_memBaseSet`, `dist_integralSum_le_of_memBaseSet`, `dist_integralSum_sum_integral_le_of_memBaseSet`, `dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq`, `hasIntegral`, `mono`, `neg`, `of_neg`, `of_smul`, `smul`, `sub`, `sum_integral_congr`, `tendsto_integralSum_sum_integral`, `tendsto_integralSum_toFilter_prod_self_inf_iUnion_eq_uniformity`, `tendsto_integralSum_toFilteriUnion_single`, `toBoxAdditive_apply`, `to_subbox`, `to_subbox_aux`, `hasIntegral_const`, `hasIntegral_iff`, `hasIntegral_zero`, `integrable_const`, `integrable_iff_cauchy`, `integrable_iff_cauchy_basis`, `integrable_neg`, `integrable_of_bounded_and_ae_continuous`, `integrable_of_bounded_and_ae_continuousWithinAt`, `integrable_of_continuousOn`, `integrable_zero`, `integralSum_add`, `integralSum_biUnionTagged`, `integralSum_biUnion_partition`, `integralSum_disjUnion`, `integralSum_fiberwise`, `integralSum_inf_partition`, `integralSum_neg`, `integralSum_smul`, `integralSum_sub_partitions`, `integral_add`, `integral_const`, `integral_neg`, `integral_nonneg`, `integral_smul`, `integral_sub`, `integral_zero`, `norm_integral_le_of_le_const`, `norm_integral_le_of_norm_le`	64
Total	69

BoxIntegral

Definitions

Name	Category	Theorems
`HasIntegral` 📖	MathDef	12 math, 5 bridge math: `hasIntegral_zero`, `hasIntegral_GP_pderiv`, `hasIntegral_GP_divergence_of_forall_hasDerivWithinAt`, `HasIntegral.of_mul`, `Integrable.to_subbox_aux`, `MeasureTheory.AEContinuous.hasBoxIntegral`, `Integrable.hasIntegral`, `MeasureTheory.ContinuousOn.hasBoxIntegral`, `hasIntegral_const`, `HasIntegral.of_le_Henstock_of_forall_isLittleO`, `hasIntegral_iff`, `HasIntegral.mcShane_of_forall_isLittleO` bridge: `hasIntegralIndicatorConst`, `MeasureTheory.SimpleFunc.hasBoxIntegral`, `MeasureTheory.IntegrableOn.hasBoxIntegral`, `HasIntegral.of_bRiemann_eq_false_of_forall_isLittleO`, `HasIntegral.of_aeEq_zero`
`integral` 📖	CompOp	21 math, 1 bridge math: `integral_sub`, `integral_zero`, `integral_add`, `hasIntegral_GP_pderiv`, `hasIntegral_GP_divergence_of_forall_hasDerivWithinAt`, `integral_neg`, `Integrable.toBoxAdditive_apply`, `Integrable.dist_integralSum_integral_le_of_memBaseSet`, `integral_nonneg`, `Integrable.dist_integralSum_sum_integral_le_of_memBaseSet`, `Integrable.hasIntegral`, `norm_integral_le_of_le_const`, `Integrable.sum_integral_congr`, `integral_smul`, `norm_volume_sub_integral_face_upper_sub_lower_smul_le`, `Integrable.tendsto_integralSum_toFilteriUnion_single`, `integral_const`, `Integrable.tendsto_integralSum_sum_integral`, `norm_integral_le_of_norm_le`, `Integrable.dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq`, `HasIntegral.integral_eq` bridge: `MeasureTheory.SimpleFunc.box_integral_eq_integral`
`integralSum` 📖	CompOp	23 math math: `integralSum_inf_partition`, `HasIntegral.tendsto`, `Integrable.dist_integralSum_le_of_memBaseSet`, `unitPartition.integralSum_eq_tsum_div`, `integralSum_add`, `Integrable.to_subbox_aux`, `Integrable.cauchy_map_integralSum_toFilteriUnion`, `Integrable.dist_integralSum_integral_le_of_memBaseSet`, `Integrable.dist_integralSum_sum_integral_le_of_memBaseSet`, `integralSum_neg`, `integralSum_biUnionTagged`, `integralSum_fiberwise`, `integrable_iff_cauchy_basis`, `Integrable.tendsto_integralSum_toFilteriUnion_single`, `integralSum_smul`, `integralSum_disjUnion`, `integralSum_sub_partitions`, `Integrable.tendsto_integralSum_toFilter_prod_self_inf_iUnion_eq_uniformity`, `integrable_iff_cauchy`, `integralSum_biUnion_partition`, `Integrable.tendsto_integralSum_sum_integral`, `hasIntegral_iff`, `Integrable.dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasIntegral_const` 📖	mathematical	—	`HasIntegral` `DFunLike.coe` `ContinuousLinearMap` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `ContinuousLinearMap.funLike` `BoxAdditiveMap` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Top.top` `WithTop` `Box` `WithTop.top` `BoxAdditiveMap.instFunLikeBox`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Filter.Tendsto.congr'` `Filter.Eventually.mono` `IntegrationParams.eventually_isPartition` `BoxAdditiveMap.sum_partition_boxes` `le_top` `tendsto_const_nhds`
`hasIntegral_iff` 📖	mathematical	—	`HasIntegral` `IntegrationParams.RCond` `Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `integralSum`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Filter.HasBasis.tendsto_iff` `IntegrationParams.hasBasis_toFilteriUnion_top` `Metric.nhds_basis_closedBall` `forall_swap`
`hasIntegral_zero` 📖	mathematical	—	`HasIntegral` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.map_zero` `hasIntegral_const`
`integrable_const` 📖	mathematical	—	`Integrable`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `hasIntegral_const`
`integrable_iff_cauchy` 📖	mathematical	—	`Integrable` `Cauchy` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Filter.map` `TaggedPrepartition` `integralSum` `IntegrationParams.toFilteriUnion` `Top.top` `Prepartition` `OrderTop.toTop` `Prepartition.instLE` `Prepartition.instOrderTop`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `cauchy_map_iff_exists_tendsto` `IntegrationParams.toFilteriUnion_neBot`
`integrable_iff_cauchy_basis` 📖	mathematical	—	`Integrable` `IntegrationParams.RCond` `Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `integralSum`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `integrable_iff_cauchy` `cauchy_map_iff'` `IntegrationParams.toFilteriUnion_neBot` `Filter.HasBasis.tendsto_iff` `Filter.HasBasis.prod_self` `IntegrationParams.hasBasis_toFilteriUnion_top` `Metric.uniformity_basis_dist_le`
`integrable_neg` 📖	mathematical	—	`Integrable` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Integrable.of_neg` `Integrable.neg`
`integrable_of_bounded_and_ae_continuous` 📖	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`	`Integrable` `BoxAdditiveMap.toSMul` `Top.top` `WithTop` `Box` `WithTop.top` `MeasureTheory.Measure.toBoxAdditive` `Finite.of_fintype`	—	`MeasureTheory.Measure.instOuterMeasureClass` `integrable_of_bounded_and_ae_continuousWithinAt` `Filter.Eventually.filter_mono` `MeasureTheory.ae_mono` `MeasureTheory.Measure.restrict_le_self` `Filter.Eventually.mono` `ContinuousAt.continuousWithinAt`
`integrable_of_bounded_and_ae_continuousWithinAt` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `Filter.Eventually` `ContinuousWithinAt` `Pi.topologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `OrderEmbedding` `Box` `Set` `Box.instLE` `Set.instLE` `instFunLikeOrderEmbedding` `Box.Icc` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasurableSpace.pi` `Real.measurableSpace` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.restrict`	`Integrable` `BoxAdditiveMap.toSMul` `Top.top` `WithTop` `WithTop.top` `MeasureTheory.Measure.toBoxAdditive` `Finite.of_fintype`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Finite.of_fintype` `integrable_iff_cauchy_basis` `Nat.instAtLeastTwoHAddOfNat` `exists_pos_mul_lt` `Real.instIsStrictOrderedRing` `Box.nonempty_coe` `le_trans` `norm_nonneg` `Box.coe_subset_Icc` `ne_of_gt` `ENNReal.ofReal_pos` `Filter.eventually_iff_exists_mem` `eq_of_le_of_not_lt` `MeasureTheory.OuterMeasure.mono` `MeasureTheory.mem_ae_iff` `not_lt_zero` `ENNReal.instCanonicallyOrderedAdd` `Set.exists_isOpen_lt_add` `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` `IsCompact.of_isClosed_subset` `Box.isCompact_Icc` `IsClosed.sdiff` `IsCompact.isClosed` `Pi.t2Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Set.diff_subset` `IsCompact.uniform_oscillationWithin` `half_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `dist_eq_norm` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `integralSum_sub_partitions` `Finset.sum_congr` `lt_of_le_of_lt` `IsCompact.measure_lt_top` `Finset.filter_subset` `lt_top_iff_ne_top` `Prepartition.le_of_mem'` `Set.iUnion_subset_iff` `Finset.sum_sdiff` `add_halves` `CharZero.NeZero.two` `RCLike.charZero_rclike` `norm_add_le` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `norm_smul` `NormedSpace.toNormSMulClass` `MeasureTheory.Measure.toBoxAdditive_apply` `Real.norm_of_nonneg` `MeasureTheory.measureReal_nonneg` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `Set.not_subset` `Finset.mem_filter` `Finset.mem_sdiff` `Metric.edist_le_ediam_of_mem` `Set.mem_image_of_mem` `Metric.closedBall_subset_ball` `div_two_lt_of_pos` `Metric.mem_closedBall_comm` `TaggedPrepartition.IsSubordinate.infPrepartition` `IntegrationParams.MemBaseSet.isSubordinate` `TaggedPrepartition.tag_mem_Icc` `TaggedPrepartition.mem_infPrepartition_comm` `edist_le_ofReal` `le_of_lt` `LE.le.trans` `Metric.eball_ofReal` `norm_sum_le` `Finset.sum_le_sum` `Finset.sum_mul` `mul_le_mul_iff_left₀` `IsOrderedRing.toMulPosMono` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `ENNReal.toReal_sum` `Finset.tsum_subtype` `ENNReal.toReal_mono` `ne_of_lt` `Finset.sdiff_subset` `le_of_eq` `MeasureTheory.measure_biUnion` `Finset.countable_toSet` `Prepartition.pairwiseDisjoint` `Box.measurableSet_coe` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Nat.cast_one` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_neg` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `CancelDenoms.sub_subst` `CancelDenoms.div_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.isNat_mul` `CancelDenoms.mul_subst` `Mathlib.Tactic.Linarith.mul_neg` `Mathlib.Meta.NormNum.isNat_lt_true` `two_mul` `norm_sub_le_of_le` `norm_sum_le_of_le` `ENNReal.toReal_ofReal` `ENNReal.ofReal_ne_top` `MeasureTheory.Measure.restrict_eq_self` `HasSubset.Subset.trans` `Set.instIsTransSubset` `MeasureTheory.measure_biUnion_finset` `zero_add` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.mul_nonpos` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `mul_le_mul_of_nonneg_right` `mul_nonneg_iff_of_pos_left` `two_pos` `Real.instZeroLEOneClass` `NeZero.charZero_one`
`integrable_of_continuousOn` 📖	mathematical	`ContinuousOn` `Pi.topologicalSpace` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `OrderEmbedding` `Box` `Set` `Box.instLE` `Set.instLE` `instFunLikeOrderEmbedding` `Box.Icc`	`Integrable` `BoxAdditiveMap.toSMul` `Top.top` `WithTop` `WithTop.top` `MeasureTheory.Measure.toBoxAdditive` `Finite.of_fintype`	—	`integrable_of_bounded_and_ae_continuousWithinAt` `NormedSpace.isBounded_iff_subset_smul_closedBall` `IsCompact.isBounded` `IsCompact.image_of_continuousOn` `Box.isCompact_Icc` `smul_unitClosedBall` `Set.mem_image_of_mem` `Filter.eventually_of_mem` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.mem_ae_iff` `MeasureTheory.Measure.restrict_apply` `MeasurableSet.compl_iff` `Box.measurableSet_Icc` `Finite.to_countable` `Finite.of_fintype` `Set.compl_inter_self` `MeasureTheory.measure_empty` `ContinuousOn.continuousWithinAt`
`integrable_zero` 📖	mathematical	—	`Integrable` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `hasIntegral_zero`
`integralSum_add` 📖	mathematical	—	`integralSum` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Finset.sum_congr` `ContinuousLinearMap.map_add` `Finset.sum_add_distrib`
`integralSum_biUnionTagged` 📖	mathematical	—	`integralSum` `Prepartition.biUnionTagged` `Finset.sum` `Box` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Prepartition.boxes`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Prepartition.sum_biUnion_boxes` `Finset.sum_congr` `Prepartition.tag_biUnionTagged`
`integralSum_biUnion_partition` 📖	mathematical	`Prepartition.IsPartition`	`integralSum` `TaggedPrepartition.biUnionPrepartition`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Prepartition.sum_biUnion_boxes` `Finset.sum_congr` `Prepartition.biUnionIndex_of_mem` `BoxAdditiveMap.sum_partition_boxes` `le_top`
`integralSum_disjUnion` 📖	mathematical	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `TaggedPrepartition.iUnion`	`integralSum` `TaggedPrepartition.disjUnion` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Prepartition.sum_disj_union_boxes` `Finset.sum_congr` `TaggedPrepartition.disjUnion_tag_of_mem_left` `TaggedPrepartition.disjUnion_tag_of_mem_right`
`integralSum_fiberwise` 📖	mathematical	—	`Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.image` `Box` `Prepartition.boxes` `TaggedPrepartition.toPrepartition` `integralSum` `TaggedPrepartition.filter`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Prepartition.sum_fiberwise`
`integralSum_inf_partition` 📖	mathematical	`Prepartition.IsPartition`	`integralSum` `TaggedPrepartition.infPrepartition`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `integralSum_biUnion_partition` `Prepartition.IsPartition.restrict` `Prepartition.le_of_mem`
`integralSum_neg` 📖	mathematical	—	`integralSum` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Finset.sum_congr` `ContinuousLinearMap.map_neg` `Finset.sum_neg_distrib`
`integralSum_smul` 📖	mathematical	—	`integralSum` `Real` `Function.hasSMul` `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`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Finset.sum_congr` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `Finset.smul_sum`
`integralSum_sub_partitions` 📖	mathematical	`TaggedPrepartition.IsPartition`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `integralSum` `Finset.sum` `Box` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Prepartition.boxes` `Prepartition` `SemilatticeInf.toMin` `Prepartition.instSemilatticeInf` `TaggedPrepartition.toPrepartition` `DFunLike.coe` `ContinuousLinearMap` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NormedSpace.toModule` `Real.normedField` `ContinuousLinearMap.funLike` `BoxAdditiveMap` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Top.top` `WithTop` `WithTop.top` `BoxAdditiveMap.instFunLikeBox` `TaggedPrepartition.tag` `TaggedPrepartition.infPrepartition`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `integralSum_inf_partition` `integralSum.eq_1` `Finset.sum_sub_distrib` `Finset.sum_congr` `inf_comm`
`integral_add` 📖	mathematical	`Integrable`	`integral` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `HasIntegral.integral_eq` `HasIntegral.add` `Integrable.hasIntegral`
`integral_const` 📖	mathematical	—	`integral` `DFunLike.coe` `ContinuousLinearMap` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `ContinuousLinearMap.funLike` `BoxAdditiveMap` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Top.top` `WithTop` `Box` `WithTop.top` `BoxAdditiveMap.instFunLikeBox`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `HasIntegral.integral_eq` `hasIntegral_const`
`integral_neg` 📖	mathematical	—	`integral` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `HasIntegral.integral_eq` `HasIntegral.neg` `Integrable.hasIntegral` `integral.eq_1` `Integrable.of_neg` `neg_zero`
`integral_nonneg` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `BoxAdditiveMap.toSMul` `Top.top` `WithTop` `Box` `WithTop.top` `MeasureTheory.Measure.toBoxAdditive` `Finite.of_fintype`	—	`Finite.of_fintype` `ge_of_tendsto'` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `IntegrationParams.toFilteriUnion_neBot` `Integrable.hasIntegral` `Finset.sum_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `ENNReal.toReal_nonneg` `TaggedPrepartition.tag_mem_Icc` `integral.eq_1` `le_refl`
`integral_smul` 📖	mathematical	—	`integral` `Real` `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`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `eq_or_ne` `zero_smul` `integral_zero` `HasIntegral.integral_eq` `HasIntegral.smul` `Integrable.hasIntegral` `Integrable.of_smul` `integral.eq_1` `smul_zero`
`integral_sub` 📖	mathematical	`Integrable`	`integral` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `HasIntegral.integral_eq` `HasIntegral.sub` `Integrable.hasIntegral`
`integral_zero` 📖	mathematical	—	`integral` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `HasIntegral.integral_eq` `hasIntegral_zero`
`norm_integral_le_of_le_const` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm`	`integral` `BoxAdditiveMap.toSMul` `Top.top` `WithTop` `Box` `WithTop.top` `MeasureTheory.Measure.toBoxAdditive` `Finite.of_fintype` `Real.instMul` `MeasureTheory.Measure.real` `MeasurableSpace.pi` `Real.measurableSpace` `Box.toSet`	—	`Finite.of_fintype` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `integral_const` `norm_integral_le_of_norm_le` `integrable_const`
`norm_integral_le_of_norm_le` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `Integrable` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `BoxAdditiveMap.toSMul` `Top.top` `WithTop` `Box` `WithTop.top` `MeasureTheory.Measure.toBoxAdditive` `Finite.of_fintype`	`integral`	—	`Finite.of_fintype` `le_of_tendsto_of_tendsto'` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `IntegrationParams.toFilteriUnion_neBot` `Filter.Tendsto.norm` `Integrable.hasIntegral` `norm_sum_le_of_le` `norm_smul` `NormedSpace.toNormSMulClass` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `MeasureTheory.measureReal_nonneg` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `TaggedPrepartition.tag_mem_Icc` `integral.eq_1` `norm_zero` `integral_nonneg` `LE.le.trans` `norm_nonneg`

BoxIntegral.HasIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`BoxIntegral.HasIntegral`	`Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Filter.Tendsto.add`
`integrable` 📖	mathematical	`BoxIntegral.HasIntegral`	`BoxIntegral.Integrable`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`integral_eq` 📖	mathematical	`BoxIntegral.HasIntegral`	`BoxIntegral.integral`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `unique` `BoxIntegral.Integrable.hasIntegral` `integrable`
`mcShane_of_forall_isLittleO` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `DFunLike.coe` `BoxIntegral.BoxAdditiveMap` `Real.instAddCommMonoid` `WithTop.some` `BoxIntegral.Box` `BoxIntegral.BoxAdditiveMap.instFunLikeBox` `Real.instLT` `Dist.dist` `PseudoMetricSpace.toDist` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ContinuousLinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `ContinuousLinearMap.funLike` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Top.top` `WithTop` `WithTop.top` `Real.instMul`	`BoxIntegral.HasIntegral` `BoxIntegral.IntegrationParams.McShane`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `of_bRiemann_eq_false_of_forall_isLittleO` `Set.countable_empty` `Set.diff_empty` `Bool.coe_sort_false`
`mono` 📖	—	`BoxIntegral.HasIntegral` `BoxIntegral.IntegrationParams` `Preorder.toLE` `PartialOrder.toPreorder` `BoxIntegral.IntegrationParams.instPartialOrder`	—	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Filter.Tendsto.mono_left` `BoxIntegral.IntegrationParams.toFilteriUnion_mono`
`neg` 📖	mathematical	`BoxIntegral.HasIntegral`	`Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Filter.Tendsto.neg` `IsTopologicalAddGroup.toContinuousNeg`
`of_bRiemann_eq_false_of_forall_isLittleO` 📖	bridging (sound)	`BoxIntegral.IntegrationParams.bRiemann` `Real` `Real.instLE` `Real.instZero` `DFunLike.coe` `BoxIntegral.BoxAdditiveMap` `Real.instAddCommMonoid` `WithTop.some` `BoxIntegral.Box` `BoxIntegral.BoxAdditiveMap.instFunLikeBox` `BoxIntegral.IntegrationParams.bHenstock` `Real.instLT` `Dist.dist` `PseudoMetricSpace.toDist` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ContinuousLinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `ContinuousLinearMap.funLike` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Top.top` `WithTop` `WithTop.top` `Real.instMul`	`BoxIntegral.HasIntegral`	`BoxIntegral.IntegrationParams.bRiemann`	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Filter.HasBasis.tendsto_iff` `BoxIntegral.IntegrationParams.hasBasis_toFilteriUnion_top` `Metric.nhds_basis_closedBall` `Nat.instAtLeastTwoHAddOfNat` `half_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `pow_pos` `Real.instZeroLEOneClass` `zero_lt_two` `NeZero.charZero_one` `RCLike.charZero_rclike` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Set.Countable.exists_pos_forall_sum_le` `div_pos` `exists_pos_mul_lt` `BoxIntegral.IntegrationParams.rCond_of_bRiemann_eq_false` `BoxIntegral.BoxAdditiveMap.sum_partition_boxes` `le_rfl` `Metric.mem_closedBall` `BoxIntegral.integralSum.eq_1` `Finset.sum_filter_add_sum_filter_not` `add_halves` `CharZero.NeZero.two` `dist_add_add_le_of_le` `Set.eq_empty_or_nonempty` `Finset.sum_congr` `Finset.filter.congr_simp` `Finset.filter_false` `dist_self` `LT.lt.le` `le_div_iff₀'` `Finset.mul_sum` `Finset.mem_filter` `BoxIntegral.TaggedPrepartition.tag_mem_Icc` `BoxIntegral.Prepartition.le_of_mem'` `BoxIntegral.IntegrationParams.MemBaseSet.isSubordinate` `BoxIntegral.IntegrationParams.MemBaseSet.isHenstock` `LE.le.trans` `Finset.le_sup` `BoxIntegral.IntegrationParams.MemBaseSet.distortion_le` `dist_sum_sum_le_of_le` `Finset.sum_comp` `Finset.sum_le_sum` `Nat.cast_two` `Nat.cast_pow` `nsmul_eq_mul` `nsmul_le_nsmul_left` `Finset.card_le_card` `Finset.filter_subset_filter` `Finset.filter_subset` `BoxIntegral.TaggedPrepartition.IsHenstock.card_filter_tag_eq_le` `Finset.coe_image` `Set.image_subset_iff` `Finset.sum_le_sum_of_subset_of_nonneg` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `mul_comm` `nonempty_gt` `instNoMaxOrderOfNontrivial` `Real.instNontrivial` `Function.sometimes_spec`
`of_le_Henstock_of_forall_isLittleO` 📖	mathematical	`BoxIntegral.IntegrationParams` `Preorder.toLE` `PartialOrder.toPreorder` `BoxIntegral.IntegrationParams.instPartialOrder` `BoxIntegral.IntegrationParams.Henstock` `Real` `Real.instLE` `Real.instZero` `DFunLike.coe` `BoxIntegral.BoxAdditiveMap` `Real.instAddCommMonoid` `WithTop.some` `BoxIntegral.Box` `BoxIntegral.BoxAdditiveMap.instFunLikeBox` `Real.instLT` `Dist.dist` `PseudoMetricSpace.toDist` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ContinuousLinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `ContinuousLinearMap.funLike` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Top.top` `WithTop` `WithTop.top` `Real.instMul`	`BoxIntegral.HasIntegral`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `of_bRiemann_eq_false_of_forall_isLittleO`
`of_mul` 📖	mathematical	`BoxIntegral.IntegrationParams.RCond` `Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `BoxIntegral.integralSum` `Real.instMul`	`BoxIntegral.HasIntegral`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `BoxIntegral.hasIntegral_iff` `exists_pos_mul_lt` `Real.instIsStrictOrderedRing` `LE.le.trans` `LT.lt.le`
`smul` 📖	mathematical	`BoxIntegral.HasIntegral`	`Real` `Function.hasSMul` `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`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Filter.Tendsto.smul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `tendsto_const_nhds`
`sub` 📖	mathematical	`BoxIntegral.HasIntegral`	`Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `sub_eq_add_neg` `add` `neg`
`sum` 📖	mathematical	`BoxIntegral.HasIntegral`	`Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Finset.induction_on` `Finset.sum_insert` `add` `Finset.forall_mem_insert`
`tendsto` 📖	mathematical	`BoxIntegral.HasIntegral`	`Filter.Tendsto` `BoxIntegral.TaggedPrepartition` `BoxIntegral.integralSum` `BoxIntegral.IntegrationParams.toFilteriUnion` `Top.top` `BoxIntegral.Prepartition` `OrderTop.toTop` `BoxIntegral.Prepartition.instLE` `BoxIntegral.Prepartition.instOrderTop` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`unique` 📖	—	`BoxIntegral.HasIntegral`	—	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `tendsto_nhds_unique` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `BoxIntegral.IntegrationParams.toFilteriUnion_neBot`

BoxIntegral.Integrable

Definitions

Name	Category	Theorems
`convergenceR` 📖	CompOp	1 math math: `convergenceR_cond`
`toBoxAdditive` 📖	CompOp	1 math math: `toBoxAdditive_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`BoxIntegral.Integrable`	`Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `BoxIntegral.HasIntegral.integrable` `BoxIntegral.HasIntegral.add` `hasIntegral`
`cauchy_map_integralSum_toFilteriUnion` 📖	mathematical	`BoxIntegral.Integrable`	`Cauchy` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Filter.map` `BoxIntegral.TaggedPrepartition` `BoxIntegral.integralSum` `BoxIntegral.IntegrationParams.toFilteriUnion`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Filter.map_neBot` `BoxIntegral.IntegrationParams.toFilteriUnion_neBot` `Filter.prod_map_map_eq` `BoxIntegral.IntegrationParams.toFilter_inf_iUnion_eq` `Filter.prod_inf_prod` `Filter.prod_principal_principal` `Filter.Tendsto.mono_left` `tendsto_integralSum_toFilter_prod_self_inf_iUnion_eq_uniformity` `inf_le_inf_left` `Filter.principal_mono`
`convergenceR_cond` 📖	mathematical	`BoxIntegral.Integrable`	`BoxIntegral.IntegrationParams.RCond` `convergenceR`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `convergenceR.eq_1` `BoxIntegral.hasIntegral_iff` `hasIntegral`
`dist_integralSum_integral_le_of_memBaseSet` 📖	mathematical	`BoxIntegral.Integrable` `Real` `Real.instLT` `Real.instZero` `BoxIntegral.IntegrationParams.MemBaseSet` `convergenceR` `BoxIntegral.TaggedPrepartition.IsPartition`	`Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `BoxIntegral.integralSum` `BoxIntegral.integral`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `BoxIntegral.hasIntegral_iff` `hasIntegral` `convergenceR.eq_1`
`dist_integralSum_le_of_memBaseSet` 📖	mathematical	`BoxIntegral.Integrable` `Real` `Real.instLT` `Real.instZero` `BoxIntegral.IntegrationParams.MemBaseSet` `convergenceR` `BoxIntegral.TaggedPrepartition.iUnion`	`Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `BoxIntegral.integralSum` `Real.instAdd`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `BoxIntegral.IntegrationParams.MemBaseSet.exists_common_compl` `instIsLinearOrder_mathlib` `instLawfulOrderInf_mathlib` `dist_integralSum_integral_le_of_memBaseSet` `BoxIntegral.IntegrationParams.MemBaseSet.unionComplToSubordinate` `min_le_left` `BoxIntegral.TaggedPrepartition.isPartition_unionComplToSubordinate` `min_le_right` `BoxIntegral.integralSum_disjUnion` `dist_add_right` `NormedAddGroup.to_isIsometricVAdd_right` `LE.le.trans` `dist_triangle_right` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add`
`dist_integralSum_sum_integral_le_of_memBaseSet` 📖	mathematical	`BoxIntegral.Integrable` `Real` `Real.instLT` `Real.instZero` `BoxIntegral.IntegrationParams.MemBaseSet` `convergenceR`	`Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `BoxIntegral.integralSum` `Finset.sum` `BoxIntegral.Box` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `BoxIntegral.Prepartition.boxes` `BoxIntegral.TaggedPrepartition.toPrepartition` `BoxIntegral.integral`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq`
`dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq` 📖	mathematical	`BoxIntegral.Integrable` `Real` `Real.instLT` `Real.instZero` `BoxIntegral.IntegrationParams.MemBaseSet` `convergenceR` `BoxIntegral.TaggedPrepartition.iUnion` `BoxIntegral.Prepartition.iUnion`	`Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `BoxIntegral.integralSum` `Finset.sum` `BoxIntegral.Box` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `BoxIntegral.Prepartition.boxes` `BoxIntegral.integral`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `le_of_forall_pos_le_add` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Nat.cast_add_one_pos` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `div_pos` `Finite.of_fintype` `BoxIntegral.Prepartition.le_of_mem` `to_subbox` `instIsLinearOrder_mathlib` `instLawfulOrderInf_mathlib` `le_trans` `Finset.le_sup` `le_max_left` `BoxIntegral.IntegrationParams.exists_memBaseSet_isPartition` `BoxIntegral.IntegrationParams.MemBaseSet.mono` `le_rfl` `min_le_right` `min_le_left` `dist_integralSum_integral_le_of_memBaseSet` `BoxIntegral.IntegrationParams.biUnionTagged_memBaseSet` `le_max_right` `BoxIntegral.Prepartition.iUnion_biUnion_partition` `dist_integralSum_le_of_memBaseSet` `dist_triangle` `add_le_add` `covariant_swap_add_of_covariant_add` `BoxIntegral.integralSum_biUnionTagged` `dist_sum_sum_le_of_le` `Finset.sum_congr` `Finset.sum_const` `nsmul_eq_mul` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `ne_of_gt` `Right.add_pos_of_nonneg_of_pos` `Nat.cast_nonneg'` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.zero_mul` `Function.sometimes_spec`
`hasIntegral` 📖	mathematical	`BoxIntegral.Integrable`	`BoxIntegral.HasIntegral` `BoxIntegral.integral`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `BoxIntegral.integral.eq_1`
`mono` 📖	—	`BoxIntegral.Integrable` `BoxIntegral.IntegrationParams` `Preorder.toLE` `PartialOrder.toPreorder` `BoxIntegral.IntegrationParams.instPartialOrder`	—	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `BoxIntegral.HasIntegral.mono` `hasIntegral`
`neg` 📖	mathematical	`BoxIntegral.Integrable`	`Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `BoxIntegral.HasIntegral.integrable` `BoxIntegral.HasIntegral.neg` `hasIntegral`
`of_neg` 📖	—	`BoxIntegral.Integrable` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `neg` `neg_neg`
`of_smul` 📖	—	`BoxIntegral.Integrable` `Real` `Function.hasSMul` `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`	—	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `inv_smul_smul₀` `smul`
`smul` 📖	mathematical	`BoxIntegral.Integrable`	`Real` `Function.hasSMul` `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`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `BoxIntegral.HasIntegral.integrable` `BoxIntegral.HasIntegral.smul` `hasIntegral`
`sub` 📖	mathematical	`BoxIntegral.Integrable`	`Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `BoxIntegral.HasIntegral.integrable` `BoxIntegral.HasIntegral.sub` `hasIntegral`
`sum_integral_congr` 📖	mathematical	`BoxIntegral.Integrable` `BoxIntegral.Prepartition.iUnion`	`Finset.sum` `BoxIntegral.Box` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `BoxIntegral.Prepartition.boxes` `BoxIntegral.integral`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `tendsto_nhds_unique` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `BoxIntegral.IntegrationParams.toFilteriUnion_neBot` `tendsto_integralSum_sum_integral` `BoxIntegral.IntegrationParams.toFilteriUnion_congr`
`tendsto_integralSum_sum_integral` 📖	mathematical	`BoxIntegral.Integrable`	`Filter.Tendsto` `BoxIntegral.TaggedPrepartition` `BoxIntegral.integralSum` `BoxIntegral.IntegrationParams.toFilteriUnion` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Finset.sum` `BoxIntegral.Box` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `BoxIntegral.Prepartition.boxes` `BoxIntegral.integral`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Filter.HasBasis.tendsto_iff` `BoxIntegral.IntegrationParams.hasBasis_toFilteriUnion` `Metric.nhds_basis_closedBall` `convergenceR_cond` `dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq`
`tendsto_integralSum_toFilter_prod_self_inf_iUnion_eq_uniformity` 📖	mathematical	`BoxIntegral.Integrable`	`Filter.Tendsto` `BoxIntegral.TaggedPrepartition` `BoxIntegral.integralSum` `Filter` `Filter.instInf` `SProd.sprod` `Filter.instSProd` `BoxIntegral.IntegrationParams.toFilter` `Filter.principal` `setOf` `Set` `BoxIntegral.TaggedPrepartition.iUnion` `uniformity` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Filter.HasBasis.tendsto_iff` `Filter.HasBasis.inf_principal` `Filter.HasBasis.prod_self` `BoxIntegral.IntegrationParams.hasBasis_toFilter` `Metric.uniformity_basis_dist_le` `Nat.instAtLeastTwoHAddOfNat` `half_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `convergenceR_cond` `add_halves` `CharZero.NeZero.two` `RCLike.charZero_rclike` `dist_integralSum_le_of_memBaseSet`
`tendsto_integralSum_toFilteriUnion_single` 📖	mathematical	`BoxIntegral.Integrable` `BoxIntegral.Box` `BoxIntegral.Box.instLE`	`Filter.Tendsto` `BoxIntegral.TaggedPrepartition` `BoxIntegral.integralSum` `BoxIntegral.IntegrationParams.toFilteriUnion` `BoxIntegral.Prepartition.single` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `BoxIntegral.integral`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `to_subbox_aux` `BoxIntegral.HasIntegral.integral_eq`
`toBoxAdditive_apply` 📖	mathematical	`BoxIntegral.Integrable`	`DFunLike.coe` `BoxIntegral.BoxAdditiveMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `WithTop.some` `BoxIntegral.Box` `BoxIntegral.BoxAdditiveMap.instFunLikeBox` `toBoxAdditive` `BoxIntegral.integral`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`to_subbox` 📖	—	`BoxIntegral.Integrable` `BoxIntegral.Box` `BoxIntegral.Box.instLE`	—	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `to_subbox_aux`
`to_subbox_aux` 📖	mathematical	`BoxIntegral.Integrable` `BoxIntegral.Box` `BoxIntegral.Box.instLE`	`BoxIntegral.HasIntegral` `Filter.Tendsto` `BoxIntegral.TaggedPrepartition` `BoxIntegral.integralSum` `BoxIntegral.IntegrationParams.toFilteriUnion` `BoxIntegral.Prepartition.single` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Filter.Tendsto.comp` `BoxIntegral.IntegrationParams.tendsto_embedBox_toFilteriUnion_top` `cauchy_map_iff_exists_tendsto` `BoxIntegral.IntegrationParams.toFilteriUnion_neBot` `cauchy_map_integralSum_toFilteriUnion`

---

← Back to Index