English
Comap over a composition equals the composition of comaps: comap f (comap g μ) = comap (g ∘ f) μ, under appropriate measurability conditions.
Русский
Комап над композиционным отображением равен композиции комап: comap f (comap g μ) = comap (g ∘ f) μ, при нужной измеримости.
LaTeX
$$$\\mathrm{comap}\\ f (\\mathrm{comap}\\ g\\, \\mu) = \\mathrm{comap}\\ (g \\circ f)\\, \\mu$$$
Lean4
theorem comap_comap (hf' : ∀ s, MeasurableSet s → MeasurableSet (f '' s)) (hg : Injective g)
(hg' : ∀ s, MeasurableSet s → MeasurableSet (g '' s)) (μ : Measure γ) : comap f (comap g μ) = comap (g ∘ f) μ :=
by
by_cases hf : Injective f
· ext s hs
rw [comap_apply _ hf hf' _ hs, comap_apply _ hg hg' _ (hf' _ hs),
comap_apply _ (hg.comp hf) (fun t ht ↦ image_comp g f _ ▸ hg' _ <| hf' _ ht) _ hs, image_comp]
· rw [comap, dif_neg <| mt And.left hf, comap, dif_neg fun h ↦ hf h.1.of_comp]
