:: deftheorem defines uniformly_continuous INTEGR20:def 1 :
for X being RealNormSpace
for f being PartFunc of REAL, the carrier of X 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 ) ) );