indicator — Mathlib

English

If f is AEStronglyMeasurable, then for any measurable s the indicator s f is AEStronglyMeasurable.

Русский

Если f AEStronglyMeasurable, то для любого измеримого s индикатор s f является AEStronglyMeasurable.

LaTeX

$$$AEStronglyMeasurable(f, \mu) \Rightarrow \forall s\, MeasurableSet(s) \Rightarrow AEStronglyMeasurable(indicator\,s\,f, \mu)$$$

Lean4

@[fun_prop, measurability]
protected theorem indicator [Zero β] (hfm : AEStronglyMeasurable f μ) {s : Set α} (hs : MeasurableSet s) :
    AEStronglyMeasurable (s.indicator f) μ :=
  (aestronglyMeasurable_indicator_iff hs).mpr hfm.restrict

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