begin
theorem
:: deftheorem Def1 defines non-decreasing INTEGRA2:def 1 :
theorem
theorem
theorem
begin
:: deftheorem Def2 defines ** INTEGRA2:def 2 :
theorem
theorem
theorem Th7:
theorem Th8:
theorem
theorem
theorem
theorem
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
begin
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
begin
theorem Th32:
theorem Th33:
theorem
begin
theorem
theorem
:: deftheorem defines delta INTEGRA2:def 3 :
definition
let A be
closed-interval Subset of ;
let f be
PartFunc of ,;
let T be
DivSequence of
A;
func upper_sum f,
T -> Real_Sequence means
for
i being
Element of
NAT holds
it . i = upper_sum f,
(T . i);
existence
ex b1 being Real_Sequence st
for i being Element of NAT holds b1 . i = upper_sum f,(T . i)
uniqueness
for b1, b2 being Real_Sequence st ( for i being Element of NAT holds b1 . i = upper_sum f,(T . i) ) & ( for i being Element of NAT holds b2 . i = upper_sum f,(T . i) ) holds
b1 = b2
func lower_sum f,
T -> Real_Sequence means
for
i being
Element of
NAT holds
it . i = lower_sum f,
(T . i);
existence
ex b1 being Real_Sequence st
for i being Element of NAT holds b1 . i = lower_sum f,(T . i)
uniqueness
for b1, b2 being Real_Sequence st ( for i being Element of NAT holds b1 . i = lower_sum f,(T . i) ) & ( for i being Element of NAT holds b2 . i = lower_sum f,(T . i) ) holds
b1 = b2
end;
:: deftheorem defines upper_sum INTEGRA2:def 4 :
:: deftheorem defines lower_sum INTEGRA2:def 5 :
theorem Th37:
theorem
canceled;
theorem
canceled;
theorem Th40:
theorem
begin
theorem