let S, T be non trivial RealNormSpace; :: thesis: for f being PartFunc of S,T
for Z being Subset of S st Z is open holds
( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Point of S st x in Z holds
f is_differentiable_in x ) ) )
let f be PartFunc of S,T; :: thesis: for Z being Subset of S st Z is open holds
( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Point of S st x in Z holds
f is_differentiable_in x ) ) )
let Z be Subset of S; :: thesis: ( Z is open implies ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Point of S st x in Z holds
f is_differentiable_in x ) ) ) )
assume A1:
Z is open
; :: thesis: ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Point of S st x in Z holds
f is_differentiable_in x ) ) )
thus
( f is_differentiable_on Z implies ( Z c= dom f & ( for x being Point of S st x in Z holds
f is_differentiable_in x ) ) )
:: thesis: ( Z c= dom f & ( for x being Point of S st x in Z holds
f is_differentiable_in x ) implies f is_differentiable_on Z )proof
assume A2:
f is_differentiable_on Z
;
:: thesis: ( Z c= dom f & ( for x being Point of S st x in Z holds
f is_differentiable_in x ) )
hence A3:
Z c= dom f
by Def8;
:: thesis: for x being Point of S st x in Z holds
f is_differentiable_in x
let x0 be
Point of
S;
:: thesis: ( x0 in Z implies f is_differentiable_in x0 )
assume A4:
x0 in Z
;
:: thesis: f is_differentiable_in x0
then
f | Z is_differentiable_in x0
by A2, Def8;
then consider N being
Neighbourhood of
x0 such that A5:
(
N c= dom (f | Z) & ex
L being
Point of
(R_NormSpace_of_BoundedLinearOperators S,T) ex
R being
REST of
S,
T st
for
x being
Point of
S st
x in N holds
((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
by Def6;
take
N
;
:: according to NDIFF_1:def 6 :: thesis: ( N c= dom f & ex L being Point of (R_NormSpace_of_BoundedLinearOperators S,T) ex R being REST of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
A6:
dom (f | Z) = (dom f) /\ Z
by RELAT_1:90;
then
dom (f | Z) c= dom f
by XBOOLE_1:17;
hence
N c= dom f
by A5, XBOOLE_1:1;
:: thesis: ex L being Point of (R_NormSpace_of_BoundedLinearOperators S,T) ex R being REST of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
consider L being
Point of
(R_NormSpace_of_BoundedLinearOperators S,T),
R being
REST of
S,
T such that A7:
for
x being
Point of
S st
x in N holds
((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0))
by A5;
take
L
;
:: thesis: ex R being REST of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
take
R
;
:: thesis: for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
let x be
Point of
S;
:: thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
assume A8:
x in N
;
:: thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
then
((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0))
by A7;
then
(f /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0))
by A5, A6, A8, PARTFUN2:34;
hence
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
by A3, A4, PARTFUN2:35;
:: thesis: verum
end;
assume A9:
( Z c= dom f & ( for x being Point of S st x in Z holds
f is_differentiable_in x ) )
; :: thesis: f is_differentiable_on Z
hence
Z c= dom f
; :: according to NDIFF_1:def 8 :: thesis: for x being Point of S st x in Z holds
f | Z is_differentiable_in x
let x0 be Point of S; :: thesis: ( x0 in Z implies f | Z is_differentiable_in x0 )
assume A10:
x0 in Z
; :: thesis: f | Z is_differentiable_in x0
then
f is_differentiable_in x0
by A9;
then consider N being Neighbourhood of x0 such that
A11:
( N c= dom f & ex L being Point of (R_NormSpace_of_BoundedLinearOperators S,T) ex R being REST of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
by Def6;
consider N1 being Neighbourhood of x0 such that
A12:
N1 c= Z
by A1, A10, Th2;
consider N2 being Neighbourhood of x0 such that
A13:
( N2 c= N1 & N2 c= N )
by Th1;
take
N2
; :: according to NDIFF_1:def 6 :: thesis: ( N2 c= dom (f | Z) & ex L being Point of (R_NormSpace_of_BoundedLinearOperators S,T) ex R being REST of S,T st
for x being Point of S st x in N2 holds
((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
A14:
N2 c= dom f
by A11, A13, XBOOLE_1:1;
N2 c= Z
by A12, A13, XBOOLE_1:1;
then A15:
N2 c= (dom f) /\ Z
by A14, XBOOLE_1:19;
hence
N2 c= dom (f | Z)
by RELAT_1:90; :: thesis: ex L being Point of (R_NormSpace_of_BoundedLinearOperators S,T) ex R being REST of S,T st
for x being Point of S st x in N2 holds
((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0))
consider L being Point of (R_NormSpace_of_BoundedLinearOperators S,T), R being REST of S,T such that
A16:
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
by A11;
take
L
; :: thesis: ex R being REST of S,T st
for x being Point of S st x in N2 holds
((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0))
take
R
; :: thesis: for x being Point of S st x in N2 holds
((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0))
let x be Point of S; :: thesis: ( x in N2 implies ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
assume A17:
x in N2
; :: thesis: ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0))
then
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
by A13, A16;
then A18:
((f | Z) /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
by A15, A17, PARTFUN2:34;
x0 in N2
by NFCONT_1:4;
hence
((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0))
by A15, A18, PARTFUN2:34; :: thesis: verum