begin
:: deftheorem Def1 defines convergent_to_0 CFDIFF_1:def 1 :
theorem
:: deftheorem Def2 defines InvShift CFDIFF_1:def 2 :
theorem Th2:
theorem Th3:
reconsider cs = NAT --> 0c as Complex_Sequence ;
theorem
theorem
:: deftheorem Def3 defines REST-like CFDIFF_1:def 3 :
reconsider cf = COMPLEX --> 0c as Function of COMPLEX ,COMPLEX ;
:: deftheorem Def4 defines linear CFDIFF_1:def 4 :
:: deftheorem Def5 defines Neighbourhood CFDIFF_1:def 5 :
theorem Th6:
theorem Th7:
Lm1:
for z0 being Complex
for N1, N2 being Neighbourhood of z0 ex N being Neighbourhood of z0 st
( N c= N1 & N c= N2 )
:: deftheorem Def6 defines is_differentiable_in CFDIFF_1:def 6 :
:: deftheorem Def7 defines diff CFDIFF_1:def 7 :
:: deftheorem Def8 defines differentiable CFDIFF_1:def 8 :
:: deftheorem Def9 defines is_differentiable_on CFDIFF_1:def 9 :
theorem Th8:
:: deftheorem Def10 defines closed CFDIFF_1:def 10 :
:: deftheorem Def11 defines open CFDIFF_1:def 11 :
theorem Th9:
theorem
theorem Th11:
theorem
theorem Th13:
theorem
theorem Th15:
theorem
:: deftheorem Def12 defines `| CFDIFF_1:def 12 :
theorem
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th34:
theorem
theorem
theorem
theorem