indicator — Mathlib

English

The indicator of a measurable set times a strongly measurable function is strongly measurable.

Русский

Индикаатор множества на сильно измеримую функцию сохраняет сильную измеримость.

LaTeX

$$$\text{Measurable}(s) \Rightarrow \mathrm{StronglyMeasurable}(f) \Rightarrow \mathrm{StronglyMeasurable}(\mathbf{1}_s f)$$$

Lean4

@[measurability]
protected theorem indicator {_ : MeasurableSpace α} [TopologicalSpace β] [Zero β] (hf : StronglyMeasurable f)
    {s : Set α} (hs : MeasurableSet s) : StronglyMeasurable (s.indicator f) :=
  hf.piecewise hs stronglyMeasurable_const

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