Metamath Proof Explorer

Syntax definition chcmp

Description: Extend class notation with the Hausdorff uniform completion relation.

Ref Expression
Assertion chcmp 
class HCmp