let D be set ; :: thesis: for f being PartFunc of (REAL 3),REAL st f is_partial_differentiable`3_on D holds
( D c= dom f & ( for u being Element of REAL 3 st u in D holds
f is_partial_differentiable_in u,3 ) )
let f be PartFunc of (REAL 3),REAL; :: thesis: ( f is_partial_differentiable`3_on D implies ( D c= dom f & ( for u being Element of REAL 3 st u in D holds
f is_partial_differentiable_in u,3 ) ) )
assume A1: f is_partial_differentiable`3_on D ; :: thesis: ( D c= dom f & ( for u being Element of REAL 3 st u in D holds
f is_partial_differentiable_in u,3 ) )
hence D c= dom f ; :: thesis: for u being Element of REAL 3 st u in D holds
f is_partial_differentiable_in u,3
set g = f | D;
let u0 be Element of REAL 3; :: thesis: ( u0 in D implies f is_partial_differentiable_in u0,3 )
assume u0 in D ; :: thesis: f is_partial_differentiable_in u0,3
then f | D is_partial_differentiable_in u0,3 by A1;
then consider x0, y0, z0 being Real such that
A2: ( u0 = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 (3,(f | D),u0)) & ex L being LinearFunc ex R being RestFunc st
for z being Real st z in N holds
((SVF1 (3,(f | D),u0)) . z) - ((SVF1 (3,(f | D),u0)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) by Th15;
consider N being Neighbourhood of z0 such that
A3: ( N c= dom (SVF1 (3,(f | D),u0)) & ex L being LinearFunc ex R being RestFunc st
for z being Real st z in N holds
((SVF1 (3,(f | D),u0)) . z) - ((SVF1 (3,(f | D),u0)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) by A2;
for z being Real st z in dom (SVF1 (3,(f | D),u0)) holds
z in dom (SVF1 (3,f,u0))
proof
let z be Real; :: thesis: ( z in dom (SVF1 (3,(f | D),u0)) implies z in dom (SVF1 (3,f,u0)) )
assume z in dom (SVF1 (3,(f | D),u0)) ; :: thesis: z in dom (SVF1 (3,f,u0))
then A4: ( z in dom (reproj (3,u0)) & (reproj (3,u0)) . z in dom (f | D) ) by FUNCT_1:11;
dom (f | D) = (dom f) /\ D by RELAT_1:61;
then dom (f | D) c= dom f by XBOOLE_1:17;
hence z in dom (SVF1 (3,f,u0)) by A4, FUNCT_1:11; :: thesis: verum
end;
then for z being object st z in dom (SVF1 (3,(f | D),u0)) holds
z in dom (SVF1 (3,f,u0)) ;
then dom (SVF1 (3,(f | D),u0)) c= dom (SVF1 (3,f,u0)) ;
then A5: N c= dom (SVF1 (3,f,u0)) by A3;
consider L being LinearFunc, R being RestFunc such that
A6: for z being Real st z in N holds
((SVF1 (3,(f | D),u0)) . z) - ((SVF1 (3,(f | D),u0)) . z0) = (L . (z - z0)) + (R . (z - z0)) by A3;
for z being Real st z in N holds
((SVF1 (3,f,u0)) . z) - ((SVF1 (3,f,u0)) . z0) = (L . (z - z0)) + (R . (z - z0))
proof
let z be Real; :: thesis: ( z in N implies ((SVF1 (3,f,u0)) . z) - ((SVF1 (3,f,u0)) . z0) = (L . (z - z0)) + (R . (z - z0)) )
assume A7: z in N ; :: thesis: ((SVF1 (3,f,u0)) . z) - ((SVF1 (3,f,u0)) . z0) = (L . (z - z0)) + (R . (z - z0))
A8: for z being Real st z in dom (SVF1 (3,(f | D),u0)) holds
(SVF1 (3,(f | D),u0)) . z = (SVF1 (3,f,u0)) . z
proof
let z be Real; :: thesis: ( z in dom (SVF1 (3,(f | D),u0)) implies (SVF1 (3,(f | D),u0)) . z = (SVF1 (3,f,u0)) . z )
assume A9: z in dom (SVF1 (3,(f | D),u0)) ; :: thesis: (SVF1 (3,(f | D),u0)) . z = (SVF1 (3,f,u0)) . z
then A10: ( z in dom (reproj (3,u0)) & (reproj (3,u0)) . z in dom (f | D) ) by FUNCT_1:11;
(SVF1 (3,(f | D),u0)) . z = (f | D) . ((reproj (3,u0)) . z) by A9, FUNCT_1:12
.= f . ((reproj (3,u0)) . z) by A10, FUNCT_1:47
.= (SVF1 (3,f,u0)) . z by A10, FUNCT_1:13 ;
hence (SVF1 (3,(f | D),u0)) . z = (SVF1 (3,f,u0)) . z ; :: thesis: verum
end;
A11: z0 in N by RCOMP_1:16;
(L . (z - z0)) + (R . (z - z0)) = ((SVF1 (3,(f | D),u0)) . z) - ((SVF1 (3,(f | D),u0)) . z0) by A6, A7
.= ((SVF1 (3,f,u0)) . z) - ((SVF1 (3,(f | D),u0)) . z0) by A3, A7, A8
.= ((SVF1 (3,f,u0)) . z) - ((SVF1 (3,f,u0)) . z0) by A3, A8, A11 ;
hence ((SVF1 (3,f,u0)) . z) - ((SVF1 (3,f,u0)) . z0) = (L . (z - z0)) + (R . (z - z0)) ; :: thesis: verum
end;
hence f is_partial_differentiable_in u0,3 by A2, A5, Th15; :: thesis: verum