star_inv' — Mathlib

English

In a group with zero and a StarMul operation, the same inverse-star relation holds for sets: 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' [GroupWithZero α] [StarMul α] (s : Set α) : s⁻¹⋆ = s⋆⁻¹ :=
  by
  ext
  simp only [mem_star, mem_inv, star_inv₀]

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