continuous_inv' — Mathlib

English

The inversion map x ↦ x^{-1} is continuous.

Русский

Отображение $x \\mapsto x^{-1}$ непрерывно.

LaTeX

$$$\\mathrm{ContinuousInv}(\\mathrm{Inv.inv})$$$

Lean4

/-- A version of the global `continuous_inv` suitable for dot notation. -/
@[to_additive /-- A version of the global `continuous_neg` suitable for dot notation. -/
    ]
theorem continuous_inv' (g : GroupTopology α) :
    haveI := g.toTopologicalSpace
    Continuous (Inv.inv : α → α) :=
  by
  letI := g.toTopologicalSpace
  haveI := g.toIsTopologicalGroup
  exact continuous_inv

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