measurable_condExpKernel — Mathlib

English

For any measurable set s, the function ω ↦ condExpKernel μ m ω (s) is measurable in ω.

Русский

Для любого измеримого множества s функция ω ↦ condExpKernel μ m ω (s) измерима по ω.

LaTeX

$$$\\omega\\mapsto condExpKernel(\\mu,m)(\\omega)(s)\\quad\\text{is measurable in }\\omega\\;\\forall s\\in mΩ$$$

Lean4

theorem measurable_condExpKernel {s : Set Ω} (hs : MeasurableSet s) : Measurable[m] fun ω => condExpKernel μ m ω s :=
  (condExpKernel μ m).measurable_coe hs

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