mapOfMeasurable — Mathlib

English

For a finite μ and kernel κ, the composition μ ⊗ₘ (κ.map f) equals (μ ⊗ₘ κ).map (Prod.map id f).

Русский

Для конечной меры μ и ядра κ выполняется равно μ ⊗ₘ (κ.map f) = (μ ⊗ₘ κ).map (Prod.map id f).

LaTeX

$$$$\\mu \\otimes_m (\\kappa.map f) = (\\mu \\otimes_m \\kappa).map (Prod.map id f).$$$$

Lean4

/-- The pushforward of a kernel along a measurable function. This is an implementation detail,
use `map κ f` instead. -/
noncomputable def mapOfMeasurable (κ : Kernel α β) (f : β → γ) (hf : Measurable f) : Kernel α γ
    where
  toFun a := (κ a).map f
  measurable' := by fun_prop

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