aemeasurable_indicator_iff₀ — Mathlib

English

If s is null-measurable, then AEMeasurable (indicator s f) μ is equivalent to AEMeasurable f (μ.restrict s).

Русский

Если s является нулево измеримым множеством, то AЕмeасуемость (indicator s f) относительно μ эквивалентна AЕмeасуемости f относительно μ ограниченного до s.

LaTeX

$$$\mathrm{AEMeasurable}(\mathrm{indicator}\ s\ f,\ μ) \iff \mathrm{AEMeasurable}(f,\ μ.restrict s)$$$

Lean4

theorem aemeasurable_indicator_iff₀ {s} (hs : NullMeasurableSet s μ) :
    AEMeasurable (indicator s f) μ ↔ AEMeasurable f (μ.restrict s) :=
  by
  rcases hs with ⟨t, ht, hst⟩
  rw [← aemeasurable_congr (indicator_ae_eq_of_ae_eq_set hst.symm), aemeasurable_indicator_iff ht,
    restrict_congr_set hst]

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