:: deftheorem defines is_weakly_continuous_on DUALSP07:def 3 :
for X being RealNormSpace
for f being PartFunc of X,REAL
for X0 being Subset of X holds
( f is_weakly_continuous_on X0 iff ( X0 c= dom f & ( for x0 being Point of X st x0 in X0 holds
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 X0 & ( for y being Point of (DualSp X) st y in Y holds
|.(y . (x - x0)).| < d ) holds
|.((f . x) - (f . x0)).| < e ) ) ) ) );