English
If s is a measurable set and f,g are measurable, then the piecewise function that equals f on s and g off s is measurable.
Русский
Если s измеримо, а f,g измеримы, то функция piecewise s f g измерима.
LaTeX
$$$\\text{MeasurableSet } s \\to \\text{Measurable } f \\to \\text{Measurable } g \\to \\text{Measurable } (s.piecewise f g)$$$
Lean4
@[measurability, fun_prop]
protected theorem piecewise {_ : DecidablePred (· ∈ s)} (hs : MeasurableSet s) (hf : Measurable f) (hg : Measurable g) :
Measurable (piecewise s f g) := by
intro t ht
rw [piecewise_preimage]
exact hs.ite (hf ht) (hg ht)