measurePreserving_mul_prod — Mathlib

English

The map (x,y) ↦ (y, x/y) preserves the product measure μ×ν, mapping to ν×μ.

Русский

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

LaTeX

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

Lean4

/-- The map `(x, y) ↦ (xy, y)` preserves the measure `μ × ν`. -/
@[to_additive measurePreserving_add_prod /-- The map `(x, y) ↦ (x + y, y)` preserves the measure `μ × ν`. -/
    ]
theorem measurePreserving_mul_prod [IsMulRightInvariant μ] :
    MeasurePreserving (fun z : G × G => (z.1 * z.2, z.2)) (μ.prod ν) (μ.prod ν) :=
  measurePreserving_swap.comp (measurePreserving_prod_mul_swap_right μ ν)

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