measurePreserving_mul_right_inv — Mathlib

English

The map t ↦ (g * t)⁻¹ preserves μ; i.e., μ is preserved under this composition of left multiplication and inversion.

Русский

Отображение t ↦ (g · t)⁻¹ сохраняет μ; то есть эта композиция преобразований сохраняет меру.

LaTeX

$$$ \text{MeasurePreserving}\left(t \mapsto (g \cdot t)^{-1}\right)\, \mu \ \mu $$$

Lean4

@[to_additive]
theorem measurePreserving_mul_right_inv (μ : Measure G) [IsInvInvariant μ] [IsMulLeftInvariant μ] (g : G) :
    MeasurePreserving (fun t => (g * t)⁻¹) μ μ :=
  (measurePreserving_inv μ).comp <| measurePreserving_mul_left μ g

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