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.

theorem MeasureTheory.aemeasurable_of_exist_almost_disjoint_supersets {α : Type u_1} {m : MeasurableSpace α} (μ : Measure α) {β : Type u_2} [CompleteLinearOrder β] [DenselyOrdered β] [TopologicalSpace β] [OrderTopology β] [SecondCountableTopology β] [MeasurableSpace β] [BorelSpace β] (s : Set β) (s_count : s.Countable) (s_dense : Dense s) (f : α → β) (h : ∀ (p : β), Membership.mem s p → ∀ (q : β), Membership.mem s q → LT.lt p q → Exists fun (u : Set α) => Exists fun (v : Set α) => And (MeasurableSet u) (And (MeasurableSet v) (And (HasSubset.Subset (setOf fun (x : α) => LT.lt (f x) p) u) (And (HasSubset.Subset (setOf fun (x : α) => LT.lt q (f x)) v) (Eq (DFunLike.coe μ (Inter.inter u v)) 0))))) : AEMeasurable f μ

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.

theorem ENNReal.aemeasurable_of_exist_almost_disjoint_supersets {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ENNReal) (h : ∀ (p q : NNReal), LT.lt p q → Exists fun (u : Set α) => Exists fun (v : Set α) => And (MeasurableSet u) (And (MeasurableSet v) (And (HasSubset.Subset (setOf fun (x : α) => LT.lt (f x) (ofNNReal p)) u) (And (HasSubset.Subset (setOf fun (x : α) => LT.lt (ofNNReal q) (f x)) v) (Eq (DFunLike.coe μ (Inter.inter u v)) 0))))) : AEMeasurable f μ

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.