English
Let κ, κ′ be finite kernels between appropriate measurable spaces X→Y and X′→Y′, and let η, η′ be finite kernels Y→Z and Y′→Z′. Then the kernel obtained by taking the parallel composition of η and η′ and then composing with the product kernel κ×κ′ equals the product of the composed kernels: (η ∥ₖ η′) ∘ₖ (κ ×ₖ κ′) = (η ∘ₖ κ) ×ₖ (η′ ∘ₖ κ′).
Русский
Пусть κ и κ′ — конечные ядра между подходящими измеримыми пространствами X→Y и X′→Y′, а η и η′ — конечные ядра Y→Z и Y′→Z′. Тогда ядро, полученное как параллельная композиция η и η′ с последующей композиции с произведением κ×κ′, равно произведению композиций η∘κ и η′∘κ′: (η ∥ₖ η′) ∘ₖ (κ ×ₖ κ′) = (η ∘ₖ κ) ×ₖ (η′ ∘ₖ κ′).
LaTeX
$$$$(\\eta \\parallel_k \\eta') \\circ_k (\\kappa \\times_k \\kappa') \;=\\; (\\eta \\circ_k \\kappa) \\times_k (\\eta' \\circ_k \\kappa').$$$$
Lean4
theorem parallelComp_comp_prod [IsSFiniteKernel κ] {η : Kernel Y Z} [IsSFiniteKernel η] {κ' : Kernel X Y'}
[IsSFiniteKernel κ'] {η' : Kernel Y' Z'} [IsSFiniteKernel η'] : (η ∥ₖ η') ∘ₖ (κ ×ₖ κ') = (η ∘ₖ κ) ×ₖ (η' ∘ₖ κ') :=
by rw [← parallelComp_comp_copy, ← comp_assoc, parallelComp_comp_parallelComp, ← parallelComp_comp_copy]
