Commit 2023-06-05 10:31 84b0637c

View on Github →

feat: port Analysis.BoxIntegral.Partition.Measure (#4611)

Estimated changes

Modified Mathlib.lean

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

added theorem BoxIntegral.Box.Ioo_ae_eq_Icc

added theorem BoxIntegral.Box.coe_ae_eq_Icc

added theorem BoxIntegral.Box.measurableSet_Icc

added theorem BoxIntegral.Box.measurableSet_Ioo

added theorem BoxIntegral.Box.measurableSet_coe

added theorem BoxIntegral.Box.measure_Icc_lt_top

added theorem BoxIntegral.Box.measure_coe_lt_top

added theorem BoxIntegral.Box.volume_apply'

added theorem BoxIntegral.Box.volume_apply

added theorem BoxIntegral.Box.volume_face_mul

added theorem BoxIntegral.BoxAdditiveMap.volume_apply

added theorem BoxIntegral.Prepartition.measure_iUnion_toReal

added def MeasureTheory.Measure.toBoxAdditive