map_toOuterMeasure — Mathlib

English

If f is not aemeasurable, then the image measure is zero (reiterated variant).

Русский

Если f не a.e.-измеримо, то образующая мера нулевая.

LaTeX

$$$ \neg \mathrm{AEMeasurable}(f, \mu) \Rightarrow (\mu.map f) = 0 $$$

Lean4

theorem map_toOuterMeasure (hf : AEMeasurable f μ) :
    (μ.map f).toOuterMeasure = (OuterMeasure.map f μ.toOuterMeasure).trim :=
  by
  rw [← trimmed, OuterMeasure.trim_eq_trim_iff]
  intro s hs
  simp [hf, hs]

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