map_apply₀ — Mathlib

English

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

Русский

Если fAEMeasurable, и s нуль-масштабируемо для μ.map f, то μ.map f s = μ(f^{-1}(s)).

LaTeX

$$$ AEMeasurable f \mu \rightarrow {s} \; NullMeasurableSet(s, \mu.map f) \Rightarrow μ.map f s = μ (f^{-1} s)$$$

Lean4

theorem map_apply₀ {f : α → β} (hf : AEMeasurable f μ) {s : Set β} (hs : NullMeasurableSet s (map f μ)) :
    μ.map f s = μ (f ⁻¹' s) :=
  by
  rw [map, dif_pos hf, mapₗ, dif_pos hf.measurable_mk] at hs ⊢
  rw [liftLinear_apply₀ _ hs, measure_congr (hf.ae_eq_mk.preimage s)]
  rfl

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