proposition: Lemma uni_continuous_imp_continuous : forall (C D : CPsMetricSpace) (f : CSetoid_fun C D), uni_continuous f -> continuous f.
proof: Proof. intros C D F. red in |- *. unfold uni_continuous in |- *. intros H0 n u H3. elim H0 with u H3. intros. exists x. intro y. apply p. Qed.
imports: CoRN.metrics.CPseudoMSpaces