Metamath Proof Explorer


Syntax definition ccphlo

Description: Extend class notation with the class of all complex inner product spaces (also called pre-Hilbert spaces).

Ref Expression
Assertion ccphlo class CPreHil OLD