mathlib3

6d806348 - feat(measure_theory/{measure_space, borel_space, integration}): prove ae_measurable for various limits (#5849)

feat(measure_theory/{measure_space, borel_space, integration}): prove ae_measurable for various limits (#5849) For a sequence of `ae_measurable` functions verifying some pointwise property almost everywhere, introduce a sequence of measurable functions verifying the same property and use it to prove ae-measurability of `is_lub`, `is_glb`, `supr`, `infi`, and almost everywhere pointwise limit. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Rémy Degenne <remydegenne@gmail.com>