Metamath Proof Explorer


Syntax definition cdip

Description: Extend class notation with the class inner product functions.

Ref Expression
Assertion cdip class ·𝑖OLD