prodMkLeft_comp_compProd — Mathlib

English

For η : Kernel β γ, the identity (η.prodMkLeft α) ∘ₘ μ ⊗ₘ κ equals η ∘ₘ κ ∘ₘ μ.

Русский

Для η: Kernel β γ, (η.prodMkLeft α) ∘ μ ⊗ κ = η ∘ κ ∘ μ.

LaTeX

$$$[SFinite(\\mu)] [IsSFiniteKernel(κ)] : (\\eta.prodMkLeft α) \\circ_{m} \\mu \\otimes_{m} \\kappa = \\eta \\circ_{m} \\kappa \\circ_{m} \\mu$$$

Lean4

@[simp]
theorem prodMkLeft_comp_compProd {η : Kernel β γ} [SFinite μ] [IsSFiniteKernel κ] :
    (η.prodMkLeft α) ∘ₘ μ ⊗ₘ κ = η ∘ₘ κ ∘ₘ μ := by
  rw [← snd_compProd μ κ, Kernel.prodMkLeft, snd, ← deterministic_comp_eq_map measurable_snd, comp_assoc,
    Kernel.comp_deterministic_eq_comap]

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