measurePreserving_inv — Mathlib

English

The inversion map Inv.inv is a measure-preserving map with respect to μ when μ is inv-invariant and Inv.inv is measurable.

Русский

Инверсия сохраняет меру: отображение инверсии инвариантно по μ и измеримо.

LaTeX

$$$\text{MeasurePreserving}(Inv.inv,\mu,\mu)$$$

Lean4

@[to_additive]
theorem measurePreserving_inv (μ : Measure G) [IsInvInvariant μ] : MeasurePreserving Inv.inv μ μ :=
  ⟨measurable_inv, map_inv_eq_self μ⟩

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