Topological space structure on the opposite monoid and on the units group #
In this file we define topological_space
structure on Mᵐᵒᵖ
, Mᵃᵒᵖ
, Mˣ
, and add_units M
.
This file does not import definitions of a topological monoid and/or a continuous multiplicative
action, so we postpone the proofs of has_continuous_mul 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.
Equations
Put the same topological space structure on the opposite monoid as on the original space.
Equations
mul_opposite.op
as a homeomorphism.
Equations
- mul_opposite.op_homeomorph = {to_equiv := mul_opposite.op_equiv M, continuous_to_fun := _, continuous_inv_fun := _}
add_opposite.op
as a homeomorphism.
Equations
- add_opposite.op_homeomorph = {to_equiv := add_opposite.op_equiv M, continuous_to_fun := _, continuous_inv_fun := _}
The units of a monoid are equipped with a topology, via the embedding into M × M
.
The additive units of a monoid are equipped with a topology, via the embedding into
M × M
.