measurable_kernel_prodMk_right — Mathlib

English

If s ⊆ (β × γ) is measurable, then for each a, the value b ↦ η(a,b)(Prod.mk b ⁻¹' s) is a measurable function of b.

Русский

Если s ⊆ (β × γ) измеримо, то для каждого a функция b ↦ η(a,b)(Prod.mk b ⁻¹' s) измерима по b.

LaTeX

$$$\\forall a,\\; \\text{Measurable}\\bigl(b \\mapsto \\eta(a,b)(\\mathrm{Prod.mk}\\, b^{-1}'s)\\bigr)$$$

Lean4

theorem measurable_kernel_prodMk_right [IsSFiniteKernel κ] {s : Set (β × α)} (hs : MeasurableSet s) :
    Measurable fun y => κ y ((fun x => (x, y)) ⁻¹' s) :=
  measurable_kernel_prodMk_left (measurableSet_swap_iff.mpr hs)

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