mathlib documentation

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ᵃᵒᵖ, , 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]

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

Equations
@[continuity]
@[continuity]
@[protected, instance]
@[protected, instance]
@[simp]
@[simp]
@[protected, instance]

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

Equations