:: deftheorem defines equicontinuous ASCOLI2:def 3 :
for S, T being non empty MetrSpace
for F being Subset of (Funcs ( the carrier of S, the carrier of T)) holds
( F is equicontinuous iff for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for f being Function of the carrier of S, the carrier of T st f in F holds
for x1, x2 being Point of S st dist (x1,x2) < d holds
dist ((f . x1),(f . x2)) < e ) ) );