Theory of topological monoids
In this file we define mixin classes has_continuous_mul
and has_continuous_add
. While in many
applications the underlying type is a monoid (multiplicative or additive), we do not require this in
the definitions.
- continuous_add : continuous (λ (p : M × M), p.fst + p.snd)
Basic hypothesis to talk about a topological additive monoid or a topological additive
semigroup. A topological additive monoid over α
, for example, is obtained by requiring both the
instances add_monoid α
and has_continuous_add α
.
Instances
- has_continuous_add_of_discrete_topology
- topological_add_group.to_has_continuous_add
- add_group_with_zero_nhd.has_continuous_add
- topological_semiring.to_has_continuous_add
- topological_ring.to_has_continuous_add
- normed_top_monoid
- prod.has_continuous_add
- additive.has_continuous_add
- ennreal.has_continuous_add
- continuous_mul : continuous (λ (p : M × M), (p.fst) * p.snd)
Basic hypothesis to talk about a topological monoid or a topological semigroup.
A topological monoid over α
, for example, is obtained by requiring both the instances monoid α
and has_continuous_mul α
.
Given a open neighborhood U
of 0
there is a open neighborhood V
of 0
such that V + V ⊆ U
.
Given a neighborhood U
of 1
there is an open neighborhood V
of 1
such that VV ⊆ U
.