fact: Definition is_SubPsMetricSpace (X : CPsMetricSpace) (P : cms_crr X -> CProp) : is_CPsMetricSpace (Build_SubCSetoid X P) (dsub P) := Build_is_CPsMetricSpace (Build_SubCSetoid X P) (dsub P) ( dsub_com X P) (dsub_nneg X P) (dsub_pos_imp_ap X P) ( dsub_tri_ineq X P).
imports: CoRN.metrics.IR_CPMSpace