:: deftheorem defines is_equicontinuous_at ASCOLI:def 3 :
for S being non empty MetrSpace
for T being RealNormSpace
for F being Subset of (Funcs ( the carrier of S, the carrier of T))
for x0 being Point of S holds
( F is_equicontinuous_at x0 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 x being Point of S st dist (x,x0) < d holds
||.((f . x) - (f . x0)).|| < e ) ) );