# mathlibdocumentation

topology.algebra.constructions

# 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

@[protected, instance]
def mul_opposite.topological_space {M : Type u_1}  :

Put the same topological space structure on the opposite monoid as on the original space.

Equations
@[protected, instance]
def add_opposite.topological_space {M : Type u_1}  :

Put the same topological space structure on the opposite monoid as on the original space.

Equations
@[continuity]
theorem add_opposite.continuous_unop {M : Type u_1}  :
@[continuity]
theorem mul_opposite.continuous_unop {M : Type u_1}  :
@[continuity]
theorem add_opposite.continuous_op {M : Type u_1}  :
@[continuity]
theorem mul_opposite.continuous_op {M : Type u_1}  :
@[simp]
theorem add_opposite.op_homeomorph_apply {M : Type u_1} (ᾰ : M) :
@[simp]
theorem add_opposite.op_homeomorph_symm_apply {M : Type u_1} (ᾰ : Mᵃᵒᵖ) :
@[simp]
theorem mul_opposite.op_homeomorph_apply {M : Type u_1} (ᾰ : M) :
@[simp]
theorem mul_opposite.op_homeomorph_symm_apply {M : Type u_1} (ᾰ : Mᵐᵒᵖ) :
def mul_opposite.op_homeomorph {M : Type u_1}  :

mul_opposite.op as a homeomorphism.

Equations
def add_opposite.op_homeomorph {M : Type u_1}  :

add_opposite.op as a homeomorphism.

Equations
@[protected, instance]
def add_opposite.t2_space {M : Type u_1} [t2_space M] :
@[protected, instance]
def mul_opposite.t2_space {M : Type u_1} [t2_space M] :
@[simp]
theorem mul_opposite.map_op_nhds {M : Type u_1} (x : M) :
@[simp]
theorem add_opposite.map_op_nhds {M : Type u_1} (x : M) :
@[simp]
theorem mul_opposite.map_unop_nhds {M : Type u_1} (x : Mᵐᵒᵖ) :
@[simp]
theorem add_opposite.map_unop_nhds {M : Type u_1} (x : Mᵃᵒᵖ) :
@[simp]
theorem add_opposite.comap_op_nhds {M : Type u_1} (x : Mᵃᵒᵖ) :
@[simp]
theorem mul_opposite.comap_op_nhds {M : Type u_1} (x : Mᵐᵒᵖ) :
@[simp]
theorem add_opposite.comap_unop_nhds {M : Type u_1} (x : M) :
@[simp]
theorem mul_opposite.comap_unop_nhds {M : Type u_1} (x : M) :
@[protected, instance]
def units.topological_space {M : Type u_1} [monoid M] :

The units of a monoid are equipped with a topology, via the embedding into M × M.

Equations
@[protected, instance]

The additive units of a monoid are equipped with a topology, via the embedding into M × M.

Equations
theorem units.inducing_embed_product {M : Type u_1} [monoid M] :
theorem units.embedding_embed_product {M : Type u_1} [monoid M] :
theorem units.continuous_embed_product {M : Type u_1} [monoid M] :