# Measurability criterion for ennreal-valued functions #

Consider a function `f : α → ℝ≥0∞`

. If the level sets `{f < p}`

and `{q < f}`

have measurable
supersets which are disjoint up to measure zero when `p`

and `q`

are finite numbers satisfying
`p < q`

, then `f`

is almost-everywhere measurable. This is proved in
`ENNReal.aemeasurable_of_exist_almost_disjoint_supersets`

, and deduced from an analogous statement
for any target space which is a complete linear dense order, called
`MeasureTheory.aemeasurable_of_exist_almost_disjoint_supersets`

.

Note that it should be enough to assume that the space is a conditionally complete linear order,
but the proof would be more painful. Since our only use for now is for `ℝ≥0∞`

, we keep it as simple
as possible.

If a function `f : α → β`

is such that the level sets `{f < p}`

and `{q < f}`

have measurable
supersets which are disjoint up to measure zero when `p < q`

, then `f`

is almost-everywhere
measurable. It is even enough to have this for `p`

and `q`

in a countable dense set.

If a function `f : α → ℝ≥0∞`

is such that the level sets `{f < p}`

and `{q < f}`

have measurable
supersets which are disjoint up to measure zero when `p`

and `q`

are finite numbers satisfying
`p < q`

, then `f`

is almost-everywhere measurable.