Syntax Definition cpj 4976

Description: Extend class notation with set of projections on a Hilbert space.

Assertion

Ref	Expression
cpj	class Proj

See definition df-pj 5244 for more information.

metamath.org