Measurability of unordered-interval threshold crossings

The event {ω | t ∈ Set.uIoc (f ω) (g ω)} that a threshold t lies in the unordered half-open interval between two measurable real functions is measurable (measurableSet_setOf_mem_uIoc).

Main results

• measurableSet_setOf_mem_uIoc: {ω | t ∈ Ι (f ω) (g ω)} is measurable for measurable f, g.

theorem measurableSet_setOf_mem_uIoc {Ω : Type u_1} [MeasurableSpace Ω] {f g : Ω → ℝ} (hf : Measurable f) (hg : Measurable g) (t : ℝ) : MeasurableSet {ω : Ω | t ∈ Set.uIoc (f ω) (g ω)}

The event that a threshold lies between two measurable real functions is measurable.