Structures · Topology

ContinuousAdd

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

Defined in

Mathlib.Topology.Algebra.Monoid.Defs

Shape

One type argument · adds continuous_add