measurePreserving_div_left — Mathlib

English

For any g ∈ G, the map t ↦ g / t preserves μ; i.e., (g / t) is a μ-measure-preserving transform.

Русский

Для любого g ∈ G отображение t ↦ g / t сохраняет μ; то есть тождество меры выполняется для этой операции.

LaTeX

$$$ \forall E \text{ measurable}, \; \mu((g/t)^{-1}(E)) = \mu(E) $$$

Lean4

@[to_additive]
theorem measurePreserving_div_left (μ : Measure G) [IsInvInvariant μ] [IsMulLeftInvariant μ] (g : G) :
    MeasurePreserving (fun t => g / t) μ μ := by
  simp_rw [div_eq_mul_inv]
  exact (measurePreserving_mul_left μ g).comp (measurePreserving_inv μ)

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