:: deftheorem defines is_equicontinuous_at ASCOLI2:def 2 :
for S, T being non empty MetrSpace
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
dist ((f . x),(f . x0)) < e ) ) );