begin
theorem LM001:
:: deftheorem defines Re INTEGR16:def 1 :
:: deftheorem defines Im INTEGR16:def 2 :
:: deftheorem Def5 defines middle_volume INTEGR16:def 3 :
:: deftheorem defines middle_sum INTEGR16:def 4 :
:: deftheorem Def7 defines middle_volume_Sequence INTEGR16:def 5 :
:: deftheorem Def8 defines middle_sum INTEGR16:def 6 :
begin
theorem
theorem
theorem LMDef5:
RVSUM1102:
Sum (<*> COMPLEX ) = 0
by BINOP_2:1, FINSOP_1:11;
RVSUM1104:
for F being FinSequence of COMPLEX
for x being Element of COMPLEX holds Sum (F ^ <*x*>) = (Sum F) + x
theorem RVSUM1105:
theorem RVSUM2105:
theorem LMDefR0:
theorem LMDefI0:
theorem
theorem
:: deftheorem Def13 defines integrable INTEGR16:def 7 :
theorem BND01A:
theorem BND01B:
theorem BND01:
:: deftheorem defines integral INTEGR16:def 8 :
theorem Th11:
theorem
:: deftheorem Def16 defines is_integrable_on INTEGR16:def 9 :
:: deftheorem defines integral INTEGR16:def 10 :
Lm5:
for f being PartFunc of REAL ,COMPLEX
for A being non empty Subset of REAL
for g being Function of A,COMPLEX st f = g holds
( Re f = Re g & Im f = Im g )
Lm6:
for f being PartFunc of REAL ,COMPLEX
for A being Subset of REAL holds
( Re (f | A) = (Re f) | A & Im (f | A) = (Im f) | A )
theorem
theorem
definition
let a,
b be
real number ;
let f be
PartFunc of
REAL ,
COMPLEX ;
func integral f,
a,
b -> Element of
COMPLEX equals
(integral (Re f),a,b) + ((integral (Im f),a,b) * <i> );
correctness
coherence
(integral (Re f),a,b) + ((integral (Im f),a,b) * <i> ) is Element of COMPLEX ;
;
end;
:: deftheorem defines integral INTEGR16:def 11 :
begin
theorem Th16C:
theorem
theorem
theorem
theorem
theorem