fact: Definition uni_continuous'' (f : CSetoid_fun A B) : CProp := {mds : nat -> nat | forall (n : nat) (x y : A), x[-d]y[<=]one_div_succ (mds n) -> f x[-d]f y[<=]one_div_succ n}.
imports: CoRN.metrics.CPseudoMSpaces