indicator₀ — Mathlib

English

If f is almost everywhere measurable with respect to μ, then s.indicator f is almost everywhere μ-measurable whenever s is null-measurable.

Русский

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

LaTeX

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

Lean4

theorem indicator₀ (hfm : AEMeasurable f μ) {s} (hs : NullMeasurableSet s μ) : AEMeasurable (s.indicator f) μ :=
  (aemeasurable_indicator_iff₀ hs).mpr hfm.restrict

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