Metamath Proof Explorer


Syntax definition cipf

Description: Extend class notation with inner product function.

Ref Expression
Assertion cipf class if