# Commit 2021-01-03 23:18 96948e45

View on Github →feat(measure_theory): almost everywhere measurable functions (#5568)
This PR introduces a notion of almost everywhere measurable function, i.e., a function which coincides almost everywhere with a measurable function, and builds a basic API around the notion. It will then be used in #5510 to extend the Bochner integral. The main new definition in the PR is `h : ae_measurable f μ`

. It comes with `h.mk f`

building a measurable function that coincides almost everywhere with `f`

(these assertions are respectively `h.measurable_mk`

and `h.ae_eq_mk`

).