measurable_bind' — Mathlib

English

If g: α → M(β) is a measurable map, then the map from M(α) to M(β) given by m ↦ bind m g is measurable.

Русский

Если g: α → M(β) измерима, то отображение m ↦ bind m g из пространста мер α в β измеримо.

LaTeX

$$$\text{Measurable}(g) \Rightarrow \text{Measurable}(m \mapsto \operatorname{bind}(m, g))$$$

Lean4

@[fun_prop]
theorem measurable_bind' {g : α → Measure β} (hg : Measurable g) : Measurable fun m : Measure α => bind m g :=
  measurable_join.comp (measurable_map _ hg)

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