proposition: Lemma Quotient_pres_CMetricSpace : forall X : CMetricSpace, isopsmetry X (QuotientCPsMetricSpace X) (Emb X).
proof: Proof. intro X. unfold isopsmetry in |- *. unfold Emb in |- *. simpl in |- *. unfold emb in |- *. split. unfold bijective in |- *. split. unfold injective in |- *. simpl in |- *. intros a0 a1. unfold metric_ap in |- *. apply ax_d_apdiag_imp_grzero. unfold surjective in |- *. intro b. simpl in |- *. exists b. unfold metric_eq in |- *. apply pos_imp_ap_imp_diag_zero. apply d_pos_imp_ap. apply d_nneg. unfold equivalent_psmetric in |- *. simpl in |- *. split. split. apply CPsMetricSpace_is_CPsMetricSpace. apply Build_is_CPsMetricSpace. unfold com in |- *. simpl in |- *. unfold metric_d in |- *. apply ax_d_com. apply CPsMetricSpace_is_CPsMetricSpace. unfold nneg in |- *. simpl in |- *. unfold metric_d in |- *. apply ax_d_nneg. apply CPsMetricSpace_is_CPsMetricSpace. unfold pos_imp_ap in |- *. simpl in |- *. unfold metric_d in |- *. apply ax_d_pos_imp_ap. apply CPsMetricSpace_is_CPsMetricSpace. unfold tri_ineq in |- *. simpl in |- *. unfold metric_d in |- *. apply ax_d_tri_ineq. apply CPsMetricSpace_is_CPsMetricSpace. split. exists 0. unfold metric_d in |- *. intros x y. apply eq_imp_leEq. rational. exists 0. unfold metric_d in |- *. intros x y. apply eq_imp_leEq. rational. Qed.
imports: CoRN.metrics.Prod_Sub CoRN.metrics.Equiv