begin
:: deftheorem Def1 defines closed-interval INTEGRA1:def 1 :
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
begin
:: deftheorem Def2 defines Division INTEGRA1:def 2 :
:: deftheorem Def3 defines divs INTEGRA1:def 3 :
theorem
canceled;
theorem Th8:
theorem Th9:
:: deftheorem INTEGRA1:def 4 :
canceled;
:: deftheorem Def5 defines divset INTEGRA1:def 5 :
theorem Th10:
:: deftheorem defines vol INTEGRA1:def 6 :
theorem
begin
definition
let A be
closed-interval Subset of ;
let f be
PartFunc of ,;
let D be
Division of
A;
func upper_volume f,
D -> FinSequence of
REAL means :
Def7:
(
len it = len D & ( for
i being
Nat st
i in dom D holds
it . i = (upper_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) ) );
existence
ex b1 being FinSequence of REAL st
( len b1 = len D & ( for i being Nat st i in dom D holds
b1 . i = (upper_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) ) )
uniqueness
for b1, b2 being FinSequence of REAL st len b1 = len D & ( for i being Nat st i in dom D holds
b1 . i = (upper_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) ) & len b2 = len D & ( for i being Nat st i in dom D holds
b2 . i = (upper_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) ) holds
b1 = b2
func lower_volume f,
D -> FinSequence of
REAL means :
Def8:
(
len it = len D & ( for
i being
Nat st
i in dom D holds
it . i = (lower_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) ) );
existence
ex b1 being FinSequence of REAL st
( len b1 = len D & ( for i being Nat st i in dom D holds
b1 . i = (lower_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) ) )
uniqueness
for b1, b2 being FinSequence of REAL st len b1 = len D & ( for i being Nat st i in dom D holds
b1 . i = (lower_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) ) & len b2 = len D & ( for i being Nat st i in dom D holds
b2 . i = (lower_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) ) holds
b1 = b2
end;
:: deftheorem Def7 defines upper_volume INTEGRA1:def 7 :
:: deftheorem Def8 defines lower_volume INTEGRA1:def 8 :
:: deftheorem defines upper_sum INTEGRA1:def 9 :
:: deftheorem defines lower_sum INTEGRA1:def 10 :
definition
let A be
closed-interval Subset of ;
let f be
PartFunc of ,;
set S =
divs A;
func upper_sum_set f -> PartFunc of ,
means :
Def11:
(
dom it = divs A & ( for
D being
Division of
A st
D in dom it holds
it . D = upper_sum f,
D ) );
existence
ex b1 being PartFunc of , st
( dom b1 = divs A & ( for D being Division of A st D in dom b1 holds
b1 . D = upper_sum f,D ) )
uniqueness
for b1, b2 being PartFunc of , st dom b1 = divs A & ( for D being Division of A st D in dom b1 holds
b1 . D = upper_sum f,D ) & dom b2 = divs A & ( for D being Division of A st D in dom b2 holds
b2 . D = upper_sum f,D ) holds
b1 = b2
func lower_sum_set f -> PartFunc of ,
means :
Def12:
(
dom it = divs A & ( for
D being
Division of
A st
D in dom it holds
it . D = lower_sum f,
D ) );
existence
ex b1 being PartFunc of , st
( dom b1 = divs A & ( for D being Division of A st D in dom b1 holds
b1 . D = lower_sum f,D ) )
uniqueness
for b1, b2 being PartFunc of , st dom b1 = divs A & ( for D being Division of A st D in dom b1 holds
b1 . D = lower_sum f,D ) & dom b2 = divs A & ( for D being Division of A st D in dom b2 holds
b2 . D = lower_sum f,D ) holds
b1 = b2
end;
:: deftheorem Def11 defines upper_sum_set INTEGRA1:def 11 :
:: deftheorem Def12 defines lower_sum_set INTEGRA1:def 12 :
:: deftheorem Def13 defines upper_integrable INTEGRA1:def 13 :
:: deftheorem Def14 defines lower_integrable INTEGRA1:def 14 :
:: deftheorem defines upper_integral INTEGRA1:def 15 :
:: deftheorem defines lower_integral INTEGRA1:def 16 :
:: deftheorem Def17 defines integrable INTEGRA1:def 17 :
:: deftheorem defines integral INTEGRA1:def 18 :
begin
theorem Th12:
theorem Th13:
theorem
theorem Th15:
theorem
theorem
begin
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem
theorem Th24:
theorem Th25:
theorem Th26:
begin
theorem Th27:
theorem
theorem Th29:
theorem Th30:
:: deftheorem defines delta INTEGRA1:def 19 :
:: deftheorem Def20 defines <= INTEGRA1:def 20 :
theorem
theorem Th32:
theorem Th33:
theorem
theorem Th35:
:: deftheorem Def21 defines indx INTEGRA1:def 21 :
theorem Th36:
theorem Th37:
theorem Th38:
for
i,
j being
Element of
NAT for
A being
closed-interval Subset of
for
D being
Division of
A st
i in dom D &
j in dom D &
i <= j holds
ex
B being
closed-interval Subset of st
(
lower_bound B = (mid D,i,j) . 1 &
upper_bound B = (mid D,i,j) . (len (mid D,i,j)) &
len (mid D,i,j) = (j - i) + 1 &
mid D,
i,
j is
Division of
B )
theorem Th39:
:: deftheorem Def22 defines PartSums INTEGRA1:def 22 :
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
begin
theorem Th51:
theorem Th52:
theorem Th53:
theorem Th54:
theorem Th55:
theorem Th56:
theorem Th57:
theorem Th58:
theorem