involutiveInv — Mathlib

English

Inversion is an involution on submonoids: (S⁻¹)⁻¹ = S and the map S ↦ S⁻¹ is compatible with set-coercions.

Русский

Обратная операция на подмономидах является инволюцией: (S⁻¹)⁻¹ = S и отображение S ↦ S⁻¹ согласуется с отображением множеств.

LaTeX

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

Lean4

/-- Inversion is involutive on submonoids. -/
@[to_additive /-- Inversion is involutive on additive submonoids. -/
    ]
def involutiveInv : InvolutiveInv (Submonoid G) :=
  SetLike.coe_injective.involutiveInv _ fun _ => rfl

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