:: deftheorem defines is_weakly*_continuous_in DUALSP07:def 4 :
for X being RealNormSpace
for f being PartFunc of (DualSp X),REAL
for x0 being Point of (DualSp 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 X st
( 0 < d & Y is finite & Y <> {} & ( for x being Point of (DualSp X) st x in dom f & ( for y being Point of X st y in Y holds
|.((x - x0) . y).| < d ) holds
|.((f . x) - (f . x0)).| < e ) ) ) ) );