preimage_null — Mathlib

English

If f is quasi-measure-preserving and μb assigns measure zero to s, then μa assigns measure zero to f^{-1}(s).

Русский

Если f квази-сохраняет и μb(s) = 0, тогда μa(f^{-1}(s)) = 0.

LaTeX

$$preimage_null (h : QuasiMeasurePreserving f μa μb) {s : Set β} (hs : μb s = 0) : μa (f ⁻¹' s) = 0$$

Lean4

theorem preimage_null (h : QuasiMeasurePreserving f μa μb) {s : Set β} (hs : μb s = 0) : μa (f ⁻¹' s) = 0 :=
  preimage_null_of_map_null h.aemeasurable (h.2 hs)

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