begin
:: deftheorem Def1 defines setsum BHSP_6:def 1 :
theorem Th1:
theorem Th2:
begin
:: deftheorem Def2 defines summable_set BHSP_6:def 2 :
:: deftheorem defines sum BHSP_6:def 3 :
:: deftheorem Def4 defines Bounded BHSP_6:def 4 :
:: deftheorem Def5 defines weakly_summable_set BHSP_6:def 5 :
:: deftheorem Def6 defines is_summable_set_by BHSP_6:def 6 :
definition
let X be
RealUnitarySpace;
let Y be
Subset of ;
let L be
Functional of
X;
assume A1:
Y is_summable_set_by L
;
func sum_byfunc Y,
L -> Real means
for
e being
Real st
e > 0 holds
ex
Y0 being
finite Subset of st
( not
Y0 is
empty &
Y0 c= Y & ( for
Y1 being
finite Subset of st
Y0 c= Y1 &
Y1 c= Y holds
abs (it - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e ) );
existence
ex b1 being Real st
for e being Real st e > 0 holds
ex Y0 being finite Subset of st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of st Y0 c= Y1 & Y1 c= Y holds
abs (b1 - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e ) )
by A1, Def6;
uniqueness
for b1, b2 being Real st ( for e being Real st e > 0 holds
ex Y0 being finite Subset of st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of st Y0 c= Y1 & Y1 c= Y holds
abs (b1 - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e ) ) ) & ( for e being Real st e > 0 holds
ex Y0 being finite Subset of st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of st Y0 c= Y1 & Y1 c= Y holds
abs (b2 - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e ) ) ) holds
b1 = b2
end;
:: deftheorem defines sum_byfunc BHSP_6:def 7 :
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem
theorem
begin
theorem