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