English
If g and f are measurable, then mapping by f and then by g equals mapping by g ∘ f: μ.map g (μ.map f) = μ.map (g ∘ f).
Русский
Если g и f измеримы, то последовательное отображение даёт эквивалентный образ: μ.map g (μ.map f) = μ.map (g ∘ f).
LaTeX
$$$ (\mu.map f).map g = \mu.map (g \circ f) $ for measurable g,f$$
Lean4
/-- Mapping a measure twice is the same as mapping the measure with the composition. This version is
for measurable functions. See `map_map_of_aemeasurable` when they are just ae measurable. -/
theorem map_map {g : β → γ} {f : α → β} (hg : Measurable g) (hf : Measurable f) : (μ.map f).map g = μ.map (g ∘ f) :=
ext fun s hs => by simp [hf, hg, hs, hg hs, hg.comp hf, ← preimage_comp]
