Metamath Proof Explorer


Syntax definition c0o

Description: Extend class notation with the class of zero operators on normed complex vector spaces.

Ref Expression
Assertion c0o class 0 op