cnm - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Syntax Definition cnm 8147

Description: Extend class notation with the norm function in a normed complex vector space. In the literature, the norm of

is usually written "||

||", but we use function notation to take advantage of our existing theorems about functions.

**Assertion**
Ref	Expression
cnm

See definition df-nm 8157 for more information.

Colors of variables: wff set class