let S, T be RealNormSpace; 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; 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; ( 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
; ( 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 ) ) )
( 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
;
( 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
;
for x being Point of S st x in Z holds
f is_differentiable_in x
let x0 be
Point of
S;
( x0 in Z implies f is_differentiable_in x0 )
assume A4:
x0 in Z
;
f is_differentiable_in x0
then
f | Z is_differentiable_in x0
by A2;
then consider N being
Neighbourhood of
x0 such that A5:
N c= dom (f | Z)
and A6:
ex
L being
Point of
(R_NormSpace_of_BoundedLinearOperators (S,T)) ex
R being
RestFunc 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))
;
consider L being
Point of
(R_NormSpace_of_BoundedLinearOperators (S,T)),
R being
RestFunc 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 A6;
take
N
;
NDIFF_1:def 6 ( N c= dom f & ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc 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)) )
A8:
dom (f | Z) = (dom f) /\ Z
by RELAT_1:61;
then
dom (f | Z) c= dom f
by XBOOLE_1:17;
hence
N c= dom f
by A5;
ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc 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
L
;
ex R being RestFunc 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
;
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;
( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
assume A9:
x in N
;
(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, A8, A9, PARTFUN2:16;
hence
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
by A3, A4, PARTFUN2:17;
verum
end;
assume that
A10:
Z c= dom f
and
A11:
for x being Point of S st x in Z holds
f is_differentiable_in x
; f is_differentiable_on Z
thus
Z c= dom f
by A10; NDIFF_1:def 8 for x being Point of S st x in Z holds
f | Z is_differentiable_in x
let x0 be Point of S; ( x0 in Z implies f | Z is_differentiable_in x0 )
assume A12:
x0 in Z
; f | Z is_differentiable_in x0
then consider N1 being Neighbourhood of x0 such that
A13:
N1 c= Z
by A1, Th2;
f is_differentiable_in x0
by A11, A12;
then consider N being Neighbourhood of x0 such that
A14:
N c= dom f
and
A15:
ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc 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 N2 being Neighbourhood of x0 such that
A16:
N2 c= N1
and
A17:
N2 c= N
by Th1;
A18:
N2 c= Z
by A13, A16;
take
N2
; NDIFF_1:def 6 ( N2 c= dom (f | Z) & ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc 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)) )
N2 c= dom f
by A14, A17;
then A19:
N2 c= (dom f) /\ Z
by A18, XBOOLE_1:19;
hence
N2 c= dom (f | Z)
by RELAT_1:61; ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc 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))
A20:
x0 in N2
by NFCONT_1:4;
consider L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)), R being RestFunc of S,T such that
A21:
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
by A15;
take
L
; ex R being RestFunc 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
; 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; ( x in N2 implies ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
assume A22:
x in N2
; ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0))
then
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
by A17, A21;
then
((f | Z) /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
by A19, A22, PARTFUN2:16;
hence
((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0))
by A19, A20, PARTFUN2:16; verum