Metamath Proof Explorer


Syntax definition cmv

Description: Extend class notation with vector subtraction in Hilbert space.

Ref Expression
Assertion cmv class