preimage_null_of_map_null — Mathlib

English

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

Русский

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

LaTeX

$$$ \mu( f^{-1}(s) ) = \mu(s) \quad\text{if } (\mu.map f) = \mu \text{ and } s \text{ null-measurable} $$$

Lean4

/-- Even if `s` is not measurable, `map f μ s = 0` implies that `μ (f ⁻¹' s) = 0`. -/
theorem preimage_null_of_map_null {f : α → β} (hf : AEMeasurable f μ) {s : Set β} (hs : μ.map f s = 0) :
    μ (f ⁻¹' s) = 0 :=
  nonpos_iff_eq_zero.mp <| (le_map_apply hf s).trans_eq hs

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