fact: Definition isopsmetry (X Y : CPsMetricSpace) (f : CSetoid_fun X Y) := bijective f and equivalent_psmetric X (cms_d (c:=X)) (compose_CSetoid_bin_un_fun X Y IR (cms_d (c:=Y)) f).
imports: CoRN.metrics.IR_CPMSpace