measurable_join — Mathlib

English

The map join: Measure(Measure α) → Measure α is measurable.

Русский

Отображение join: Measure(Measure α) → Measure α измеримо.

LaTeX

$$$\\text{Measurable }(\\text{join}):\\ Measurable(\\text{join}): M( M(\\,\\cdot\\, )) → M(\\cdot)$$$

Lean4

@[fun_prop]
theorem measurable_join : Measurable (join : Measure (Measure α) → Measure α) :=
  measurable_of_measurable_coe _ fun s hs => by simp only [join_apply hs, measurable_lintegral (measurable_coe hs)]

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