measurePreserving_div_prod — Mathlib

English

The map (x,y) ↦ (xy, x⁻¹) is measure-preserving, i.e., preserves μ×ν.

Русский

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

LaTeX

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

Lean4

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

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