piecewise — Mathlib

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)

Похожие утверждения