inv — Mathlib

English

Inversion in a topological group is a self-homeomorphism of the group.

Русский

Инверсия в топологической группе образует взаимно однозначное непрерывное отображение группы на саму себя.

LaTeX

$$$\\text{Inversion } x \\mapsto x^{-1} : G \\to G \\text{ is a homeomorphism.}$$$

Lean4

/-- Inversion in a topological group as a homeomorphism. -/
@[to_additive /-- Negation in a topological group as a homeomorphism. -/
    ]
protected def inv (G : Type*) [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] : G ≃ₜ G :=
  { Equiv.inv G with
    continuous_toFun := continuous_inv
    continuous_invFun := continuous_inv }

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