Structures · Topology

ContinuousMul

Basic hypothesis to talk about a topological monoid or a topological semigroup. A topological monoid over M, for example, is obtained by requiring both the instances Monoid M and ContinuousMul M. Continuity in each argument separately can be stated using SeparatelyContinuousMul α. If one wants only continuity in either the left or right argument, but not both one can use ContinuousConstSMul α α/ContinuousConstSMul αᵐᵒᵖ α.

Defined in

Mathlib.Topology.Algebra.Monoid.Defs

Shape

One type argument · adds continuous_mul