measurableSet_regionBetween — Mathlib

English

If f,g are measurable and s is measurable, then regionBetween(f,g,s) is measurable.

Русский

Если f,g измеримы и s измеримо, то regionBetween(f,g,s) измеримо.

LaTeX

$$$$ \\text{MeasurableSet}(\\mathrm{regionBetween}(f,g,s)). $$$$

Lean4

/-- The region between two measurable functions on a measurable set is measurable. -/
theorem measurableSet_regionBetween (hf : Measurable f) (hg : Measurable g) (hs : MeasurableSet s) :
    MeasurableSet (regionBetween f g s) :=
  by
  dsimp only [regionBetween, Ioo, mem_setOf_eq, setOf_and]
  refine
    MeasurableSet.inter ?_
      ((measurableSet_lt (hf.comp measurable_fst) measurable_snd).inter
        (measurableSet_lt measurable_snd (hg.comp measurable_fst)))
  exact measurable_fst hs

Похожие утверждения