map_measureReal_apply — Mathlib

English

If f is a measurable map between spaces and s is a measurable set in the target, then the real-valued measure of μ mapped along f evaluated at s equals μ.real evaluated at the preimage f^{-1}(s).

Русский

Пусть f: α → β измерима; для измеримой области s в β выполняется: (μ.map f).real(s) = μ.real(f^{-1}(s)).

LaTeX

$$$ (\\mu \\mapsto f)_\\ast \\mu .real(s) = \\mu.real(f^{-1}(s)) $$$

Lean4

theorem map_measureReal_apply [MeasurableSpace β] {f : α → β} (hf : Measurable f) {s : Set β} (hs : MeasurableSet s) :
    (μ.map f).real s = μ.real (f ⁻¹' s) := by simp_rw [measureReal_def, map_apply hf hs]

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