Metamath Proof Explorer


Syntax definition cmet

Description: Extend class notation with the class of all metrics.

Ref Expression
Assertion cmet
class Met