Syntax Definition chil 4958

Description: Extend class notation with Hilbert vector space.

Assertion

Ref	Expression
chil	class H~

This syntax is primitive. The first axiom using it is ax-hilex 4983.

metamath.org