:: Definition of Integrability for Partial Functions from REAL toREAL and Integrability for Continuous Functions
:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama
::
:: Received March 23, 2000
:: Copyright (c) 2000 Association of Mizar Users
theorem Th1: :: INTEGRA5:1
theorem Th2: :: INTEGRA5:2
theorem Th3: :: INTEGRA5:3
theorem Th4: :: INTEGRA5:4
theorem Th5: :: INTEGRA5:5
:: deftheorem INTEGRA5:def 1 :
canceled;
:: deftheorem Def2 defines is_integrable_on INTEGRA5:def 2 :
:: deftheorem defines integral INTEGRA5:def 3 :
theorem Th6: :: INTEGRA5:6
theorem Th7: :: INTEGRA5:7
theorem Th8: :: INTEGRA5:8
theorem Th9: :: INTEGRA5:9
theorem Th10: :: INTEGRA5:10
theorem Th11: :: INTEGRA5:11
theorem Th12: :: INTEGRA5:12
theorem Th13: :: INTEGRA5:13
theorem Th14: :: INTEGRA5:14
theorem Th15: :: INTEGRA5:15
Lm1:
for A being closed-interval Subset of REAL
for f being PartFunc of REAL , REAL st f | A is non-decreasing & A c= dom f holds
f is_integrable_on A
theorem :: INTEGRA5:16
theorem :: INTEGRA5:17
theorem :: INTEGRA5:18
:: deftheorem Def4 defines [' INTEGRA5:def 4 :
definition
let a,
b be
real number ;
let f be
PartFunc of
REAL ,
REAL ;
func integral f,
a,
b -> Real equals :
Def5:
:: INTEGRA5:def 5
integral f,
['a,b'] if a <= b otherwise - (integral f,['b,a']);
correctness
coherence
( ( a <= b implies integral f,['a,b'] is Real ) & ( not a <= b implies - (integral f,['b,a']) is Real ) );
consistency
for b1 being Real holds verum;
;
end;
:: deftheorem Def5 defines integral INTEGRA5:def 5 :
for
a,
b being
real number for
f being
PartFunc of
REAL ,
REAL holds
( (
a <= b implies
integral f,
a,
b = integral f,
['a,b'] ) & ( not
a <= b implies
integral f,
a,
b = - (integral f,['b,a']) ) );
theorem :: INTEGRA5:19
theorem :: INTEGRA5:20
theorem :: INTEGRA5:21