Metamath Proof Explorer


Syntax definition cba

Description: Extend class notation with the base set of a normed complex vector space. (Note that BaseSet is capitalized because, once it is fixed for a particular vector space U , it is not a function, unlike e.g., normCV . This is our typical convention.) (New usage is discouraged.)

Ref Expression
Assertion cba class BaseSet