Additive

📁 Source: Mathlib/Analysis/BoxIntegral/Partition/Additive.lean

Statistics

Metric	Count
Definitions BoxAdditiveMap, instAdd, instAddCommMonoid, instFunLikeBox, instInhabited, instSMulOfDistribMulAction, instZero, map, ofMapSplitAdd, restrict, toFun, toSMul, upperSubLower, «term_→ᵇᵃ[_]_», «term_→ᵇᵃ_»	15
Theorems coe_inj, coe_injective, coe_mk, map_apply, map_split_add, restrict_apply, sum_boxes_congr, sum_partition_boxes, sum_partition_boxes', toSMul_apply, upperSubLower_apply, zero_apply	12
Total	27

BoxIntegral

Definitions

Name	Category	Theorems
BoxAdditiveMap 📖	CompData	17 math math: BoxAdditiveMap.map_split_add, BoxAdditiveMap.zero_apply, BoxAdditiveMap.coe_injective, Integrable.toBoxAdditive_apply, BoxAdditiveMap.volume_apply, BoxAdditiveMap.coe_mk, BoxAdditiveMap.toSMul_apply, BoxAdditiveMap.sum_partition_boxes, BoxAdditiveMap.map_apply, hasIntegral_const, integralSum_sub_partitions, MeasureTheory.Measure.toBoxAdditive_apply, integral_const, Box.volume_apply, BoxAdditiveMap.coe_inj, BoxAdditiveMap.sum_boxes_congr, BoxAdditiveMap.restrict_apply
«term_→ᵇᵃ[_]_» 📖	CompOp	—
«term_→ᵇᵃ_» 📖	CompOp	—

BoxIntegral.BoxAdditiveMap

Definitions

Name	Category	Theorems
instAdd 📖	CompOp	—
instAddCommMonoid 📖	CompOp	—
instFunLikeBox 📖	CompOp	17 math math: map_split_add, zero_apply, coe_injective, BoxIntegral.Integrable.toBoxAdditive_apply, volume_apply, coe_mk, toSMul_apply, sum_partition_boxes, map_apply, BoxIntegral.hasIntegral_const, BoxIntegral.integralSum_sub_partitions, MeasureTheory.Measure.toBoxAdditive_apply, BoxIntegral.integral_const, BoxIntegral.Box.volume_apply, coe_inj, sum_boxes_congr, restrict_apply
instInhabited 📖	CompOp	—
instSMulOfDistribMulAction 📖	CompOp	—
instZero 📖	CompOp	1 math math: zero_apply
map 📖	CompOp	1 math math: map_apply
ofMapSplitAdd 📖	CompOp	—
restrict 📖	CompOp	1 math math: restrict_apply
toFun 📖	CompOp	1 math math: sum_partition_boxes'
toSMul 📖	CompOp	9 math, 5 bridge math: BoxIntegral.integrable_of_continuousOn, BoxIntegral.unitPartition.integralSum_eq_tsum_div, MeasureTheory.AEContinuous.hasBoxIntegral, BoxIntegral.integrable_of_bounded_and_ae_continuous, BoxIntegral.integral_nonneg, BoxIntegral.norm_integral_le_of_le_const, toSMul_apply, MeasureTheory.ContinuousOn.hasBoxIntegral, BoxIntegral.integrable_of_bounded_and_ae_continuousWithinAt bridge: BoxIntegral.hasIntegralIndicatorConst, MeasureTheory.SimpleFunc.hasBoxIntegral, MeasureTheory.IntegrableOn.hasBoxIntegral, BoxIntegral.HasIntegral.of_aeEq_zero, MeasureTheory.SimpleFunc.box_integral_eq_integral
upperSubLower 📖	CompOp	1 math math: upperSubLower_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_inj 📖	mathematical	—	DFunLike.coe BoxIntegral.BoxAdditiveMap BoxIntegral.Box instFunLikeBox	—	DFunLike.coe_fn_eq
coe_injective 📖	mathematical	—	BoxIntegral.BoxAdditiveMap DFunLike.coe BoxIntegral.Box instFunLikeBox	—	DFunLike.coe_injective
coe_mk 📖	mathematical	Finset.sum BoxIntegral.Box BoxIntegral.Prepartition.boxes	DFunLike.coe BoxIntegral.BoxAdditiveMap instFunLikeBox	—	—
map_apply 📖	mathematical	—	DFunLike.coe BoxIntegral.BoxAdditiveMap BoxIntegral.Box instFunLikeBox map AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddMonoidHom.instFunLike	—	—
map_split_add 📖	mathematical	WithTop BoxIntegral.Box Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder BoxIntegral.Box.instPartialOrder WithTop.some	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Option.elim' AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFunLike.coe BoxIntegral.BoxAdditiveMap instFunLikeBox BoxIntegral.Box.splitLower BoxIntegral.Box.splitUpper	—	sum_partition_boxes BoxIntegral.Prepartition.isPartitionSplit BoxIntegral.Prepartition.sum_split_boxes
restrict_apply 📖	mathematical	WithTop BoxIntegral.Box Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder BoxIntegral.Box.instPartialOrder	DFunLike.coe BoxIntegral.BoxAdditiveMap instFunLikeBox restrict	—	—
sum_boxes_congr 📖	mathematical	WithTop BoxIntegral.Box Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder BoxIntegral.Box.instPartialOrder WithTop.some BoxIntegral.Prepartition.iUnion	Finset.sum BoxIntegral.Prepartition.boxes DFunLike.coe BoxIntegral.BoxAdditiveMap instFunLikeBox	—	BoxIntegral.Prepartition.exists_splitMany_inf_eq_filter_of_finite Set.Finite.insert Set.finite_singleton Finset.sum_congr sum_partition_boxes LE.le.trans WithTop.coe_le_coe BoxIntegral.Prepartition.le_of_mem BoxIntegral.Prepartition.isPartition_splitMany BoxIntegral.Prepartition.sum_biUnion_boxes BoxIntegral.Prepartition.inf_splitMany
sum_partition_boxes 📖	mathematical	WithTop BoxIntegral.Box Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder BoxIntegral.Box.instPartialOrder WithTop.some BoxIntegral.Prepartition.IsPartition	Finset.sum BoxIntegral.Prepartition.boxes DFunLike.coe BoxIntegral.BoxAdditiveMap instFunLikeBox	—	sum_partition_boxes'
sum_partition_boxes' 📖	mathematical	WithTop BoxIntegral.Box Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder BoxIntegral.Box.instPartialOrder WithTop.some BoxIntegral.Prepartition.IsPartition	Finset.sum BoxIntegral.Prepartition.boxes toFun	—	—
toSMul_apply 📖	mathematical	—	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 BoxIntegral.BoxAdditiveMap ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup BoxIntegral.Box instFunLikeBox toSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.instAddCommMonoid	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup
upperSubLower_apply 📖	mathematical	DFunLike.coe BoxIntegral.BoxAdditiveMap AddCommGroup.toAddCommMonoid WithTop.some BoxIntegral.Box BoxIntegral.Box.face instFunLikeBox Real Set Set.instMembership Set.Icc Real.instPreorder BoxIntegral.Box.lower BoxIntegral.Box.upper	upperSubLower SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	—
zero_apply 📖	mathematical	—	DFunLike.coe BoxIntegral.BoxAdditiveMap BoxIntegral.Box instFunLikeBox instZero Pi.instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—

---

← Back to Index