Metamath Proof Explorer


Syntax definition cds

Description: Extend class notation with the metric space distance function.

Ref Expression
Assertion cds
class dist