Theory of topological monoids #
In this file we define mixin classes
has_continuous_add. While in many
applications the underlying type is a monoid (multiplicative or additive), we do not require this in
Basic hypothesis to talk about a topological additive monoid or a topological additive
semigroup. A topological additive monoid over
M, for example, is obtained by requiring both the
add_monoid M and
Basic hypothesis to talk about a topological monoid or a topological semigroup.
A topological monoid over
M, for example, is obtained by requiring both the instances
The (topological-space) closure of a submonoid of a space
itself a submonoid.
The units of a monoid are equipped with a topology, via the embedding into
α × α.
If multiplication on a monoid is continuous, then multiplication on the units of the monoid, with respect to the induced topology, is continuous.
Inversion is also continuous, but we register this in a later file,
because the predicate
has_continuous_inv has not yet been defined.