Syntax Definition cva 4959

Description: Extend class notation with vector addition on Hilbert space. In the literature, the subscript "v" is omitted, but we need it to avoid ambiguity with complex number addition + caddc 4031.

Assertion

Ref	Expression
cva	class +v

This syntax is primitive. The first axiom using it is ax-hvaddcl 4984.

metamath.org