map_prodMk_left — Mathlib

English

For a finite measure ν, the map x ↦ map (Prod.mk x) ν is measurable.

Русский

Для конечной меры ν отображение x ↦ map (Prod.mk x) ν измеримо.

LaTeX

$$$\\text{Measurable } x \\mapsto \\mathrm{map}(\\mathrm{Prod.mk}\,x)\\, ν$$$

Lean4

theorem map_prodMk_left [SFinite ν] : Measurable fun x : α => map (Prod.mk x) ν :=
  by
  apply measurable_of_measurable_coe; intro s hs
  simp_rw [map_apply measurable_prodMk_left hs]
  exact measurable_measure_prodMk_left hs

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