to_topologicalGroup — Mathlib

English

An IsUniformGroup structure on α endows α with a topology making multiplication and inversion continuous.

Русский

Структура IsUniformGroup на α придаёт топологическую группу: умножение и обращение непрерывны.

LaTeX

$$$\\text{IsTopologicalGroup}(\\alpha)$$$

Lean4

@[to_additive]
instance (priority := 10) to_topologicalGroup : IsTopologicalGroup α
    where
  continuous_mul := uniformContinuous_mul.continuous
  continuous_inv := uniformContinuous_inv.continuous

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