Topological space structure on the opposite monoid and on the units group #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
An auxiliary lemma that can be used to prove that coercion Mˣ → M is a topological embedding.
Use units.coe_embedding₀, units.coe_embedding, or to_units_homeomorph instead.
An auxiliary lemma that can be used to prove that coercion add_units M → M is a
topological embedding. Use add_units.coe_embedding or to_add_units_homeomorph instead.