Commit 2023-05-23 16:17 ab19baaf

View on Github →

feat: port Analysis.BoxIntegral.Partition.Additive (#4054)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/BoxIntegral/Partition/Additive.lean

added theorem BoxIntegral.BoxAdditiveMap.coe_inj

added theorem BoxIntegral.BoxAdditiveMap.coe_injective

added theorem BoxIntegral.BoxAdditiveMap.coe_mk

added def BoxIntegral.BoxAdditiveMap.map

added theorem BoxIntegral.BoxAdditiveMap.map_split_add

added def BoxIntegral.BoxAdditiveMap.ofMapSplitAdd

added def BoxIntegral.BoxAdditiveMap.restrict

added theorem BoxIntegral.BoxAdditiveMap.sum_boxes_congr

added theorem BoxIntegral.BoxAdditiveMap.sum_partition_boxes

added def BoxIntegral.BoxAdditiveMap.toSmul

added theorem BoxIntegral.BoxAdditiveMap.toSmul_apply

added def BoxIntegral.BoxAdditiveMap.upperSubLower.{u}

added structure BoxIntegral.BoxAdditiveMap