Commit 2023-01-31 16:05 aa1d645a

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.