swap_prod — Mathlib

English

The kernel swap operation on the product kernel equals swapping the order of the factors: (κ ×K η) mapped by Prod.swap equals η ×K κ.

Русский

Операция swap на произведении ядер эквивалентна смене порядка факторов: (κ ×K η).map Prod.swap = η ×K κ.

LaTeX

$$$\\displaystyle (\\text{swap }\\beta \\gamma) \\circ_K (\\kappa \\times_K \\eta) = (\\eta \\times_K \\kappa)$$$

Lean4

@[simp]
theorem swap_prod {κ : Kernel α β} [IsSFiniteKernel κ] {η : Kernel α γ} [IsSFiniteKernel η] :
    (swap β γ) ∘ₖ (κ ×ₖ η) = (η ×ₖ κ) := by rw [swap_comp_eq_map, map_prod_swap]

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