stronglyMeasurable_condExpKernel — Mathlib

English

For any measurable set s, the map ω ↦ condExpKernel μ m ω s is a strongly measurable function of ω.

Русский

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

LaTeX

$$$\\text{StronglyMeasurable}_{m}(\\omega\\mapsto condExpKernel(\\mu,m)(\\omega)(s))$$$

Lean4

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

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