map_prodMk_right — Mathlib

English

For a finite measure μ, the map y ↦ map (fun x => { fst := x, snd := y }) μ is measurable.

Русский

Для конечной меры μ отображение y ↦ map (fun x => {fst:=x, snd:=y}) μ измеримо.

LaTeX

$$$\\text{Measurable } y \\mapsto \\mathrm{map}(\\mathrm{fun}\ x\\ y \\mapsto (x,y))\\, μ$$$

Lean4

theorem map_prodMk_right {μ : Measure α} [SFinite μ] : Measurable fun y : β => map (fun x : α => (x, y)) μ :=
  by
  apply measurable_of_measurable_coe; intro s hs
  simp_rw [map_apply measurable_prodMk_right hs]
  exact measurable_measure_prodMk_right hs

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