:: Scalar Multiple of Riemann Definite Integral
:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama
::
:: Received December 7, 1999
:: Copyright (c) 1999 Association of Mizar Users
theorem :: INTEGRA2:1
:: deftheorem Def1 defines non-decreasing INTEGRA2:def 1 :
theorem :: INTEGRA2:2
theorem :: INTEGRA2:3
theorem :: INTEGRA2:4
:: deftheorem Def2 defines ** INTEGRA2:def 2 :
theorem :: INTEGRA2:5
theorem :: INTEGRA2:6
theorem Th7: :: INTEGRA2:7
theorem Th8: :: INTEGRA2:8
theorem :: INTEGRA2:9
theorem :: INTEGRA2:10
theorem :: INTEGRA2:11
theorem :: INTEGRA2:12
theorem Th13: :: INTEGRA2:13
theorem Th14: :: INTEGRA2:14
theorem Th15: :: INTEGRA2:15
theorem Th16: :: INTEGRA2:16
theorem Th17: :: INTEGRA2:17
theorem Th18: :: INTEGRA2:18
theorem Th19: :: INTEGRA2:19
theorem Th20: :: INTEGRA2:20
theorem Th21: :: INTEGRA2:21
theorem Th22: :: INTEGRA2:22
theorem Th23: :: INTEGRA2:23
theorem Th24: :: INTEGRA2:24
theorem Th25: :: INTEGRA2:25
theorem Th26: :: INTEGRA2:26
theorem Th27: :: INTEGRA2:27
theorem Th28: :: INTEGRA2:28
theorem Th29: :: INTEGRA2:29
theorem Th30: :: INTEGRA2:30
theorem Th31: :: INTEGRA2:31
theorem Th32: :: INTEGRA2:32
theorem Th33: :: INTEGRA2:33
theorem :: INTEGRA2:34
theorem :: INTEGRA2:35
theorem :: INTEGRA2:36
:: deftheorem defines delta INTEGRA2:def 3 :
definition
let A be
closed-interval Subset of
REAL ;
let f be
PartFunc of
A,
REAL ;
let T be
DivSequence of
A;
func upper_sum f,
T -> Real_Sequence means :: INTEGRA2:def 4
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 :: INTEGRA2:def 5
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: :: INTEGRA2:37
theorem :: INTEGRA2:38
canceled;
theorem :: INTEGRA2:39
canceled;
theorem Th40: :: INTEGRA2:40
theorem :: INTEGRA2:41
theorem :: INTEGRA2:42