measurePreserving_mul_left — Mathlib

English

If μ is invariant under right multiplication, then the map x ↦ x g is measure-preserving for any g ∈ G.

Русский

Если μ инвариантна справа, то отображение x ↦ x g сохраняет меру для любого g.

LaTeX

$$$\\text{MeasurePreserving}(x \\mapsto x g) \\mu \\mu$$$

Lean4

@[to_additive]
theorem measurePreserving_mul_left (μ : Measure G) [IsMulLeftInvariant μ] (g : G) : MeasurePreserving (g * ·) μ μ :=
  ⟨measurable_const_mul g, map_mul_left_eq_self μ g⟩

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