coe_inv — Mathlib

English

The underlying function of the inversion homeomorphism is the inversion map.

Русский

Фонковая функция гомеоморфа инверсии совпадает с отображением инверсии.

LaTeX

$$$(\\\\mathrm{Homeomorph.inv} G)(x) = x^{-1} \\quad \\text{для всех } x \\in G.$$$

Lean4

@[to_additive (attr := simp)]
theorem coe_inv {G : Type*} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] : ⇑(Homeomorph.inv G) = Inv.inv :=
  rfl

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