quasiMeasurePreserving_div_left — Mathlib

English

For a left‑invariant measure μ, the map h ↦ g/h is quasi‑measure‑preserving on G with respect to μ and itself, for any fixed g ∈ G.

Русский

Пусть μ есть левая инвариантная мера; отображение h ↦ g/h сохраняет меру в квази‑смысле относительно μ и μ для любого фиксированного g ∈ G.

LaTeX

$$$\\mathrm{QuasiMeasurePreserving}\\bigl(\\lambda h:G,\\; g/h\\bigr)\\; (\\mu)\\; (\\mu)$$$$

Lean4

@[to_additive]
theorem quasiMeasurePreserving_div_left [IsMulLeftInvariant μ] (g : G) :
    QuasiMeasurePreserving (fun h : G => g / h) μ μ :=
  by
  simp_rw [div_eq_mul_inv]
  exact (measurePreserving_mul_left μ g).quasiMeasurePreserving.comp (quasiMeasurePreserving_inv μ)

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