measurable_densityProcess_right — Mathlib

English

The left-densityProcess density on p ↦ densityProcess κ ν n p.1 p.2 s is measurable.

Русский

Левая плотность densityProcess κ ν n p.1 p.2 s измерима.

LaTeX

$$$\mathsf{Measurable}\big( p \mapsto \text{densityProcess}(\kappa,\nu,n,p.1,p.2,s) \big)$$$

Lean4

theorem measurable_densityProcess_right (κ : Kernel α (γ × β)) (ν : Kernel α γ) (n : ℕ) {s : Set β} (a : α)
    (hs : MeasurableSet s) : Measurable (fun x ↦ densityProcess κ ν n a x s) :=
  ((measurable_densityProcess κ ν n hs).comp (measurable_const.prodMk measurable_id) :)

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