Commit 2021-11-25 07:53 5b767aac

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.