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