inv_smul_ae_eq_self — Mathlib

English

If x moves s to itself a.e., then its inverse also moves s to itself a.e.

Русский

Если x переводит s в себя почти всюду, то и x^{-1} переводит s в себя почти всюду.

LaTeX

$$$(x\cdot s =^{\mu} s) \Rightarrow (x^{-1}\cdot s =^{\mu} s)$$$

Lean4

@[to_additive]
theorem inv_smul_ae_eq_self (hs : (x • s : Set α) =ᵐ[μ] s) : (x⁻¹ • s : Set α) =ᵐ[μ] s :=
  inv_mem (s := MulAction.aestabilizer G μ s) hs

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