map_apply_of_aemeasurable — Mathlib

English

If f is AEMeasurable and s is measurable, then μ.map f s = μ(f^{-1}(s)).

Русский

Если f является a.e.-измеримой и s является измеримым, то μ.map f s = μ(f^{-1}(s)).

LaTeX

$$$ (\text{AEMeasurable } f \mu) \rightarrow (s: \text{Set } \Beta) \rightarrow \text{MeasurableSet } s \Rightarrow μ.map f s = μ (f^{-1} s) $$$

Lean4

/-- We can evaluate the pushforward on measurable sets. For non-measurable sets, see
  `MeasureTheory.Measure.le_map_apply` and `MeasurableEquiv.map_apply`. -/
@[simp]
theorem map_apply_of_aemeasurable (hf : AEMeasurable f μ) {s : Set β} (hs : MeasurableSet s) :
    μ.map f s = μ (f ⁻¹' s) :=
  map_apply₀ hf hs.nullMeasurableSet

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