csp - Hilbert Space Explorer

Hilbert Space Explorer

< Previous Next >
Related theorems
Unicode version

Syntax Definition csp 8788

Description: Extend class notation with inner (scalar) product in Hilbert space. In the literature, the inner product of

and

is usually written

but our operation notation allows us to use existing theorems about operations and also eliminates ambiguity with the definition of an ordered pair df-op 2420.

**Assertion**
Ref	Expression
csp

See definition df-hnorm 8832 for more information.

Colors of variables: wff set class