swap — Mathlib

English

The swap kernel maps (x, y) to the Dirac measure at (y, x) on β × α.

Русский

Ядро swap переводит пару (x, y) в меру Дирака в (y, x) на β × α.

LaTeX

$$$(\text{swap }\alpha \beta)(x,y) = \delta_{(y,x)}$$$

Lean4

/-- The deterministic kernel that maps `(x, y)` to the Dirac measure at `(y, x)`. -/
noncomputable def swap (α β : Type*) [MeasurableSpace α] [MeasurableSpace β] : Kernel (α × β) (β × α) :=
  Kernel.deterministic Prod.swap measurable_swap

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