:: deftheorem defines is_weakly_continuous_in DUALSP07:def 2 :
for X being RealNormSpace
for f being PartFunc of X,REAL
for x0 being Point of X holds
( f is_weakly_continuous_in x0 iff ( x0 in dom f & ( for e being Real st 0 < e holds
ex d being Real ex Y being Subset of (DualSp X) st
( 0 < d & Y is finite & Y <> {} & ( for x being Point of X st x in dom f & ( for y being Point of (DualSp X) st y in Y holds
|.(y . (x - x0)).| < d ) holds
|.((f . x) - (f . x0)).| < e ) ) ) ) );