csp - Hilbert Space Explorer

	Hilbert Space Explorer		< Previous Next > Nearby theorems
Mirrors > Home > HSE Home > Th. List > csp		Structured version Visualization version Unicode version

Syntax Definition csp 27779

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

**Assertion**
Ref	Expression
csp

See definition df-hnorm 27825 for more information.

Colors of variables: wff setvar class

W3C validator