:: On Some Properties of Real {H}ilbert Space, {I}
:: by Hiroshi Yamazaki , Yasumasa Suzuki , Takao Inou\'e and Yasunari Shidama
::
:: Received February 25, 2003
:: Copyright (c) 2003 Association of Mizar Users
:: deftheorem Def1 defines setsum BHSP_6:def 1 :
theorem Th1: :: BHSP_6:1
theorem Th2: :: BHSP_6:2
:: 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
X;
let L be
Functional of
X;
assume A1:
Y is_summable_set_by L
;
func sum_byfunc Y,
L -> Real means :: BHSP_6:def 7
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
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 X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X 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 X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X 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 X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X 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: :: BHSP_6:3
theorem Th4: :: BHSP_6:4
theorem Th5: :: BHSP_6:5
theorem Th6: :: BHSP_6:6
theorem Th7: :: BHSP_6:7
theorem :: BHSP_6:8
theorem :: BHSP_6:9
theorem :: BHSP_6:10