map_comp_right — Mathlib

English

For a measurable equivalence f, κ.map f = η iff κ = η.map f^{-1}.

Русский

Для измеримого эквивалента f: κ.map f = η тогда и только если κ = η.map f^{-1}.

LaTeX

$$$$\\kappa.map f = \\eta \\iff \\kappa = \\eta.map f^{-1}.$$$$

Lean4

theorem map_comp_right (κ : Kernel α β) {f : β → γ} (hf : Measurable f) {g : γ → δ} (hg : Measurable g) :
    κ.map (g ∘ f) = (κ.map f).map g := by
  ext1 x
  rw [map_apply _ hg, map_apply _ hf, Measure.map_map hg hf, ← map_apply _ (hg.comp hf)]

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