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 :
for A being closed-interval Subset of REAL
for f being PartFunc of REAL ,REAL holds
( f is_integrable_on A iff f || A is integrable );
:: deftheorem defines integral INTEGRA5:def 3 :
for A being closed-interval Subset of REAL
for f being PartFunc of REAL ,REAL holds integral f,A = integral (f || A);
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 :
for a, b being real number st a <= b holds
['a,b'] = [.a,b.];
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