:: deftheorem defines is_differentiable_in CFDIFF_1:def 6 :
for f being PartFunc of COMPLEX,COMPLEX
for z0 being Complex holds
( f is_differentiable_in z0 iff ex N being Neighbourhood of z0 st
( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st
for z being Complex st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) );