English
Let κ be a kernel α → β × γ. The right-swap construction produces a kernel from α to γ × β by transporting κ(a) along the swap map on the product. Concretely, for each a ∈ α, (swapRight κ)(a) is the image of κ(a) under the swap map Prod.swap : β × γ → γ × β.
Русский
Пусть κ — ядро α → β × γ. Операция swapRight строит ядро из α в γ × β путём переноса κ(a) вдоль отображения перестановки координат Prod.swap: β × γ → γ × β. То есть для каждого a выполняется (swapRight κ)(a) = (κ(a)) map Prod.swap.
LaTeX
$$$$\\forall a,\\; (swapRight \\kappa)(a) = (\\kappa(a)) \\circ \\mathrm{Prod.swap}^{-1}, \\quad \\text{то есть }(swapRight \\kappa)(a)(S) = \\kappa(a)(\\mathrm{Prod.swap}^{-1}(S))\\text{ для всех измеримых }S\\subseteq (\\gamma \\times \\beta).$$$$
Lean4
/-- Define a `Kernel α (γ × β)` from a `Kernel α (β × γ)` by taking the map of `Prod.swap`.
We use `mapOfMeasurable` in the definition for better defeqs. -/
noncomputable def swapRight (κ : Kernel α (β × γ)) : Kernel α (γ × β) :=
mapOfMeasurable κ Prod.swap measurable_swap
