English
The region between f and g with Ico bound is measurable on a measurable set.
Русский
Область между f и g с ограничением Ico измерима на измеримом множестве.
LaTeX
$$$$ \\mathrm{MeasurableSet}\\{ (x,t) : x \\in s ∧ t ∈ Ico(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 lower function. -/
theorem measurableSet_region_between_co (hf : Measurable f) (hg : Measurable g) (hs : MeasurableSet s) :
MeasurableSet {p : α × ℝ | p.fst ∈ s ∧ p.snd ∈ Ico (f p.fst) (g p.fst)} :=
by
dsimp only [regionBetween, Ico, mem_setOf_eq, setOf_and]
refine
MeasurableSet.inter ?_
((measurableSet_le (hf.comp measurable_fst) measurable_snd).inter
(measurableSet_lt measurable_snd (hg.comp measurable_fst)))
exact measurable_fst hs
