Metamath Proof Explorer


Syntax definition cch

Description: Extend class notation with set of closed subspaces of a Hilbert space.

Ref Expression
Assertion cch class C