Metamath Proof Explorer


Syntax definition chlo

Description: Extend class notation with the class of all complex Hilbert spaces.

Ref Expression
Assertion chlo class CHilOLD