19.2. Continuous Linear Maps🔗

If F is another TVS:

variable (F : Type*) [AddCommGroup F] [Module 𝕜 F]
  [TopologicalSpace F]
  [ContinuousAdd F] [ContinuousSMul 𝕜 F]

we can speak of the continuous linear maps between E and F. The relevant definition is ContinuousLinearMap and it has special notation as follows:

E →L[𝕜] F : Type (max u_1 u_3)#check E →L[𝕜] F