:: deftheorem defines uniformly_continuous UNIFORM3:def 18 :
for US1, US2 being UniformSpaceStr
for f being Function of US1,US2 holds
( f is uniformly_continuous iff for V being Element of the entourages of US2 ex U being Element of the entourages of US1 st
for x, y being object st [x,y] in U holds
[(f . x),(f . y)] in V );