let Z be Subset of (REAL 2); for f being PartFunc of (REAL 2),REAL st f is_partial_differentiable`1_on Z holds
( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds
f is_partial_differentiable_in z,1 ) )
let f be PartFunc of (REAL 2),REAL ; ( f is_partial_differentiable`1_on Z implies ( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds
f is_partial_differentiable_in z,1 ) ) )
set g = f | Z;
assume A1:
f is_partial_differentiable`1_on Z
; ( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds
f is_partial_differentiable_in z,1 ) )
hence
Z c= dom f
by Def2; for z being Element of REAL 2 st z in Z holds
f is_partial_differentiable_in z,1
let z0 be Element of REAL 2; ( z0 in Z implies f is_partial_differentiable_in z0,1 )
assume
z0 in Z
; f is_partial_differentiable_in z0,1
then
f | Z is_partial_differentiable_in z0,1
by A1, Def2;
then consider x0, y0 being Real such that
A2:
z0 = <*x0,y0*>
and
A3:
ex N being Neighbourhood of x0 st
( N c= dom (SVF1 1,(f | Z),z0) & ex L being LINEAR ex R being REST st
for x being Real st x in N holds
((SVF1 1,(f | Z),z0) . x) - ((SVF1 1,(f | Z),z0) . x0) = (L . (x - x0)) + (R . (x - x0)) )
by Th9;
consider N being Neighbourhood of x0 such that
A4:
N c= dom (SVF1 1,(f | Z),z0)
and
A5:
ex L being LINEAR ex R being REST st
for x being Real st x in N holds
((SVF1 1,(f | Z),z0) . x) - ((SVF1 1,(f | Z),z0) . x0) = (L . (x - x0)) + (R . (x - x0))
by A3;
consider L being LINEAR, R being REST such that
A6:
for x being Real st x in N holds
((SVF1 1,(f | Z),z0) . x) - ((SVF1 1,(f | Z),z0) . x0) = (L . (x - x0)) + (R . (x - x0))
by A5;
A7:
for x being Real st x in N holds
((SVF1 1,f,z0) . x) - ((SVF1 1,f,z0) . x0) = (L . (x - x0)) + (R . (x - x0))
proof
let x be
Real;
( x in N implies ((SVF1 1,f,z0) . x) - ((SVF1 1,f,z0) . x0) = (L . (x - x0)) + (R . (x - x0)) )
A8:
for
x being
Real st
x in dom (SVF1 1,(f | Z),z0) holds
(SVF1 1,(f | Z),z0) . x = (SVF1 1,f,z0) . x
proof
let x be
Real;
( x in dom (SVF1 1,(f | Z),z0) implies (SVF1 1,(f | Z),z0) . x = (SVF1 1,f,z0) . x )
assume A9:
x in dom (SVF1 1,(f | Z),z0)
;
(SVF1 1,(f | Z),z0) . x = (SVF1 1,f,z0) . x
then A10:
x in dom (reproj 1,z0)
by FUNCT_1:21;
A11:
(reproj 1,z0) . x in dom (f | Z)
by A9, FUNCT_1:21;
(SVF1 1,(f | Z),z0) . x =
(f | Z) . ((reproj 1,z0) . x)
by A9, FUNCT_1:22
.=
f . ((reproj 1,z0) . x)
by A11, FUNCT_1:70
.=
(SVF1 1,f,z0) . x
by A10, FUNCT_1:23
;
hence
(SVF1 1,(f | Z),z0) . x = (SVF1 1,f,z0) . x
;
verum
end;
A12:
x0 in N
by RCOMP_1:37;
assume A13:
x in N
;
((SVF1 1,f,z0) . x) - ((SVF1 1,f,z0) . x0) = (L . (x - x0)) + (R . (x - x0))
then (L . (x - x0)) + (R . (x - x0)) =
((SVF1 1,(f | Z),z0) . x) - ((SVF1 1,(f | Z),z0) . x0)
by A6
.=
((SVF1 1,f,z0) . x) - ((SVF1 1,(f | Z),z0) . x0)
by A4, A13, A8
.=
((SVF1 1,f,z0) . x) - ((SVF1 1,f,z0) . x0)
by A4, A8, A12
;
hence
((SVF1 1,f,z0) . x) - ((SVF1 1,f,z0) . x0) = (L . (x - x0)) + (R . (x - x0))
;
verum
end;
for x being Real st x in dom (SVF1 1,(f | Z),z0) holds
x in dom (SVF1 1,f,z0)
proof
let x be
Real;
( x in dom (SVF1 1,(f | Z),z0) implies x in dom (SVF1 1,f,z0) )
dom (f | Z) = (dom f) /\ Z
by RELAT_1:90;
then A14:
dom (f | Z) c= dom f
by XBOOLE_1:17;
assume
x in dom (SVF1 1,(f | Z),z0)
;
x in dom (SVF1 1,f,z0)
then
(
x in dom (reproj 1,z0) &
(reproj 1,z0) . x in dom (f | Z) )
by FUNCT_1:21;
hence
x in dom (SVF1 1,f,z0)
by A14, FUNCT_1:21;
verum
end;
then
for x being set st x in dom (SVF1 1,(f | Z),z0) holds
x in dom (SVF1 1,f,z0)
;
then
dom (SVF1 1,(f | Z),z0) c= dom (SVF1 1,f,z0)
by TARSKI:def 3;
then
N c= dom (SVF1 1,f,z0)
by A4, XBOOLE_1:1;
hence
f is_partial_differentiable_in z0,1
by A2, A7, Th9; verum