parallelComp_comp_copy — Mathlib

English

The parallel composition with a copy operator yields the product kernel; formally (κ ∥ₖ η) ∘ₖ copy α = κ ×ₖ η.

Русский

Параллельная композиция с оператором копирования даёт ядро произведения: (κ ∥ₖ η) ∘ₖ copy α = κ ×ₖ η.

LaTeX

$$$$(κ ∥ₖ η) \\circₖ copy α = κ ×ₖ η.$$$$

Lean4

theorem parallelComp_comp_copy (κ : Kernel α β) (η : Kernel α γ) : (κ ∥ₖ η) ∘ₖ copy α = κ ×ₖ η :=
  rfl

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