join_map_join — Mathlib

English

For a measure μ of measures, join (map join μ) = join (join μ).

Русский

Для меры мер выполняется: join (map join μ) = join (join μ).

LaTeX

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

Lean4

theorem join_map_join (μ : Measure (Measure (Measure α))) : join (map join μ) = join (join μ) :=
  by
  change bind μ join = join (join μ)
  rw [join_eq_bind, join_eq_bind, bind_bind aemeasurable_id aemeasurable_id]
  apply congr_arg (bind μ)
  funext ν
  exact join_eq_bind ν

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