measurable_condDistrib — Mathlib

English

For measurable sets s, the map a ↦ condDistrib Y X μ (X a) s is measurable with respect to the comap σ-algebra mβ.comap X.

Русский

Для измеримых множеств s отображение a ↦ condDistrib Y X μ (X a) s измеримо относительно σ-алгебры обратного образа mβ.comap X.

LaTeX

$$$$ \\text{Measurable } a \\mapsto \\mathrm{condDistrib}(Y,X,μ)(X(a),\, s) \\text{ w.r.t. } mβ.comap X.$$$$

Lean4

theorem measurable_condDistrib (hs : MeasurableSet s) : Measurable[mβ.comap X] fun a => condDistrib Y X μ (X a) s :=
  (Kernel.measurable_coe _ hs).comp (Measurable.of_comap_le le_rfl)

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