Metamath Proof Explorer


Syntax definition ctms

Description: Extend class notation with the function mapping a metric to the metric space it defines.

Ref Expression
Assertion ctms class toMetSp