:: deftheorem defines uniformly_continuous FCONT_2:def 1 :
for f being PartFunc of REAL,REAL holds
( f is uniformly_continuous iff for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom f & x2 in dom f & |.(x1 - x2).| < s holds
|.((f . x1) - (f . x2)).| < r ) ) );