let X be set ; for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st f is_differentiable_on X & Z c= X holds
f is_differentiable_on Z
let Z be open Subset of REAL; for f being PartFunc of REAL,REAL st f is_differentiable_on X & Z c= X holds
f is_differentiable_on Z
let f be PartFunc of REAL,REAL; ( 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
X c= dom f
by A1;
hence
Z c= dom f
by A2; FDIFF_1:def 6 for x being Real st x in Z holds
f | Z is_differentiable_in x
let x0 be Real; ( x0 in Z implies f | Z is_differentiable_in x0 )
assume A3:
x0 in Z
; f | Z is_differentiable_in x0
then
f | X is_differentiable_in x0
by A1, A2;
then consider N being Neighbourhood of x0 such that
A4:
N c= dom (f | X)
and
A5:
ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((f | X) . x) - ((f | X) . x0) = (L . (x - x0)) + (R . (x - x0))
;
consider N1 being Neighbourhood of x0 such that
A6:
N1 c= Z
by A3, RCOMP_1:18;
consider N2 being Neighbourhood of x0 such that
A7:
N2 c= N
and
A8:
N2 c= N1
by RCOMP_1:17;
A9:
N2 c= Z
by A6, A8;
take
N2
; FDIFF_1:def 4 ( N2 c= dom (f | Z) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N2 holds
((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - 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 A4;
then
N2 c= dom f
by A7;
then
N2 c= (dom f) /\ Z
by A9, XBOOLE_1:19;
hence A10:
N2 c= dom (f | Z)
by RELAT_1:61; ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N2 holds
((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0))
consider L being LinearFunc, R being RestFunc such that
A11:
for x being Real st x in N holds
((f | X) . x) - ((f | X) . x0) = (L . (x - x0)) + (R . (x - x0))
by A5;
take
L
; ex R being RestFunc st
for x being Real st x in N2 holds
((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0))
take
R
; for x being Real st x in N2 holds
((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0))
let x be Real; ( x in N2 implies ((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) )
assume A12:
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 A7, A11;
then A13:
((f | X) . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))
by A2, A3, FUNCT_1:49;
x in N
by A7, A12;
then
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))
by A4, A13, FUNCT_1:47;
then
(f . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0))
by A3, FUNCT_1:49;
hence
((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0))
by A10, A12, FUNCT_1:47; verum