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