mathlib

aa1d645a - chore(measure_theory/integrals): API improvements for interval_integrable (#18335)

chore(measure_theory/integrals): API improvements for interval_integrable (#18335) This moves some lemmas which had ended up in a duplicated namespace `interval_integral.interval_integrable`, and fills in a couple of obvious lemmas which were missing.