English
If s is measurable and f and g are strongly measurable, then the piecewise function with respect to s is strongly measurable.
Русский
Если s измеримо и f, g сильно измеримы, то s.piecewise(f,g) сильно измеримо.
LaTeX
$$$\text{MeasurableSet}(s) \land \mathrm{StronglyMeasurable}(f) \land \mathrm{StronglyMeasurable}(g) \Rightarrow \mathrm{StronglyMeasurable}(\mathrm{Set.piecewise}\ s\ f\ g)$$$
Lean4
protected theorem piecewise {m : MeasurableSpace α} [TopologicalSpace β] {s : Set α} {_ : DecidablePred (· ∈ s)}
(hs : MeasurableSet s) (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) :
StronglyMeasurable (Set.piecewise s f g) :=
by
refine ⟨fun n => SimpleFunc.piecewise s hs (hf.approx n) (hg.approx n), fun x => ?_⟩
by_cases hx : x ∈ s
· simpa [@Set.piecewise_eq_of_mem _ _ _ _ _ (fun _ => Classical.propDecidable _) _ hx, hx] using hf.tendsto_approx x
·
simpa [@Set.piecewise_eq_of_notMem _ _ _ _ _ (fun _ => Classical.propDecidable _) _ hx, hx] using
hg.tendsto_approx x
