:: deftheorem defines is_uniformly_convergent_to MESFUN10:def 2 :
for X being set
for F being Functional_Sequence of X,ExtREAL
for f being PartFunc of X,ExtREAL holds
( F is_uniformly_convergent_to f iff ( F is with_the_same_dom & dom (F . 0) = dom f & ( for e being Real st e > 0 holds
ex N being Nat st
for n being Nat
for x being set st n >= N & x in dom (F . 0) holds
|.(((F . n) . x) - (f . x)).| < e ) ) );