compProd_eq_parallelComp_comp_copy_comp

English

Let κ: γ→β, η: ε→β′, ξ: (ε×β)→δ, f γ→ε deterministic. Then (ξ ×ₖ η.prodMkRight β) ∘ₖ (deterministic f hf ×ₖ κ) equals (ξ ∘ₖ (deterministic f hf ×ₖ κ)) ×ₖ (η ∘ₖ deterministic f hf).

Русский

Пусть κ: γ→β, η: ε→β′, ξ: (ε×β)→δ и f: γ→ε детерминировано. Тогда (ξ ×ₖ η.prodMkRight β) ∘ₖ (deterministic f hf ×ₖ κ) = (ξ ∘ₖ (deterministic f hf ×ₖ κ)) ×ₖ (η ∘ₖ deterministic f hf).

LaTeX

$$$$(\\xi ×_k η.{\\text{prodMkRight } β}) ∘_k (deterministic f hf ×_k κ) = (\\xi ∘_k (deterministic f hf ×_k κ)) ×_k (η ∘_k deterministic f hf).$$$$

Lean4

theorem compProd_eq_parallelComp_comp_copy_comp [SFinite μ] : μ ⊗ₘ κ = (Kernel.id ∥ₖ κ) ∘ₘ Kernel.copy α ∘ₘ μ :=
  by
  by_cases hκ : IsSFiniteKernel κ
  swap; · simp [hκ]
  rw [compProd_eq_comp_prod, ← Kernel.parallelComp_comp_copy, Measure.comp_assoc]

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