Metamath Proof Explorer


Syntax definition cnsb

Description: Extend class notation with vector subtraction in a normed complex vector space.

Ref Expression
Assertion cnsb class 𝑣