Def MeasureTheory.Measure.toBoxAdditive

Modification history

2024-02-06 09:06
Mathlib/Analysis/BoxIntegral/Partition/Measure.lean
chore(Analysis/BoxIntegral): `Fintype` -> `Finite` (#10292)
Modified MeasureTheory.Measure.toBoxAdditiveView on Github →
2023-06-05 10:31
Mathlib/Analysis/BoxIntegral/Partition/Measure.lean
feat: port Analysis.BoxIntegral.Partition.Measure (#4611)
Added MeasureTheory.Measure.toBoxAdditiveView on Github →