English
Let G be a group with a left‑invariant measure ν. The map ψ: G × G → G given by ψ(x,y) = y^{-1} x is quasi‑measure‑preserving with respect to μ × ν and μ.
Русский
Пусть G — группа с левоинвариантной мерой ν. Отображение ψ: G × G → G, ψ(x,y) = y^{-1} x, является квази‑сохранением меры относительно μ × ν и μ.
LaTeX
$$$\\mathrm{QuasiMeasurePreserving}\\left(\\lambda p:(G \\times G). p_{2}^{-1} p_{1}\\right) \\, (\\mu \\times \\nu) \\, \\mu$$$
Lean4
/-- The map `(x, y) ↦ y⁻¹ * x` is quasi-measure-preserving. -/
@[to_additive (attr := fun_prop) /-- The map `(x, y) ↦ -y + x` is quasi-measure-preserving. -/
]
theorem quasiMeasurePreserving_inv_mul_swap [IsMulLeftInvariant μ] :
QuasiMeasurePreserving (fun p ↦ p.2⁻¹ * p.1) (μ.prod ν) μ :=
quasiMeasurePreserving_snd.comp (measurePreserving_prod_inv_mul_swap _ _).quasiMeasurePreserving
