Metamath Proof Explorer


Syntax definition cmetu

Description: Extend class notation with the function mapping metrics to the uniform structure generated by that metric.

Ref Expression
Assertion cmetu class metUnif