star_inv — Mathlib

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]

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