inv_inv — Mathlib

English

Let G be a group with a measurable inversion map x ↦ x⁻¹. For any measure μ on G, applying inversion twice yields the original measure: μ.inv.inv = μ.

Русский

Пусть G — группа с измеримой операцией обращения x ↔ x⁻¹. Для любой меры μ на G применение обращения дважды возвращает исходную меру: μ.inv.inv = μ.

LaTeX

$$$ (\mu^{\mathrm{inv}})^{\mathrm{inv}} = \mu $$$

Lean4

@[to_additive (attr := simp)]
protected theorem inv_inv (μ : Measure G) : μ.inv.inv = μ :=
  (MeasurableEquiv.inv G).map_symm_map

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