swap_comp_eq_map — Mathlib

English

For a kernel κ: α → β×γ, swapping yields κ mapped by Prod.swap: (swap β γ) ∘ₖ κ = κ.map Prod.swap.

Русский

Свапирование β и γ эквивалентно отображению ядра κ через Prod.swap: (swap β γ) ∘ₖ κ = κ.map Prod.swap.

LaTeX

$$$ (\text{swap } β γ) \circ_K κ = κ.map Prod.swap $$$

Lean4

theorem swap_comp_eq_map {κ : Kernel α (β × γ)} : (swap β γ) ∘ₖ κ = κ.map Prod.swap := by
  rw [swap, deterministic_comp_eq_map]

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