Def BoxIntegral.BoxAdditiveMap.restrict

Modification history

2023-05-23 16:17

Mathlib/Analysis/BoxIntegral/Partition/Additive.lean

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

Added BoxIntegral.BoxAdditiveMap.restrict View on Github →