Metamath Proof Explorer


Syntax definition ccpms

Description: Completion of a metric space.

Ref Expression
Assertion ccpms class cplMetSp