Theorems · Inductive type · Lie groups

IsTopologicalGroup

(G : Type u_4) → [TopologicalSpace G] → [Group G] → Prop

A topological group is a group in which the multiplication and inversion 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 IsUniformGroup using IsTopologicalGroup.rightUniformSpace and isUniformGroup_of_commGroup.

Defined in

Mathlib.Topology.Algebra.Group.Defs

Cited by

469 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceGroup