mathlib3

733fa004 - feat(measure_theory/integral): integration lemmas from #18392 (#18466)

feat(measure_theory/integral): integration lemmas from #18392 (#18466) Some lemmas about integration of continuous functions split off from my Poisson-summation / zeta-functions project at #18392.