Metamath Proof Explorer


Syntax definition cpadd

Description: Extend class notation with projective subspace sum.

Ref Expression
Assertion cpadd class +𝑃