mem_map_restrict_ae_iff — Mathlib

English

For a measurable s and map f, t belongs to the image of the a.e. set under f iff μ((f^{-1}(t))^c ∩ s) = 0.

Русский

Для измеримого s и отображения f, множество t принадлежит образу a.e.-множества под f тогда и только тогда, когда μ((f^{-1}(t))^c ∩ s) = 0.

LaTeX

$$$\text{MeasurableSet}(s) \Rightarrow (t \in \text{map } f (\text{ae}(μ|_s))) \iff μ ((f^{-1}(t))^c \cap s) = 0.$$$

Lean4

theorem mem_map_restrict_ae_iff {β} {s : Set α} {t : Set β} {f : α → β} (hs : MeasurableSet s) :
    t ∈ Filter.map f (ae (μ.restrict s)) ↔ μ ((f ⁻¹' t)ᶜ ∩ s) = 0 := by
  rw [mem_map, mem_ae_iff, Measure.restrict_apply' hs]

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