cno - Hilbert Space Explorer

Hilbert Space Explorer

< Previous Next >
Related theorems
Unicode version

Syntax Definition cno 8789

Description: Extend class notation with the norm function in Hilbert 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
cno

See definition df-hnorm 8832 for more information.

Colors of variables: wff set class