swapRight_eq

Mathlib.Probability.Kernel.Composition.MapComap

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.Kernel.swapRight_eq

English

The right-swap operation is given by simply pushing κ forward along the swap map; i.e., swapRight κ = map κ Prod.swap.

Русский

Операция swapRight задаётся как сдвиг ядра κ вдоль перестановки; то есть swapRight κ = map κ Prod.swap.

LaTeX

$$$$swapRight \\kappa = map \\kappa Prod.swap$$$$

Lean4

theorem swapRight_eq (κ : Kernel α (β × γ)) : swapRight κ = map κ Prod.swap := by simp [swapRight]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru