nullMeasurableSet_preimage — Mathlib

English

If f is AEMeasurable and s is a measurable set, then the preimage f^{-1}[s] is NullMeasurable.

Русский

Если f является а.е.-измеримой, и s измеримо, то прообраз f^{-1}[s] нулевомериен по μ.

LaTeX

$$AEMeasurable f μ → MeasurableSet s → NullMeasurableSet (f^{-1}' s) μ$$

Lean4

theorem _root_.AEMeasurable.nullMeasurableSet_preimage {f : α → β} {s : Set β} (hf : AEMeasurable f μ)
    (hs : MeasurableSet s) : NullMeasurableSet (f ⁻¹' s) μ :=
  hf.nullMeasurable hs

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