English
Let α be a type with an involutive inversion (inv(inv(x)) = x). For any finite subset s ⊆ α, the set of inverses of its elements coincides with the finset obtained by applying inversion to every element of s, i.e. the inverse finset s^{-1} has the same elements as {x^{-1} : x ∈ s}. In particular, |s^{-1}| = |s|.
Русский
Пусть α — множества с инволютивной операцией обращения inv: α → α (inv(inv(x)) = x). Для любого конечного подмножества s ⊆ α множество обратимых элементов совпадает с Finset, полученным применением инверсии ко всем элементам s, т.е. s^{-1} имеет те же элементы, что и {x^{-1} : x ∈ s}. В частности, |s^{-1}| = |s|.
LaTeX
$$$\uparrow s^{-1} = (s : \mathrm{Set}\, \alpha)^{-1}$$$
Lean4
@[to_additive (attr := simp, norm_cast)]
theorem coe_inv (s : Finset α) : ↑s⁻¹ = (s : Set α)⁻¹ :=
coe_image.trans Set.image_inv_eq_inv
