Theorem MeasureTheory.IntegrableOn.of_inter_support

Modification history

2025-09-23 12:05

Mathlib/MeasureTheory/Integral/IntegrableOn.lean

feat(MeasureTheory/Integral/IntegrableOn): add `IntegrableOn.of_inter_support` (#29895) …

Added MeasureTheory.IntegrableOn.of_inter_support View on Github →