involutiveInv — Mathlib

English

The inverse operation on sets is an involution: applying it twice returns the original set.

Русский

Операция взятия обратного над множествами есть инволютивна: дважды взятое обратное возвращает исходное множество.

LaTeX

$$$ (S^{-1})^{-1} = S $$$

Lean4

@[to_additive (attr := simp)]
instance involutiveInv : InvolutiveInv (Set α) where
  inv := Inv.inv
  inv_inv s := by simp only [← inv_preimage, preimage_preimage, inv_inv, preimage_id']

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