:: Complex Function Differentiability
:: by Chanapat Pacharapokin , Hiroshi Yamazaki , Yasunari Shidama and Yatsuka Nakamura
::
:: Received November 4, 2008
:: Copyright (c) 2008 Association of Mizar Users
:: deftheorem Def1 defines convergent_to_0 CFDIFF_1:def 1 :
theorem :: CFDIFF_1:1
:: deftheorem Def2 defines InvShift CFDIFF_1:def 2 :
theorem Th2: :: CFDIFF_1:2
theorem Th3: :: CFDIFF_1:3
reconsider cs = NAT --> 0c as Complex_Sequence ;
theorem :: CFDIFF_1:4
theorem :: CFDIFF_1:5
:: 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 Th8: :: CFDIFF_1:6
theorem Th9: :: CFDIFF_1:7
Th10:
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 Th11: :: CFDIFF_1:8
:: deftheorem Def10 defines closed CFDIFF_1:def 10 :
:: deftheorem Def11 defines open CFDIFF_1:def 11 :
theorem Th12: :: CFDIFF_1:9
theorem :: CFDIFF_1:10
theorem Th14: :: CFDIFF_1:11
theorem :: CFDIFF_1:12
theorem Th16: :: CFDIFF_1:13
theorem :: CFDIFF_1:14
theorem Th18: :: CFDIFF_1:15
theorem :: CFDIFF_1:16
:: deftheorem Def12 defines `| CFDIFF_1:def 12 :
theorem :: CFDIFF_1:17
theorem Th22: :: CFDIFF_1:18
theorem Th23: :: CFDIFF_1:19
theorem Th24: :: CFDIFF_1:20
theorem Th25: :: CFDIFF_1:21
theorem Th26: :: CFDIFF_1:22
theorem Th27: :: CFDIFF_1:23
theorem Th28: :: CFDIFF_1:24
theorem Th29: :: CFDIFF_1:25
theorem Th30: :: CFDIFF_1:26
theorem :: CFDIFF_1:27
theorem :: CFDIFF_1:28
theorem :: CFDIFF_1:29
theorem :: CFDIFF_1:30
theorem :: CFDIFF_1:31
theorem :: CFDIFF_1:32
theorem :: CFDIFF_1:33
theorem Th38: :: CFDIFF_1:34
theorem :: CFDIFF_1:35
theorem :: CFDIFF_1:36
theorem :: CFDIFF_1:37
theorem :: CFDIFF_1:38