begin
theorem Th1:
theorem Th2:
theorem Th3:
begin
theorem Th4:
theorem Th5:
:: deftheorem INTEGRA5:def 1 :
canceled;
:: deftheorem Def2 defines is_integrable_on INTEGRA5:def 2 :
:: deftheorem defines integral INTEGRA5:def 3 :
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
begin
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
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
theorem
theorem
:: 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:
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
theorem
theorem