:: deftheorem defines equicontinuous ASCOLI:def 4 :
for S being non empty MetrSpace
for T being RealNormSpace
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
||.((f . x1) - (f . x2)).|| < e ) ) );