swapRight_apply

Mathlib.Probability.Kernel.Composition.MapComap

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

English

For any κ and a, the value of swapRight κ at a is the κ-value at a mapped by the swap: (swapRight κ)(a) = (κ(a)).map Prod.swap.

Русский

Для любых κ и a: (swapRight κ)(a) = (κ(a)).map Prod.swap.

LaTeX

$$$$swapRight \\kappa a = (\\kappa a) \\;.\\mathrm{map} \\; Prod.swap$$$$

Lean4

theorem swapRight_apply (κ : Kernel α (β × γ)) (a : α) : swapRight κ a = (κ a).map Prod.swap :=
  rfl

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

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

Разделы

Аффилиация

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