English
If p is a measurable predicate and f,g are measurable, then the function x ↦ ite (p x) (f x) (g x) is measurable.
Русский
Если p измеримо и f,g измеримы, то функция x ↦ ite(p x) f(x) g(x) измерима.
LaTeX
$$$\\forall p : \\alpha \\to \\text{Prop}, {\\_}:\\DecidablePred p \\to \\text{MeasurableSet } \\{a : \\alpha | p a\\} \\to \\text{Measurable } f \\to \\text{Measurable } g \\to \\text{Measurable } (\\lambda x \\mapsto \\text{ite } (p x) (f x) (g x))$$$
Lean4
/-- This is slightly different from `Measurable.piecewise`. It can be used to show
`Measurable (ite (x=0) 0 1)` by
`exact Measurable.ite (measurableSet_singleton 0) measurable_const measurable_const`,
but replacing `Measurable.ite` by `Measurable.piecewise` in that example proof does not work. -/
theorem ite {p : α → Prop} {_ : DecidablePred p} (hp : MeasurableSet {a : α | p a}) (hf : Measurable f)
(hg : Measurable g) : Measurable fun x => ite (p x) (f x) (g x) :=
Measurable.piecewise hp hf hg
