let X be set ; 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; 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; ( 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
; f is_differentiable_on Z
A3:
f | X is differentiable
by A1;
X c= dom f
by A1;
hence
Z c= dom f
by A2; CFDIFF_1:def 9 f | Z is differentiable
let x0 be Complex; CFDIFF_1:def 8 ( x0 in dom (f | Z) implies f | Z is_differentiable_in x0 )
assume A4:
x0 in dom (f | Z)
; f | Z is_differentiable_in x0
then A5:
x0 in dom f
by RELAT_1:57;
A6:
x0 in Z
by A4, RELAT_1:57;
then consider N1 being Neighbourhood of x0 such that
A7:
N1 c= Z
by Th9;
x0 in dom (f | X)
by A2, A5, A6, RELAT_1:57;
then
f | X is_differentiable_in x0
by A3;
then consider N being Neighbourhood of x0 such that
A8:
N c= dom (f | X)
and
A9:
ex L being C_LinearFunc ex R being C_RestFunc st
for x being Complex st x in N holds
((f | X) /. x) - ((f | X) /. x0) = (L /. (x - x0)) + (R /. (x - x0))
;
consider N2 being Neighbourhood of x0 such that
A10:
N2 c= N
and
A11:
N2 c= N1
by Lm1;
A12:
N2 c= Z
by A7, A11;
take
N2
; CFDIFF_1:def 6 ( N2 c= dom (f | Z) & ex L being C_LinearFunc ex R being C_RestFunc 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:61;
then
dom (f | X) c= dom f
by XBOOLE_1:17;
then
N c= dom f
by A8;
then
N2 c= dom f
by A10;
then
N2 c= (dom f) /\ Z
by A12, XBOOLE_1:19;
hence A13:
N2 c= dom (f | Z)
by RELAT_1:61; ex L being C_LinearFunc ex R being C_RestFunc 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_LinearFunc, R being C_RestFunc such that
A14:
for x being Complex st x in N holds
((f | X) /. x) - ((f | X) /. x0) = (L /. (x - x0)) + (R /. (x - x0))
by A9;
take
L
; ex R being C_RestFunc st
for z being Complex st z in N2 holds
((f | Z) /. z) - ((f | Z) /. x0) = (L /. (z - x0)) + (R /. (z - x0))
take
R
; 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; ( x in N2 implies ((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )
assume A15:
x in N2
; ((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0))
then
((f | X) /. x) - ((f | X) /. x0) = (L /. (x - x0)) + (R /. (x - x0))
by A10, A14;
then A16:
((f | X) /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
by A2, A5, A6, PARTFUN2:17;
x in N
by A10, A15;
then
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
by A8, A16, PARTFUN2:15;
then
(f /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0))
by A5, A6, PARTFUN2:17;
hence
((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0))
by A13, A15, PARTFUN2:15; verum