English
The region between two measurable functions on a measurable set is measurable with Ioc bound on the second coordinate.
Русский
Область между измеримыми функциями на измеримом множестве измерима и Bound на второй координате Ioc.
LaTeX
$$$$ \\mathrm{MeasurableSet}\\{ (x,t) : x \\in s ∧ t ∈ Ioc(f(x),g(x)) \\}\\,. $$$$
Lean4
/-- The region between two measurable functions on a measurable set is measurable;
a version for the region together with the graph of the upper function. -/
theorem measurableSet_region_between_oc (hf : Measurable f) (hg : Measurable g) (hs : MeasurableSet s) :
MeasurableSet {p : α × ℝ | p.fst ∈ s ∧ p.snd ∈ Ioc (f p.fst) (g p.fst)} :=
by
dsimp only [regionBetween, Ioc, mem_setOf_eq, setOf_and]
refine
MeasurableSet.inter ?_
((measurableSet_lt (hf.comp measurable_fst) measurable_snd).inter
(measurableSet_le measurable_snd (hg.comp measurable_fst)))
exact measurable_fst hs
