topologicalAddGroup — Mathlib

English

If C is an AddCommGroup with an R-module structure and the module topology, then C is a topological additive group; addition and negation are continuous.

Русский

Если C является аддитивной коммутативной группой с структурой R-модуля и модульной топологией, то C — топологическая аддитивная группа; сложение и отрицание непрерывны.

LaTeX

$$$IsTopologicalAddGroup(C).$$$

Lean4

theorem topologicalAddGroup (C : Type*) [AddCommGroup C] [Module R C] [TopologicalSpace C] [IsModuleTopology R C] :
    IsTopologicalAddGroup C
    where
  continuous_add := (IsModuleTopology.toContinuousAdd R C).1
  continuous_neg := continuous_neg R C

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