swap_compProd_posterior — Mathlib

English

A canonical rearrangement shows the swap of components in the posterior decomposition.

Русский

Каноническое перераспределение демонстрирует перестановку компонентов в постериорном разложении.

LaTeX

$$$Kernel.swap Ω 𝓧 \\circ (κ ∘ μ) ⊗ κ†μ = μ ⊗ κ$$$

Lean4

theorem swap_compProd_posterior : Kernel.swap 𝓧 Ω ∘ₘ (κ ∘ₘ μ) ⊗ₘ κ†μ = μ ⊗ₘ κ := by
  rw [compProd_posterior_eq_swap_comp, Measure.comp_assoc, Kernel.swap_swap, Measure.id_comp]

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