:: deftheorem defines weakly_summable_set BHSP_6:def 5 :

for X being RealUnitarySpace

for Y being Subset of X holds

( Y is weakly_summable_set iff ex x being Point of X st

for L being linear-Functional of X st L is Lipschitzian holds

for e being Real st e > 0 holds

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds

|.(L . (x - (setsum Y1))).| < e ) ) );

for X being RealUnitarySpace

for Y being Subset of X holds

( Y is weakly_summable_set iff ex x being Point of X st

for L being linear-Functional of X st L is Lipschitzian holds

for e being Real st e > 0 holds

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds

|.(L . (x - (setsum Y1))).| < e ) ) );