join_map_map — Mathlib

English

For a measurable f, join (map (map f) μ) = map f (join μ).

Русский

Для измеримого отображения f выполнено: join (map (map f) μ) = map f (join μ).

LaTeX

$$$\\mathrm{join}(\\mathrm{map}(\\mathrm{map} f)\\, \\mu) = \\mathrm{map} f\\, (\\mathrm{join}\\, \\mu)$$$

Lean4

theorem join_map_map {f : α → β} (hf : Measurable f) (μ : Measure (Measure α)) :
    join (map (map f) μ) = map f (join μ) := by
  ext1 s hs
  rw [join_apply hs, map_apply hf hs, join_apply (hf hs), lintegral_map (measurable_coe hs) (measurable_map f hf)]
  simp_rw [map_apply hf hs]

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