English
If f is continuous on a set s and g is continuous on its complement s^c, and s is measurable, then the piecewise function that equals f on s and g on s^c is measurable.
Русский
Если f непрерывна на s, а g непрерывна на дополнении s^c, и s измеримо, то функция piecewise f g измерима на всей области.
LaTeX
$$$\\forall f,g:\\alpha\\to\\gamma\\,\\{s:\\mathrm{Set}\\alpha\\},\\ hf:\\mathrm{ContinuousOn}(f,s)\\ \\ hg:\\mathrm{ContinuousOn}(g,s^c)\\ \\ hs:\\mathrm{MeasurableSet}(s)\\Rightarrow\\mathrm{Measurable}(s.piecewise f g)$$$
Lean4
/-- If a function is defined piecewise in terms of functions which are continuous on their
respective pieces, then it is measurable. -/
theorem measurable_piecewise {f g : α → γ} {s : Set α} [∀ j : α, Decidable (j ∈ s)] (hf : ContinuousOn f s)
(hg : ContinuousOn g sᶜ) (hs : MeasurableSet s) : Measurable (s.piecewise f g) :=
by
refine measurable_of_isOpen fun t ht => ?_
rw [piecewise_preimage, Set.ite]
apply MeasurableSet.union
· rcases _root_.continuousOn_iff'.1 hf t ht with ⟨u, u_open, hu⟩
rw [hu]
exact u_open.measurableSet.inter hs
· rcases _root_.continuousOn_iff'.1 hg t ht with ⟨u, u_open, hu⟩
rw [diff_eq_compl_inter, inter_comm, hu]
exact u_open.measurableSet.inter hs.compl
