Theorem ContinuousOn.integrableOn_compact

Modification history

2023-11-07 13:31
Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
feat: bound the measure of a set by the integral of a function, from above and from below (#8123) …
Modified ContinuousOn.integrableOn_compactView on Github →
2023-06-01 05:57
Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
feat: port MeasureTheory.Function.LocallyIntegrable (#4524)
Added ContinuousOn.integrableOn_compactView on Github →