inv_eq_self — Mathlib

English

For a measure μ on a set with a group operation, if μ is invariant under inversion (i.e., μ.inv = μ), then μ is unchanged by inversion.

Русский

Для меры μ на группе, если μ инвариантна относительно инверсии, то μ не меняется при инверсии.

LaTeX

$$$ μ.inv = μ $$$

Lean4

@[to_additive (attr := simp)]
theorem inv_eq_self (μ : Measure G) [IsInvInvariant μ] : μ.inv = μ :=
  IsInvInvariant.inv_eq_self

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