mem_ae_map_iff — Mathlib

English

For AEMeasurable f with MeasurableSet s, s ∈ ae(μ.map f) iff f^{-1}(s) ∈ ae μ.

Русский

Для AEMеас measurable f и измеримого s: s принадлежит ae(μ.map f) тогда и только тогда, когда f^{-1}(s) принадлежит ae μ.

LaTeX

$$$ s \in ae (\mu.map f) \iff f^{-1}(s) \in ae \mu $$$

Lean4

theorem mem_ae_map_iff {f : α → β} (hf : AEMeasurable f μ) {s : Set β} (hs : MeasurableSet s) :
    s ∈ ae (μ.map f) ↔ f ⁻¹' s ∈ ae μ := by
  simp only [mem_ae_iff, map_apply_of_aemeasurable hf hs.compl, preimage_compl]

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