:: INTEGRA5 semantic presentation
:: Showing IDV graph ... (Click the Palm Trees again to close it)
theorem Th1: :: INTEGRA5:1
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th2: :: INTEGRA5:2
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th3: :: INTEGRA5:3
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem defines || INTEGRA5:def 1 :
theorem Th4: :: INTEGRA5:4
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th5: :: INTEGRA5:5
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem Def2 defines is_integrable_on INTEGRA5:def 2 :
:: deftheorem defines integral INTEGRA5:def 3 :
theorem Th6: :: INTEGRA5:6
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th7: :: INTEGRA5:7
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th8: :: INTEGRA5:8
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th9: :: INTEGRA5:9
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th10: :: INTEGRA5:10
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th11: :: INTEGRA5:11
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th12: :: INTEGRA5:12
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th13: :: INTEGRA5:13
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th14: :: INTEGRA5:14
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th15: :: INTEGRA5:15
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
Lm1:
for A being closed-interval Subset of REAL
for f being PartFunc of REAL , REAL st f is_non_decreasing_on A & A c= dom f holds
f is_integrable_on A
theorem :: INTEGRA5:16
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th17: :: INTEGRA5:17
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: INTEGRA5:18
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: 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
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: INTEGRA5:20
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: INTEGRA5:21
:: Showing IDV graph ... (Click the Palm Tree again to close it) 