English
In a group with an involutive star, the star operation commutes with set inversion: the star of the inverse set equals the inverse of the star of the set.
Русский
В группе с инволютивной звездой операция звезды коммуницирует с взятием инверсии множества: звезда множества-обратного равна обратному звезде множества.
LaTeX
$$$\\\\forall s \\\\subseteq\\\\alpha, \\\\ (s^{-1})^{\\\\star} = (s^{\\\\star})^{-1}.$$$
Lean4
protected theorem star_inv [Group α] [StarMul α] (s : Set α) : s⁻¹⋆ = s⋆⁻¹ :=
by
ext
simp only [mem_star, mem_inv, star_inv]