Commit 2021-01-25 16:06 6d806348

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.