instIsTopologicalAddGroupAdditiveOfIsTopologicalGroup

English

If G is a group with a topology and is a topological group, then the additive structure on G makes Additive G into a topological additive group; equivalently, the negation map x ↦ −x is continuous.

Русский

Если G — группа с топологией, и она является топологической группой, то аддитивная структура G образует топологическую аддитивную группу; эквивалентно тому, что отображение x ↦ −x непрерывно.

LaTeX

$$$ IsTopologicalAddGroup (Additive\U0001D400 G) $$$

Lean4

instance {G} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : IsTopologicalAddGroup (Additive G) where
  continuous_neg := @continuous_inv G _ _ _

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