Commit 2025-01-25 09:47 974ebe9d

feat(MeasureTheory/IntegrableOn): add integrableAtFilter_atBot_iff (#21016) Add the following statement

theorem integrableAtFilter_atBot_iff : IntegrableAtFilter f atBot μ ↔ ∃ a, IntegrableOn f (Iic a) μ 

and a similar statement for atTop.