:: The Definition of Riemann Definite Integral and some Related Lemmas
:: by Noboru Endou and Artur Korni{\l}owicz
::
:: Received March 13, 1999
:: Copyright (c) 1999 Association of Mizar Users
:: deftheorem Def1 defines closed-interval INTEGRA1:def 1 :
theorem Th1: :: INTEGRA1:1
theorem Th2: :: INTEGRA1:2
theorem Th3: :: INTEGRA1:3
theorem Th4: :: INTEGRA1:4
theorem Th5: :: INTEGRA1:5
theorem Th6: :: INTEGRA1:6
:: deftheorem Def2 defines DivisionPoint INTEGRA1:def 2 :
:: deftheorem Def3 defines divs INTEGRA1:def 3 :
:: deftheorem Def4 defines Division INTEGRA1:def 4 :
theorem :: INTEGRA1:7
canceled;
theorem Th8: :: INTEGRA1:8
theorem Th9: :: INTEGRA1:9
:: deftheorem Def5 defines divset INTEGRA1:def 5 :
theorem Th10: :: INTEGRA1:10
:: deftheorem defines vol INTEGRA1:def 6 :
theorem :: INTEGRA1:11
definition
let A be
closed-interval Subset of
REAL ;
let f be
PartFunc of
A,
REAL ;
let S be non
empty Division of
A;
let D be
Element of
S;
func upper_volume f,
D -> FinSequence of
REAL means :
Def7:
:: INTEGRA1:def 7
(
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:
:: INTEGRA1:def 8
(
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
REAL ;
let f be
PartFunc of
A,
REAL ;
func upper_sum_set f -> PartFunc of
divs A,
REAL means :
Def11:
:: INTEGRA1:def 11
(
dom it = divs A & ( for
D being
Element of
divs A st
D in dom it holds
it . D = upper_sum f,
D ) );
existence
ex b1 being PartFunc of divs A, REAL st
( dom b1 = divs A & ( for D being Element of divs A st D in dom b1 holds
b1 . D = upper_sum f,D ) )
uniqueness
for b1, b2 being PartFunc of divs A, REAL st dom b1 = divs A & ( for D being Element of divs A st D in dom b1 holds
b1 . D = upper_sum f,D ) & dom b2 = divs A & ( for D being Element of divs A st D in dom b2 holds
b2 . D = upper_sum f,D ) holds
b1 = b2
func lower_sum_set f -> PartFunc of
divs A,
REAL means :
Def12:
:: INTEGRA1:def 12
(
dom it = divs A & ( for
D being
Element of
divs A st
D in dom it holds
it . D = lower_sum f,
D ) );
existence
ex b1 being PartFunc of divs A, REAL st
( dom b1 = divs A & ( for D being Element of divs A st D in dom b1 holds
b1 . D = lower_sum f,D ) )
uniqueness
for b1, b2 being PartFunc of divs A, REAL st dom b1 = divs A & ( for D being Element of divs A st D in dom b1 holds
b1 . D = lower_sum f,D ) & dom b2 = divs A & ( for D being Element of divs 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 :
theorem Th12: :: INTEGRA1:12
theorem Th13: :: INTEGRA1:13
theorem :: INTEGRA1:14
theorem Th15: :: INTEGRA1:15
theorem :: INTEGRA1:16
theorem :: INTEGRA1:17
theorem Th18: :: INTEGRA1:18
theorem Th19: :: INTEGRA1:19
theorem Th20: :: INTEGRA1:20
theorem Th21: :: INTEGRA1:21
theorem Th22: :: INTEGRA1:22
theorem :: INTEGRA1:23
theorem Th24: :: INTEGRA1:24
theorem Th25: :: INTEGRA1:25
theorem Th26: :: INTEGRA1:26
theorem Th27: :: INTEGRA1:27
theorem :: INTEGRA1:28
theorem Th29: :: INTEGRA1:29
theorem Th30: :: INTEGRA1:30
:: deftheorem defines delta INTEGRA1:def 19 :
:: deftheorem Def20 defines <= INTEGRA1:def 20 :
theorem Th31: :: INTEGRA1:31
theorem Th32: :: INTEGRA1:32
theorem Th33: :: INTEGRA1:33
theorem :: INTEGRA1:34
theorem Th35: :: INTEGRA1:35
:: deftheorem Def21 defines indx INTEGRA1:def 21 :
theorem Th36: :: INTEGRA1:36
theorem Th37: :: INTEGRA1:37
theorem Th38: :: INTEGRA1:38
for
A being
closed-interval Subset of
REAL for
S being non
empty Division of
A for
D being
Element of
S for
i,
j being
Element of
NAT st
i in dom D &
j in dom D &
i <= j holds
ex
B being
closed-interval Subset of
REAL 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
DivisionPoint of
B )
theorem Th39: :: INTEGRA1:39
:: deftheorem Def22 defines PartSums INTEGRA1:def 22 :
theorem Th40: :: INTEGRA1:40
theorem Th41: :: INTEGRA1:41
theorem Th42: :: INTEGRA1:42
theorem Th43: :: INTEGRA1:43
theorem Th44: :: INTEGRA1:44
theorem Th45: :: INTEGRA1:45
theorem Th46: :: INTEGRA1:46
theorem Th47: :: INTEGRA1:47
theorem Th48: :: INTEGRA1:48
theorem Th49: :: INTEGRA1:49
theorem Th50: :: INTEGRA1:50
theorem Th51: :: INTEGRA1:51
theorem Th52: :: INTEGRA1:52
theorem Th53: :: INTEGRA1:53
theorem Th54: :: INTEGRA1:54
theorem Th55: :: INTEGRA1:55
theorem Th56: :: INTEGRA1:56
theorem Th57: :: INTEGRA1:57
theorem Th58: :: INTEGRA1:58
theorem :: INTEGRA1:59