snd_compProd_prodMkLeft — Mathlib

English

Deterministic copy and parallel composition satisfy a basic equivalence with the kernel composition.

Русский

Копирование и параллельная композиция удовлетворяют базовой эквивалентности с композициями ядер.

LaTeX

$$$$ deterministic\\_copy \\parallel κ = κ \\parallel deterministic\\_copy $$$$

Lean4

@[simp]
theorem snd_compProd_prodMkLeft (κ : Kernel X Y) (η : Kernel Y Z) [IsSFiniteKernel κ] [IsSFiniteKernel η] :
    snd (κ ⊗ₖ prodMkLeft X η) = η ∘ₖ κ :=
  (comp_eq_snd_compProd η κ).symm

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