English
A.e. stabilizer of a set under a group action is the set of g ∈ G that move s to itself almost everywhere.
Русский
A.e. стабилизатор множества при группе — это множество элементов g, переводящих s в себя почти всюду.
LaTeX
$$$\mathrm{aestabilizer}(G,\mu,s) = \{ g\in G : g\cdot s =^{\mu} s \}$$$
Lean4
/-- A.e. stabilizer of a set under a group action. -/
@[to_additive (attr := simps) /-- A.e. stabilizer of a set under an additive group action. -/
]
def aestabilizer (s : Set α) : Subgroup G
where
carrier := {g | g • s =ᵐ[μ] s}
one_mem' := by
simp
-- TODO: `calc` would be more readable but fails because of defeq abuse
mul_mem' {g₁ g₂} h₁ h₂ := by simpa only [smul_smul] using ((smul_set_ae_eq g₁).2 h₂).trans h₁
inv_mem' {g} h := by simpa using (smul_set_ae_eq g⁻¹).2 h.out.symm
