csp - Hilbert Space Explorer

Hilbert Space Explorer

< Previous Next >
Related theorems
Unicode version

Syntax Definition csp 8973

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 2387.

**Assertion**
Ref	Expression
csp

This syntax is primitive. The first axiom using it is ax-hfi 9095.

Colors of variables: wff set class