map_map_of_aemeasurable — Mathlib

English

If g is AEMeasurable with μ.map f and f is AEMeasurable with μ, then μ.map f maps through g to γ as g ∘ f.

Русский

Если g — AЕ-измеримая относительно μ.map f, а f — AЕ-измеримая относительно μ, тогда отображение μ проходит через g: μ.map f под g.

LaTeX

$$$\mathrm{AEMeasurable}(g, \mu\map f) \rightarrow \mathrm{AEMeasurable}(f, \mu) \rightarrow \mathrm{Eq}(\mathrm{map}\ g (\mathrm{map}\ f \mu), \mathrm{map}\ (g \circ f) \mu)$$$

Lean4

theorem map_map_of_aemeasurable {g : β → γ} {f : α → β} (hg : AEMeasurable g (Measure.map f μ))
    (hf : AEMeasurable f μ) : (μ.map f).map g = μ.map (g ∘ f) :=
  by
  ext1 s hs
  rw [map_apply_of_aemeasurable hg hs, map_apply₀ hf (hg.nullMeasurable hs),
    map_apply_of_aemeasurable (hg.comp_aemeasurable hf) hs, preimage_comp]

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