mathlib3

5b767aac - feat(measure_theory/integral/integral_eq_improper): weaken measurability assumptions (#10387)

feat(measure_theory/integral/integral_eq_improper): weaken measurability assumptions (#10387) As suggested by @fpvandoorn, this removes a.e. measurability assumptions which could be deduced from integrability assumptions. More of them could be removed assuming the codomain is a `borel_space` and not only an `open_measurable_space`, but I’m not sure wether or not it would be a good idea.