Theorem IntervalIntegrable.comp_sub_left_iff

Modification history

2025-08-13 12:33
Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean
refactor(Intervalintegral): generalise to enorms (#27418) …
Modified IntervalIntegrable.comp_sub_left_iffView on Github →
2025-08-11 13:56
Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean
chore(IntegrableOn): generalise one more section to enorms (#27419)
Modified IntervalIntegrable.comp_sub_left_iffView on Github →
2025-04-14 15:20
Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean
feat(IntervalIntegral): add `IntervalIntegrable.trans_iff` etc (#24009)
Added IntervalIntegrable.comp_sub_left_iffView on Github →