comap_swap — Mathlib

English

Swapping coordinates in a product measure corresponds to applying comap and map with the swapped projection: μ.comap Prod.swap = μ.map Prod.swap.

Русский

Перемещая координаты в произведение меры, получаем равенство comap и map после обмена проекции.

LaTeX

$$$\\mu.\\mathrm{comap}\\ \\mathrm{Prod.swap} = \\mu.\\mathrm{map}\\ Prod.swap$$

Lean4

theorem comap_swap (μ : Measure (α × β)) : μ.comap .swap = μ.map .swap :=
  (MeasurableEquiv.prodComm ..).comap_symm

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