English
A variant of piecewise, using a measurable predicate, yields strong measurability.
Русский
Вариант с условной конструкцией: при измеримом предикате f на α → β остаётся сильно измеримой.
LaTeX
$$$\forall p, \text{MeasurableSet}\{a\mid p(a)\} \Rightarrow \mathrm{StronglyMeasurable}(\lambda x. \text{ite}(p(x), f(x), g(x)))$$$
Lean4
/-- this is slightly different from `StronglyMeasurable.piecewise`. It can be used to show
`StronglyMeasurable (ite (x=0) 0 1)` by
`exact StronglyMeasurable.ite (measurableSet_singleton 0) stronglyMeasurable_const
stronglyMeasurable_const`, but replacing `StronglyMeasurable.ite` by
`StronglyMeasurable.piecewise` in that example proof does not work. -/
protected theorem ite {_ : MeasurableSpace α} [TopologicalSpace β] {p : α → Prop} {_ : DecidablePred p}
(hp : MeasurableSet {a : α | p a}) (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) :
StronglyMeasurable fun x => ite (p x) (f x) (g x) :=
StronglyMeasurable.piecewise hp hf hg
