Metamath Proof Explorer


Syntax definition ccp

Description: Metric completion of _Qp .

Ref Expression
Assertion ccp class p