# Commit 2021-01-25 16:06 6d806348

View on Github →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.