let X be set ; :: thesis: for f being PartFunc of COMPLEX ,COMPLEX
for Z being open Subset of COMPLEX st f is_differentiable_on X & Z c= X holds
f is_differentiable_on Z
let f be PartFunc of COMPLEX ,COMPLEX ; :: thesis: for Z being open Subset of COMPLEX st f is_differentiable_on X & Z c= X holds
f is_differentiable_on Z
let Z be open Subset of COMPLEX ; :: thesis: ( f is_differentiable_on X & Z c= X implies f is_differentiable_on Z )
assume that
A1: f is_differentiable_on X and
A2: Z c= X ; :: thesis: f is_differentiable_on Z
X c= dom f by A1, Def9;
hence Z c= dom f by A2, XBOOLE_1:1; :: according to CFDIFF_1:def 9 :: thesis: f | Z is differentiable
let x0 be Complex; :: according to CFDIFF_1:def 8 :: thesis: ( x0 in dom (f | Z) implies f | Z is_differentiable_in x0 )
assume x0 in dom (f | Z) ; :: thesis: f | Z is_differentiable_in x0
then A3: ( x0 in dom f & x0 in Z ) by RELAT_1:86;
then A4: x0 in dom (f | X) by A2, RELAT_1:86;
f | X is differentiable by A1, Def9;
then f | X is_differentiable_in x0 by A4, Def8;
then consider N being Neighbourhood of x0 such that
A5: ( N c= dom (f | X) & ex L being C_LINEAR ex R being C_REST st
for x being Complex st x in N holds
((f | X) /. x) - ((f | X) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) by Def6;
consider N1 being Neighbourhood of x0 such that
A6: N1 c= Z by A3, Th12;
consider N2 being Neighbourhood of x0 such that
A7: ( N2 c= N & N2 c= N1 ) by Th10;
take N2 ; :: according to CFDIFF_1:def 6 :: thesis: ( N2 c= dom (f | Z) & ex L being C_LINEAR ex R being C_REST st
for z being Complex st z in N2 holds
((f | Z) /. z) - ((f | Z) /. x0) = (L /. (z - x0)) + (R /. (z - x0)) )
dom (f | X) = (dom f) /\ X by RELAT_1:90;
then dom (f | X) c= dom f by XBOOLE_1:17;
then N c= dom f by A5, XBOOLE_1:1;
then A8: N2 c= dom f by A7, XBOOLE_1:1;
N2 c= Z by A6, A7, XBOOLE_1:1;
then N2 c= (dom f) /\ Z by A8, XBOOLE_1:19;
hence A9: N2 c= dom (f | Z) by RELAT_1:90; :: thesis: ex L being C_LINEAR ex R being C_REST st
for z being Complex st z in N2 holds
((f | Z) /. z) - ((f | Z) /. x0) = (L /. (z - x0)) + (R /. (z - x0))
consider L being C_LINEAR, R being C_REST such that
A10: for x being Complex st x in N holds
((f | X) /. x) - ((f | X) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A5;
take L ; :: thesis: ex R being C_REST st
for z being Complex st z in N2 holds
((f | Z) /. z) - ((f | Z) /. x0) = (L /. (z - x0)) + (R /. (z - x0))
take R ; :: thesis: for z being Complex st z in N2 holds
((f | Z) /. z) - ((f | Z) /. x0) = (L /. (z - x0)) + (R /. (z - x0))
let x be Complex; :: thesis: ( x in N2 implies ((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )
assume A11: x in N2 ; :: thesis: ((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0))
then A12: x in N by A7;
((f | X) /. x) - ((f | X) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A7, A10, A11;
then ((f | X) /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A3, A2, PARTFUN2:35;
then (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A5, A12, PARTFUN2:32;
then (f /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A3, PARTFUN2:35;
hence ((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A9, A11, PARTFUN2:32; :: thesis: verum