Metamath Proof Explorer


Syntax definition cpolN

Description: Extend class notation with polarity of projective subspace $m$.

Ref Expression
Assertion cpolN class 𝑃