measurePreserving_swap — Mathlib

English

The product measure is invariant under swapping coordinates: map swap (μ.prod ν) = ν.prod μ.

Русский

Производная по смене координат сохраняет меру: отображение перестановки координат переводит μ × ν в ν × μ.

LaTeX

$$$\\operatorname{map}(\\mathrm{Prod.swap})(\\mu \\prod \\nu) = \\nu \\prod \\mu$$$

Lean4

theorem measurePreserving_swap : MeasurePreserving Prod.swap (μ.prod ν) (ν.prod μ) :=
  ⟨measurable_swap, prod_swap⟩

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