Theorem volume_regionBetween_eq_integral

Modification history

2023-06-08 18:26
Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean
feat: port MeasureTheory.Measure.Lebesgue.Integral (#4734)
Added volume_regionBetween_eq_integralView on Github →