map_ae — Mathlib

English

Under a MeasurableEquiv f, the image of the a.e. filter of μ is the a.e. filter of μ.map f.

Русский

При отображении MeasurableEquiv f образа почти всюду фильтра меры μ совпадает с почти всюду фильтром меры μ.map f.

LaTeX

$$$$\\forall f:\\alpha \\simeq\\beta,\\; \\mathrm{AE}(f)\\,\\mu\\;\\rightarrow\\; \\mathrm{map}\; f\\,(\\mathrm{ae}\\,\\mu) = \\mathrm{ae}\\,(\\mathrm{map}\\ f\\,\\mu).$$$$

Lean4

theorem map_ae (f : α ≃ᵐ β) (μ : Measure α) : Filter.map f (ae μ) = ae (map f μ) :=
  by
  ext s
  simp_rw [mem_map, mem_ae_iff, ← preimage_compl, f.map_apply]

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