mathlib3

93df724a - feat(measure_theory/integral/integral_eq_improper): Covering finite intervals by finite intervals (#13514)

feat(measure_theory/integral/integral_eq_improper): Covering finite intervals by finite intervals (#13514) Currently, the ability to prove facts about improper integrals only allows for at least one infinite endpoint. However, it is a common need to work with functions that blow up at an end point (e.g., x^r on [0, 1] for r in (-1, 0)). As a step toward allowing that, we introduce `ae_cover`s that allow exhausting finite intervals by finite intervals. Partially addresses: #12666