indicator — Mathlib

English

If f is almost everywhere measurable with respect to μ and s is a measurable set, then s.indicator f is almost everywhere measurable with respect to μ.

Русский

Если f а.е.-измеримая относительно μ и s — измеримое множество, то s.indicator f а.е.-измерима относительно μ.

LaTeX

$$$\mathrm{AEMeasurable}(f, μ) \rightarrow \forall \{s\},\mathrm{MeasurableSet}(s)\rightarrow \mathrm{AEMeasurable}(s.indicator f, μ)$$$

Lean4

@[measurability]
theorem indicator (hfm : AEMeasurable f μ) {s} (hs : MeasurableSet s) : AEMeasurable (s.indicator f) μ :=
  (aemeasurable_indicator_iff hs).mpr hfm.restrict

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