We say that two pseudo metric spaces are equivalent, when there exists a
bijective, structure-preserving function between them.
Definition equivalent_psmetric (X : CSetoid) (d0 d1 : CSetoid_bin_fun X X IR)
: CProp :=
(is_CPsMetricSpace X d0 and is_CPsMetricSpace X d1)
and {n : N | forall x y : X, d0 x y[<=]nring (S n)[*]d1 x y}
and {n : N | forall x y : X, d1 x y[<=]nring (S n)[*]d0 x y}.
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).
Lemma isopsmetry_imp_bij :
forall (X Y : CPsMetricSpace) (f : CSetoid_fun X Y),
isopsmetry f -> bijective f.
Lemma isopsmetry_imp_lipschitz :
forall (X Y : CPsMetricSpace) (f : CSetoid_fun X Y),
isopsmetry f -> lipschitz' f.
Lemma id_is_isopsmetry : forall X : CPsMetricSpace, isopsmetry (id_un_op X).
Lemma comp_resp_isopsmetry :
forall (X Y Z : CPsMetricSpace) (f : CSetoid_fun X Y) (g : CSetoid_fun Y Z),
isopsmetry f -> isopsmetry g -> isopsmetry (compose_CSetoid_fun X Y Z f g).
Lemma inv_isopsmetry :
forall (X Y : CPsMetricSpace) (f : CSetoid_fun X Y) (H : isopsmetry f),
isopsmetry (Inv f (isopsmetry_imp_bij X Y f H)).
Definition MSequivalent (X Y : CPsMetricSpace) :=
{f : CSetoid_fun X Y | isopsmetry f}.
Not all pseudo metric spaces are equivalent:
Lemma MSequivalent_discr :
~ (MSequivalent IR_as_CPsMetricSpace (zf_as_CPsMetricSpace IR)).
End equivalent.