Topological space structure on the opposite monoid and on the units group #
In this file we define TopologicalSpace
structure on Mᵐᵒᵖ
, Mᵃᵒᵖ
, Mˣ
, and AddUnits M
.
This file does not import definitions of a topological monoid and/or a continuous multiplicative
action, so we postpone the proofs of HasContinuousMul Mᵐᵒᵖ
etc till we have these definitions.
Tags #
topological space, opposite monoid, units
Put the same topological space structure on the opposite monoid as on the original space.
Put the same topological space structure on the opposite monoid as on the original space.
AddOpposite.op
as a homeomorphism.
Instances For
MulOpposite.op
as a homeomorphism.
Instances For
The additive units of a monoid are equipped with a topology, via the embedding into
M × M
.
The units of a monoid are equipped with a topology, via the embedding into M × M
.
An auxiliary lemma that can be used to prove that coercion AddUnits M → M
is a
topological embedding. Use AddUnits.embedding_val
or toAddUnits_homeomorph
instead.
An auxiliary lemma that can be used to prove that coercion Mˣ → M
is a topological embedding.
Use Units.embedding_val₀
, Units.embedding_val
, or toUnits_homeomorph
instead.
An auxiliary lemma that can be used to prove that coercion AddUnits M → M
is a
topological embedding. Use AddUnits.embedding_val
or toAddUnits_homeomorph
instead.
An auxiliary lemma that can be used to prove that coercion Mˣ → M
is a topological embedding.
Use Units.embedding_val₀
, Units.embedding_val
, or toUnits_homeomorph
instead.