HomeHome Hilbert Space Explorer < Previous   Next >
Related theorems
Unicode version
Syntax Definition c0v 8971
Description: Extend class notation with zero vector in Hilbert space.
Assertion
Ref Expression
c0v class 0h
This syntax is primitive. The first axiom using it is ax-hv0cl 9021.
Colors of variables: wff set class
Copyright terms: Public domain