measurePreserving_prod_div_swap — Mathlib

English

The map (x,y) ↦ (x y, y) preserves μ×ν, i.e., MeasurePreserving (fun z : G × G => (z.1 * z.2, z.2)) (μ.prod ν) (μ.prod ν).

Русский

Отображение (x,y) ↦ (xy,y) сохраняет меру μ×ν.

LaTeX

$$$\text{MeasurePreserving}(\lambda z. (z.1 * z.2, z.2),\ (\mu \prod ν), (\mu \prod ν))$$$

Lean4

/-- The map `(x, y) ↦ (y, x / y)` sends `μ × ν` to `ν × μ`. -/
@[to_additive measurePreserving_prod_sub_swap /-- The map `(x, y) ↦ (y, x - y)` sends `μ × ν` to `ν × μ`. -/
    ]
theorem measurePreserving_prod_div_swap [IsMulRightInvariant μ] :
    MeasurePreserving (fun z : G × G => (z.2, z.1 / z.2)) (μ.prod ν) (ν.prod μ) :=
  (measurePreserving_prod_div ν μ).comp measurePreserving_swap

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