A topological semimodule, over a semiring which is also a topological space, is a semimodule in which scalar multiplication is continuous. In applications, α will be a topological semiring and β a topological additive semigroup, but this is not needed for the definition

A topological module, over a ring which is also a topological space, is a module in which scalar multiplication is continuous. In applications, α will be a topological ring and β a topological additive group, but this is not needed for the definition

A topological vector space is a topological module over a field.

Continuous linear maps between modules. We only put the type classes that are necessary for the definition, although in applications β and γ will be topological modules over the topological ring α

Coerce continuous linear maps to linear maps.

Coerce continuous linear maps to functions.

The continuous map that is constantly zero.

the identity map as a continuous linear map.

Composition of bounded linear maps.

The cartesian product of two bounded linear maps, as a bounded linear map.

Associating to a scalar-valued linear map and an element of γ the γ-valued linear map obtained by multiplying the two (a.k.a. tensoring by γ)