Theorems · Inductive type · Lie groups

ContinuousAdd

(M : Type u_1) → [TopologicalSpace M] → [Add M] → Prop

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

Cited by

777 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 3 definitions · uses no axioms

Assumes

TopologicalSpaceAdd