fact: Definition uni_continuous (f : CSetoid_fun A B) : CProp := forall (n : nat) (H : Two[#][0]), {m : nat | forall x y : A, x[-d]y[<]([1][/] Two:IR[//]H)[^]m -> f x[-d]f y[<]([1][/] Two:IR[//]H)[^]n}.
imports: CoRN.metrics.CPseudoMSpaces