swap_apply

Mathlib.Probability.Kernel.Basic

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

← MathLib Explorer

English

For any (a,b), swap(a,b) is the Dirac measure at (b,a).

Русский

Для любых (a,b) перестановка применяется как мера Дирака в (b,a).

LaTeX

$$$(\text{swap }\alpha \beta)(a,b) = \delta_{(b,a)}$$$

Lean4

/-- See `swap_apply'` for a fully applied version of this lemma. -/
theorem swap_apply (ab : α × β) : swap α β ab = Measure.dirac ab.swap := by rw [swap, deterministic_apply]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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