proposition: Lemma d_is_uni_continuous : forall a : X, uni_continuous (projected_bin_fun X X IR_as_CPsMetricSpace (cms_d (c:=X)) a).
proof: Proof. intro a. apply lipschitz_imp_uni_continuous. apply d_is_lipschitz. Qed.
imports: CoRN.metrics.ContFunctions