parallelComp_comp_parallelComp — Mathlib

English

Parallel composition with identity and other kernels equals swapping to a parallel formation.

Русский

Параллельная композиция с идентичностью и другим ядром эквивалентна формированию параллельной композиции.

LaTeX

$$$$ (ξ \\parallelₖ Kernel.id) ∘ₖ (η \\parallelₖ κ) = (ξ ∘ₖ η) \\parallelₖ κ $$$$

Lean4

theorem parallelComp_comp_parallelComp [IsSFiniteKernel κ] {η : Kernel Y Z} [IsSFiniteKernel η] {κ' : Kernel X' Y'}
    [IsSFiniteKernel κ'] {η' : Kernel Y' Z'} [IsSFiniteKernel η'] : (η ∥ₖ η') ∘ₖ (κ ∥ₖ κ') = (η ∘ₖ κ) ∥ₖ (η' ∘ₖ κ') :=
  by
  rw [← parallelComp_id_left_comp_parallelComp, ← parallelComp_id_right_comp_parallelComp, ← comp_assoc,
    parallelComp_id_left_comp_parallelComp, comp_id]

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