quasiMeasurePreserving_inv_of_right_invariant

English

If μ is right‑invariant under multiplication, then the inverse map inv: G → G is quasi‑measure‑preserving with respect to μ.

Русский

Если мера μ правосторонне инвариантна относительно умножения, то отображение обратного элемента inv: G → G сохраняет меру в квази‑смысле относительно μ.

LaTeX

$$$\\mathrm{QuasiMeasurePreserving}(\\mathrm{Inv.inv}:G\\to G)\\; \\mu\\; \\mu$$$

Lean4

@[to_additive (attr := fun_prop)]
theorem quasiMeasurePreserving_inv_of_right_invariant [IsMulRightInvariant μ] :
    QuasiMeasurePreserving (Inv.inv : G → G) μ μ :=
  by
  rw [← μ.inv_inv]
  exact (quasiMeasurePreserving_inv μ.inv).mono (inv_absolutelyContinuous μ.inv) (absolutelyContinuous_inv μ.inv)

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