instInvolutiveInv — Mathlib

English

If G has an involutive inversion, then Germ l G inherits an involutive inversion; inv on germs is defined by applying inv to representatives.

Русский

Если у G есть инволютивная операция обращения, то Germ l G наследует такую же инволюцию; операция обращения на гермах задаётся через обращение в G.

LaTeX

$$$ \\operatorname{inv}_{\\mathrm{Germ}}(\\operatorname{inv}_{\\mathrm{Germ}}(q)) = q \\quad\\text{для всех } q \\in \\mathrm{Germ}(l,G). $$$

Lean4

@[to_additive]
instance instInvolutiveInv [InvolutiveInv G] : InvolutiveInv (Germ l G) :=
  { inv_inv := Quotient.ind' fun _ => congrArg ofFun <| inv_inv _ }

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