let F be RealNormSpace; for X being set
for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X & Z c= X holds
f is_differentiable_on Z
let X be set ; for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F 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, the carrier of F st f is_differentiable_on X & Z c= X holds
f is_differentiable_on Z
let f be PartFunc of REAL, the carrier of F; ( 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;
then A3:
Z c= dom f
by A2;
now for x0 being Real st x0 in Z holds
f | Z is_differentiable_in x0let x0 be
Real;
( x0 in Z implies f | Z is_differentiable_in x0 )assume A4:
x0 in Z
;
f | Z is_differentiable_in x0then
f | X is_differentiable_in x0
by A1, A2;
then consider N being
Neighbourhood of
x0 such that A5:
N c= dom (f | X)
and A6:
ex
L being
LinearFunc of
F ex
R being
RestFunc of
F 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 A7:
N1 c= Z
by A4, RCOMP_1:18;
consider N2 being
Neighbourhood of
x0 such that A8:
N2 c= N
and A9:
N2 c= N1
by RCOMP_1:17;
A10:
N2 c= Z
by A7, A9;
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 A5;
then
N2 c= dom f
by A8;
then
N2 c= (dom f) /\ Z
by A10, XBOOLE_1:19;
then A11:
N2 c= dom (f | Z)
by RELAT_1:61;
A12:
N2 c= dom (f | X)
by A8, A5;
consider L being
LinearFunc of
F,
R being
RestFunc of
F such that A13:
for
x being
Real st
x in N holds
((f | X) /. x) - ((f | X) /. x0) = (L /. (x - x0)) + (R /. (x - x0))
by A6;
for
x being
Real st
x in N2 holds
((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0))
proof
let x be
Real;
( x in N2 implies ((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )
assume A14:
x in N2
;
((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0))
then A15:
((f | X) /. x) - ((f | X) /. x0) = (L /. (x - x0)) + (R /. (x - x0))
by A8, A13;
A16:
x0 in N2
by RCOMP_1:16;
((f | X) /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
by A15, A16, A12, PARTFUN2:15;
then
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
by A14, A12, PARTFUN2:15;
then
(f /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0))
by A16, A11, PARTFUN2:15;
hence
((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0))
by A14, A11, PARTFUN2:15;
verum
end; hence
f | Z is_differentiable_in x0
by A11;
verum end;
hence
f is_differentiable_on Z
by A3; verum