:: deftheorem defines uniformly_continuous UNIFORM1:def 1 :
for X, Y being non empty MetrStruct
for f being Function of X,Y holds
( f is uniformly_continuous iff for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for u1, u2 being Element of X st dist (u1,u2) < s holds
dist ((f /. u1),(f /. u2)) < r ) ) );