posterior_prod_id_comp — Mathlib

English

The posterior composed with identity in a product setting equals the product of μ and κ.

Русский

Постериорная композиция с идентичностью в произведении равна произведению μ и κ.

LaTeX

$$$(κ†μ) \\otimes κ = μ \\otimes κ$$$

Lean4

theorem posterior_prod_id_comp : (κ†μ ×ₖ Kernel.id) ∘ₘ κ ∘ₘ μ = μ ⊗ₘ κ := by
  rw [← Kernel.swap_prod, ← Measure.comp_assoc, ← Measure.compProd_eq_comp_prod, compProd_posterior_eq_swap_comp,
    Measure.comp_assoc, Kernel.swap_swap, Measure.id_comp]

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