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