Theorems · Inductive type · Lie groups

IsTopologicalAddGroup

(G : Type u) → [TopologicalSpace G] → [AddGroup G] → Prop

A topological (additive) group is a group in which the addition and negation operations are continuous. When you declare an instance that does not already have a UniformSpace instance, you should also provide an instance of UniformSpace and IsUniformAddGroup using IsTopologicalAddGroup.rightUniformSpace and isUniformAddGroup_of_addCommGroup.

Defined in

Mathlib.Topology.Algebra.Group.Defs

Cited by

1,394 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 3 definitions · uses no axioms

Assumes

TopologicalSpaceAddGroup