map_mul_right_inv_eq_self — Mathlib

English

The pushforward of μ by t ↦ (g * t)⁻¹ equals μ; i.e., map (fun t => (g * t)⁻¹) μ = μ.

Русский

Образ μ по отображению t ↦ (g · t)⁻¹ равен μ; то есть map (t ↦ (g · t)⁻¹) μ = μ.

LaTeX

$$$ \mathrm{map}\left( t \mapsto (g t)^{-1} \right) \mu = \mu $$$

Lean4

@[to_additive]
theorem map_mul_right_inv_eq_self (μ : Measure G) [IsInvInvariant μ] [IsMulLeftInvariant μ] (g : G) :
    map (fun t => (g * t)⁻¹) μ = μ :=
  (measurePreserving_mul_right_inv μ g).map_eq

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