begin
definition
let f be
PartFunc of
(REAL 3),
REAL ;
let u be
Element of
REAL 3;
pred f is_hpartial_differentiable`11_in u means :
Def3:
ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
x0 st
(
N c= dom (SVF1 1,(pdiff1 f,1),u) & ex
L being
LINEAR ex
R being
REST st
for
x being
Real st
x in N holds
((SVF1 1,(pdiff1 f,1),u) . x) - ((SVF1 1,(pdiff1 f,1),u) . x0) = (L . (x - x0)) + (R . (x - x0)) ) );
pred f is_hpartial_differentiable`12_in u means :
Def4:
ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
y0 st
(
N c= dom (SVF1 2,(pdiff1 f,1),u) & ex
L being
LINEAR ex
R being
REST st
for
y being
Real st
y in N holds
((SVF1 2,(pdiff1 f,1),u) . y) - ((SVF1 2,(pdiff1 f,1),u) . y0) = (L . (y - y0)) + (R . (y - y0)) ) );
pred f is_hpartial_differentiable`13_in u means :
Def4ForZ:
ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
z0 st
(
N c= dom (SVF1 3,(pdiff1 f,1),u) & ex
L being
LINEAR ex
R being
REST st
for
z being
Real st
z in N holds
((SVF1 3,(pdiff1 f,1),u) . z) - ((SVF1 3,(pdiff1 f,1),u) . z0) = (L . (z - z0)) + (R . (z - z0)) ) );
pred f is_hpartial_differentiable`21_in u means :
Def5:
ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
x0 st
(
N c= dom (SVF1 1,(pdiff1 f,2),u) & ex
L being
LINEAR ex
R being
REST st
for
x being
Real st
x in N holds
((SVF1 1,(pdiff1 f,2),u) . x) - ((SVF1 1,(pdiff1 f,2),u) . x0) = (L . (x - x0)) + (R . (x - x0)) ) );
pred f is_hpartial_differentiable`22_in u means :
Def6:
ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
y0 st
(
N c= dom (SVF1 2,(pdiff1 f,2),u) & ex
L being
LINEAR ex
R being
REST st
for
y being
Real st
y in N holds
((SVF1 2,(pdiff1 f,2),u) . y) - ((SVF1 2,(pdiff1 f,2),u) . y0) = (L . (y - y0)) + (R . (y - y0)) ) );
pred f is_hpartial_differentiable`23_in u means :
Def6ForZ:
ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
z0 st
(
N c= dom (SVF1 3,(pdiff1 f,2),u) & ex
L being
LINEAR ex
R being
REST st
for
z being
Real st
z in N holds
((SVF1 3,(pdiff1 f,2),u) . z) - ((SVF1 3,(pdiff1 f,2),u) . z0) = (L . (z - z0)) + (R . (z - z0)) ) );
pred f is_hpartial_differentiable`31_in u means :
Def5ForSecondOrder:
ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
x0 st
(
N c= dom (SVF1 1,(pdiff1 f,3),u) & ex
L being
LINEAR ex
R being
REST st
for
x being
Real st
x in N holds
((SVF1 1,(pdiff1 f,3),u) . x) - ((SVF1 1,(pdiff1 f,3),u) . x0) = (L . (x - x0)) + (R . (x - x0)) ) );
pred f is_hpartial_differentiable`32_in u means :
Def6ForSecondOrder:
ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
y0 st
(
N c= dom (SVF1 2,(pdiff1 f,3),u) & ex
L being
LINEAR ex
R being
REST st
for
y being
Real st
y in N holds
((SVF1 2,(pdiff1 f,3),u) . y) - ((SVF1 2,(pdiff1 f,3),u) . y0) = (L . (y - y0)) + (R . (y - y0)) ) );
pred f is_hpartial_differentiable`33_in u means :
Def6ForZForSecondOrder:
ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
z0 st
(
N c= dom (SVF1 3,(pdiff1 f,3),u) & ex
L being
LINEAR ex
R being
REST st
for
z being
Real st
z in N holds
((SVF1 3,(pdiff1 f,3),u) . z) - ((SVF1 3,(pdiff1 f,3),u) . z0) = (L . (z - z0)) + (R . (z - z0)) ) );
end;
:: deftheorem Def3 defines is_hpartial_differentiable`11_in PDIFF_5:def 1 :
for
f being
PartFunc of
(REAL 3),
REAL for
u being
Element of
REAL 3 holds
(
f is_hpartial_differentiable`11_in u iff ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
x0 st
(
N c= dom (SVF1 1,(pdiff1 f,1),u) & ex
L being
LINEAR ex
R being
REST st
for
x being
Real st
x in N holds
((SVF1 1,(pdiff1 f,1),u) . x) - ((SVF1 1,(pdiff1 f,1),u) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) );
:: deftheorem Def4 defines is_hpartial_differentiable`12_in PDIFF_5:def 2 :
for
f being
PartFunc of
(REAL 3),
REAL for
u being
Element of
REAL 3 holds
(
f is_hpartial_differentiable`12_in u iff ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
y0 st
(
N c= dom (SVF1 2,(pdiff1 f,1),u) & ex
L being
LINEAR ex
R being
REST st
for
y being
Real st
y in N holds
((SVF1 2,(pdiff1 f,1),u) . y) - ((SVF1 2,(pdiff1 f,1),u) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) );
:: deftheorem Def4ForZ defines is_hpartial_differentiable`13_in PDIFF_5:def 3 :
for
f being
PartFunc of
(REAL 3),
REAL for
u being
Element of
REAL 3 holds
(
f is_hpartial_differentiable`13_in u iff ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
z0 st
(
N c= dom (SVF1 3,(pdiff1 f,1),u) & ex
L being
LINEAR ex
R being
REST st
for
z being
Real st
z in N holds
((SVF1 3,(pdiff1 f,1),u) . z) - ((SVF1 3,(pdiff1 f,1),u) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) );
:: deftheorem Def5 defines is_hpartial_differentiable`21_in PDIFF_5:def 4 :
for
f being
PartFunc of
(REAL 3),
REAL for
u being
Element of
REAL 3 holds
(
f is_hpartial_differentiable`21_in u iff ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
x0 st
(
N c= dom (SVF1 1,(pdiff1 f,2),u) & ex
L being
LINEAR ex
R being
REST st
for
x being
Real st
x in N holds
((SVF1 1,(pdiff1 f,2),u) . x) - ((SVF1 1,(pdiff1 f,2),u) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) );
:: deftheorem Def6 defines is_hpartial_differentiable`22_in PDIFF_5:def 5 :
for
f being
PartFunc of
(REAL 3),
REAL for
u being
Element of
REAL 3 holds
(
f is_hpartial_differentiable`22_in u iff ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
y0 st
(
N c= dom (SVF1 2,(pdiff1 f,2),u) & ex
L being
LINEAR ex
R being
REST st
for
y being
Real st
y in N holds
((SVF1 2,(pdiff1 f,2),u) . y) - ((SVF1 2,(pdiff1 f,2),u) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) );
:: deftheorem Def6ForZ defines is_hpartial_differentiable`23_in PDIFF_5:def 6 :
for
f being
PartFunc of
(REAL 3),
REAL for
u being
Element of
REAL 3 holds
(
f is_hpartial_differentiable`23_in u iff ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
z0 st
(
N c= dom (SVF1 3,(pdiff1 f,2),u) & ex
L being
LINEAR ex
R being
REST st
for
z being
Real st
z in N holds
((SVF1 3,(pdiff1 f,2),u) . z) - ((SVF1 3,(pdiff1 f,2),u) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) );
:: deftheorem Def5ForSecondOrder defines is_hpartial_differentiable`31_in PDIFF_5:def 7 :
for
f being
PartFunc of
(REAL 3),
REAL for
u being
Element of
REAL 3 holds
(
f is_hpartial_differentiable`31_in u iff ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
x0 st
(
N c= dom (SVF1 1,(pdiff1 f,3),u) & ex
L being
LINEAR ex
R being
REST st
for
x being
Real st
x in N holds
((SVF1 1,(pdiff1 f,3),u) . x) - ((SVF1 1,(pdiff1 f,3),u) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) );
:: deftheorem Def6ForSecondOrder defines is_hpartial_differentiable`32_in PDIFF_5:def 8 :
for
f being
PartFunc of
(REAL 3),
REAL for
u being
Element of
REAL 3 holds
(
f is_hpartial_differentiable`32_in u iff ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
y0 st
(
N c= dom (SVF1 2,(pdiff1 f,3),u) & ex
L being
LINEAR ex
R being
REST st
for
y being
Real st
y in N holds
((SVF1 2,(pdiff1 f,3),u) . y) - ((SVF1 2,(pdiff1 f,3),u) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) );
:: deftheorem Def6ForZForSecondOrder defines is_hpartial_differentiable`33_in PDIFF_5:def 9 :
for
f being
PartFunc of
(REAL 3),
REAL for
u being
Element of
REAL 3 holds
(
f is_hpartial_differentiable`33_in u iff ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
z0 st
(
N c= dom (SVF1 3,(pdiff1 f,3),u) & ex
L being
LINEAR ex
R being
REST st
for
z being
Real st
z in N holds
((SVF1 3,(pdiff1 f,3),u) . z) - ((SVF1 3,(pdiff1 f,3),u) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) );
definition
let f be
PartFunc of
(REAL 3),
REAL ;
let u be
Element of
REAL 3;
assume A1:
f is_hpartial_differentiable`11_in u
;
func hpartdiff11 f,
u -> Real means :
Def7:
ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
x0 st
(
N c= dom (SVF1 1,(pdiff1 f,1),u) & ex
L being
LINEAR ex
R being
REST st
(
it = L . 1 & ( for
x being
Real st
x in N holds
((SVF1 1,(pdiff1 f,1),u) . x) - ((SVF1 1,(pdiff1 f,1),u) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) );
existence
ex b1, x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 1,(pdiff1 f,1),u) & ex L being LINEAR ex R being REST st
( b1 = L . 1 & ( for x being Real st x in N holds
((SVF1 1,(pdiff1 f,1),u) . x) - ((SVF1 1,(pdiff1 f,1),u) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) )
uniqueness
for b1, b2 being Real st ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 1,(pdiff1 f,1),u) & ex L being LINEAR ex R being REST st
( b1 = L . 1 & ( for x being Real st x in N holds
((SVF1 1,(pdiff1 f,1),u) . x) - ((SVF1 1,(pdiff1 f,1),u) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) & ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 1,(pdiff1 f,1),u) & ex L being LINEAR ex R being REST st
( b2 = L . 1 & ( for x being Real st x in N holds
((SVF1 1,(pdiff1 f,1),u) . x) - ((SVF1 1,(pdiff1 f,1),u) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def7 defines hpartdiff11 PDIFF_5:def 10 :
for
f being
PartFunc of
(REAL 3),
REAL for
u being
Element of
REAL 3 st
f is_hpartial_differentiable`11_in u holds
for
b3 being
Real holds
(
b3 = hpartdiff11 f,
u iff ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
x0 st
(
N c= dom (SVF1 1,(pdiff1 f,1),u) & ex
L being
LINEAR ex
R being
REST st
(
b3 = L . 1 & ( for
x being
Real st
x in N holds
((SVF1 1,(pdiff1 f,1),u) . x) - ((SVF1 1,(pdiff1 f,1),u) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) );
definition
let f be
PartFunc of
(REAL 3),
REAL ;
let u be
Element of
REAL 3;
assume A1:
f is_hpartial_differentiable`12_in u
;
func hpartdiff12 f,
u -> Real means :
Def8:
ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
y0 st
(
N c= dom (SVF1 2,(pdiff1 f,1),u) & ex
L being
LINEAR ex
R being
REST st
(
it = L . 1 & ( for
y being
Real st
y in N holds
((SVF1 2,(pdiff1 f,1),u) . y) - ((SVF1 2,(pdiff1 f,1),u) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) );
existence
ex b1, x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 2,(pdiff1 f,1),u) & ex L being LINEAR ex R being REST st
( b1 = L . 1 & ( for y being Real st y in N holds
((SVF1 2,(pdiff1 f,1),u) . y) - ((SVF1 2,(pdiff1 f,1),u) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) )
uniqueness
for b1, b2 being Real st ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 2,(pdiff1 f,1),u) & ex L being LINEAR ex R being REST st
( b1 = L . 1 & ( for y being Real st y in N holds
((SVF1 2,(pdiff1 f,1),u) . y) - ((SVF1 2,(pdiff1 f,1),u) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) & ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 2,(pdiff1 f,1),u) & ex L being LINEAR ex R being REST st
( b2 = L . 1 & ( for y being Real st y in N holds
((SVF1 2,(pdiff1 f,1),u) . y) - ((SVF1 2,(pdiff1 f,1),u) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def8 defines hpartdiff12 PDIFF_5:def 11 :
for
f being
PartFunc of
(REAL 3),
REAL for
u being
Element of
REAL 3 st
f is_hpartial_differentiable`12_in u holds
for
b3 being
Real holds
(
b3 = hpartdiff12 f,
u iff ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
y0 st
(
N c= dom (SVF1 2,(pdiff1 f,1),u) & ex
L being
LINEAR ex
R being
REST st
(
b3 = L . 1 & ( for
y being
Real st
y in N holds
((SVF1 2,(pdiff1 f,1),u) . y) - ((SVF1 2,(pdiff1 f,1),u) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) );
definition
let f be
PartFunc of
(REAL 3),
REAL ;
let u be
Element of
REAL 3;
assume A1:
f is_hpartial_differentiable`13_in u
;
func hpartdiff13 f,
u -> Real means :
Def8ForZ:
ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
z0 st
(
N c= dom (SVF1 3,(pdiff1 f,1),u) & ex
L being
LINEAR ex
R being
REST st
(
it = L . 1 & ( for
z being
Real st
z in N holds
((SVF1 3,(pdiff1 f,1),u) . z) - ((SVF1 3,(pdiff1 f,1),u) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) );
existence
ex b1, x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 3,(pdiff1 f,1),u) & ex L being LINEAR ex R being REST st
( b1 = L . 1 & ( for z being Real st z in N holds
((SVF1 3,(pdiff1 f,1),u) . z) - ((SVF1 3,(pdiff1 f,1),u) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) )
uniqueness
for b1, b2 being Real st ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 3,(pdiff1 f,1),u) & ex L being LINEAR ex R being REST st
( b1 = L . 1 & ( for z being Real st z in N holds
((SVF1 3,(pdiff1 f,1),u) . z) - ((SVF1 3,(pdiff1 f,1),u) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) & ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 3,(pdiff1 f,1),u) & ex L being LINEAR ex R being REST st
( b2 = L . 1 & ( for z being Real st z in N holds
((SVF1 3,(pdiff1 f,1),u) . z) - ((SVF1 3,(pdiff1 f,1),u) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def8ForZ defines hpartdiff13 PDIFF_5:def 12 :
for
f being
PartFunc of
(REAL 3),
REAL for
u being
Element of
REAL 3 st
f is_hpartial_differentiable`13_in u holds
for
b3 being
Real holds
(
b3 = hpartdiff13 f,
u iff ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
z0 st
(
N c= dom (SVF1 3,(pdiff1 f,1),u) & ex
L being
LINEAR ex
R being
REST st
(
b3 = L . 1 & ( for
z being
Real st
z in N holds
((SVF1 3,(pdiff1 f,1),u) . z) - ((SVF1 3,(pdiff1 f,1),u) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) );
definition
let f be
PartFunc of
(REAL 3),
REAL ;
let u be
Element of
REAL 3;
assume A1:
f is_hpartial_differentiable`21_in u
;
func hpartdiff21 f,
u -> Real means :
Def9:
ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
x0 st
(
N c= dom (SVF1 1,(pdiff1 f,2),u) & ex
L being
LINEAR ex
R being
REST st
(
it = L . 1 & ( for
x being
Real st
x in N holds
((SVF1 1,(pdiff1 f,2),u) . x) - ((SVF1 1,(pdiff1 f,2),u) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) );
existence
ex b1, x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 1,(pdiff1 f,2),u) & ex L being LINEAR ex R being REST st
( b1 = L . 1 & ( for x being Real st x in N holds
((SVF1 1,(pdiff1 f,2),u) . x) - ((SVF1 1,(pdiff1 f,2),u) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) )
uniqueness
for b1, b2 being Real st ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 1,(pdiff1 f,2),u) & ex L being LINEAR ex R being REST st
( b1 = L . 1 & ( for x being Real st x in N holds
((SVF1 1,(pdiff1 f,2),u) . x) - ((SVF1 1,(pdiff1 f,2),u) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) & ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 1,(pdiff1 f,2),u) & ex L being LINEAR ex R being REST st
( b2 = L . 1 & ( for x being Real st x in N holds
((SVF1 1,(pdiff1 f,2),u) . x) - ((SVF1 1,(pdiff1 f,2),u) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def9 defines hpartdiff21 PDIFF_5:def 13 :
for
f being
PartFunc of
(REAL 3),
REAL for
u being
Element of
REAL 3 st
f is_hpartial_differentiable`21_in u holds
for
b3 being
Real holds
(
b3 = hpartdiff21 f,
u iff ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
x0 st
(
N c= dom (SVF1 1,(pdiff1 f,2),u) & ex
L being
LINEAR ex
R being
REST st
(
b3 = L . 1 & ( for
x being
Real st
x in N holds
((SVF1 1,(pdiff1 f,2),u) . x) - ((SVF1 1,(pdiff1 f,2),u) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) );
definition
let f be
PartFunc of
(REAL 3),
REAL ;
let u be
Element of
REAL 3;
assume A1:
f is_hpartial_differentiable`22_in u
;
func hpartdiff22 f,
u -> Real means :
Def10:
ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
y0 st
(
N c= dom (SVF1 2,(pdiff1 f,2),u) & ex
L being
LINEAR ex
R being
REST st
(
it = L . 1 & ( for
y being
Real st
y in N holds
((SVF1 2,(pdiff1 f,2),u) . y) - ((SVF1 2,(pdiff1 f,2),u) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) );
existence
ex b1, x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 2,(pdiff1 f,2),u) & ex L being LINEAR ex R being REST st
( b1 = L . 1 & ( for y being Real st y in N holds
((SVF1 2,(pdiff1 f,2),u) . y) - ((SVF1 2,(pdiff1 f,2),u) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) )
uniqueness
for b1, b2 being Real st ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 2,(pdiff1 f,2),u) & ex L being LINEAR ex R being REST st
( b1 = L . 1 & ( for y being Real st y in N holds
((SVF1 2,(pdiff1 f,2),u) . y) - ((SVF1 2,(pdiff1 f,2),u) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) & ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 2,(pdiff1 f,2),u) & ex L being LINEAR ex R being REST st
( b2 = L . 1 & ( for y being Real st y in N holds
((SVF1 2,(pdiff1 f,2),u) . y) - ((SVF1 2,(pdiff1 f,2),u) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def10 defines hpartdiff22 PDIFF_5:def 14 :
for
f being
PartFunc of
(REAL 3),
REAL for
u being
Element of
REAL 3 st
f is_hpartial_differentiable`22_in u holds
for
b3 being
Real holds
(
b3 = hpartdiff22 f,
u iff ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
y0 st
(
N c= dom (SVF1 2,(pdiff1 f,2),u) & ex
L being
LINEAR ex
R being
REST st
(
b3 = L . 1 & ( for
y being
Real st
y in N holds
((SVF1 2,(pdiff1 f,2),u) . y) - ((SVF1 2,(pdiff1 f,2),u) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) );
definition
let f be
PartFunc of
(REAL 3),
REAL ;
let u be
Element of
REAL 3;
assume A1:
f is_hpartial_differentiable`23_in u
;
func hpartdiff23 f,
u -> Real means :
Def10ForZ:
ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
z0 st
(
N c= dom (SVF1 3,(pdiff1 f,2),u) & ex
L being
LINEAR ex
R being
REST st
(
it = L . 1 & ( for
z being
Real st
z in N holds
((SVF1 3,(pdiff1 f,2),u) . z) - ((SVF1 3,(pdiff1 f,2),u) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) );
existence
ex b1, x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 3,(pdiff1 f,2),u) & ex L being LINEAR ex R being REST st
( b1 = L . 1 & ( for z being Real st z in N holds
((SVF1 3,(pdiff1 f,2),u) . z) - ((SVF1 3,(pdiff1 f,2),u) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) )
uniqueness
for b1, b2 being Real st ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 3,(pdiff1 f,2),u) & ex L being LINEAR ex R being REST st
( b1 = L . 1 & ( for z being Real st z in N holds
((SVF1 3,(pdiff1 f,2),u) . z) - ((SVF1 3,(pdiff1 f,2),u) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) & ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 3,(pdiff1 f,2),u) & ex L being LINEAR ex R being REST st
( b2 = L . 1 & ( for z being Real st z in N holds
((SVF1 3,(pdiff1 f,2),u) . z) - ((SVF1 3,(pdiff1 f,2),u) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def10ForZ defines hpartdiff23 PDIFF_5:def 15 :
for
f being
PartFunc of
(REAL 3),
REAL for
u being
Element of
REAL 3 st
f is_hpartial_differentiable`23_in u holds
for
b3 being
Real holds
(
b3 = hpartdiff23 f,
u iff ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
z0 st
(
N c= dom (SVF1 3,(pdiff1 f,2),u) & ex
L being
LINEAR ex
R being
REST st
(
b3 = L . 1 & ( for
z being
Real st
z in N holds
((SVF1 3,(pdiff1 f,2),u) . z) - ((SVF1 3,(pdiff1 f,2),u) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) );
definition
let f be
PartFunc of
(REAL 3),
REAL ;
let u be
Element of
REAL 3;
assume A1:
f is_hpartial_differentiable`31_in u
;
func hpartdiff31 f,
u -> Real means :
Def9ForSecondOrder:
ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
x0 st
(
N c= dom (SVF1 1,(pdiff1 f,3),u) & ex
L being
LINEAR ex
R being
REST st
(
it = L . 1 & ( for
x being
Real st
x in N holds
((SVF1 1,(pdiff1 f,3),u) . x) - ((SVF1 1,(pdiff1 f,3),u) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) );
existence
ex b1, x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 1,(pdiff1 f,3),u) & ex L being LINEAR ex R being REST st
( b1 = L . 1 & ( for x being Real st x in N holds
((SVF1 1,(pdiff1 f,3),u) . x) - ((SVF1 1,(pdiff1 f,3),u) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) )
uniqueness
for b1, b2 being Real st ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 1,(pdiff1 f,3),u) & ex L being LINEAR ex R being REST st
( b1 = L . 1 & ( for x being Real st x in N holds
((SVF1 1,(pdiff1 f,3),u) . x) - ((SVF1 1,(pdiff1 f,3),u) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) & ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 1,(pdiff1 f,3),u) & ex L being LINEAR ex R being REST st
( b2 = L . 1 & ( for x being Real st x in N holds
((SVF1 1,(pdiff1 f,3),u) . x) - ((SVF1 1,(pdiff1 f,3),u) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def9ForSecondOrder defines hpartdiff31 PDIFF_5:def 16 :
for
f being
PartFunc of
(REAL 3),
REAL for
u being
Element of
REAL 3 st
f is_hpartial_differentiable`31_in u holds
for
b3 being
Real holds
(
b3 = hpartdiff31 f,
u iff ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
x0 st
(
N c= dom (SVF1 1,(pdiff1 f,3),u) & ex
L being
LINEAR ex
R being
REST st
(
b3 = L . 1 & ( for
x being
Real st
x in N holds
((SVF1 1,(pdiff1 f,3),u) . x) - ((SVF1 1,(pdiff1 f,3),u) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) );
definition
let f be
PartFunc of
(REAL 3),
REAL ;
let u be
Element of
REAL 3;
assume A1:
f is_hpartial_differentiable`32_in u
;
func hpartdiff32 f,
u -> Real means :
Def10ForSecondOrder:
ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
y0 st
(
N c= dom (SVF1 2,(pdiff1 f,3),u) & ex
L being
LINEAR ex
R being
REST st
(
it = L . 1 & ( for
y being
Real st
y in N holds
((SVF1 2,(pdiff1 f,3),u) . y) - ((SVF1 2,(pdiff1 f,3),u) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) );
existence
ex b1, x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 2,(pdiff1 f,3),u) & ex L being LINEAR ex R being REST st
( b1 = L . 1 & ( for y being Real st y in N holds
((SVF1 2,(pdiff1 f,3),u) . y) - ((SVF1 2,(pdiff1 f,3),u) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) )
uniqueness
for b1, b2 being Real st ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 2,(pdiff1 f,3),u) & ex L being LINEAR ex R being REST st
( b1 = L . 1 & ( for y being Real st y in N holds
((SVF1 2,(pdiff1 f,3),u) . y) - ((SVF1 2,(pdiff1 f,3),u) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) & ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 2,(pdiff1 f,3),u) & ex L being LINEAR ex R being REST st
( b2 = L . 1 & ( for y being Real st y in N holds
((SVF1 2,(pdiff1 f,3),u) . y) - ((SVF1 2,(pdiff1 f,3),u) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def10ForSecondOrder defines hpartdiff32 PDIFF_5:def 17 :
for
f being
PartFunc of
(REAL 3),
REAL for
u being
Element of
REAL 3 st
f is_hpartial_differentiable`32_in u holds
for
b3 being
Real holds
(
b3 = hpartdiff32 f,
u iff ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
y0 st
(
N c= dom (SVF1 2,(pdiff1 f,3),u) & ex
L being
LINEAR ex
R being
REST st
(
b3 = L . 1 & ( for
y being
Real st
y in N holds
((SVF1 2,(pdiff1 f,3),u) . y) - ((SVF1 2,(pdiff1 f,3),u) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) );
definition
let f be
PartFunc of
(REAL 3),
REAL ;
let u be
Element of
REAL 3;
assume A1:
f is_hpartial_differentiable`33_in u
;
func hpartdiff33 f,
u -> Real means :
Def10ForZForSecondOrder:
ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
z0 st
(
N c= dom (SVF1 3,(pdiff1 f,3),u) & ex
L being
LINEAR ex
R being
REST st
(
it = L . 1 & ( for
z being
Real st
z in N holds
((SVF1 3,(pdiff1 f,3),u) . z) - ((SVF1 3,(pdiff1 f,3),u) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) );
existence
ex b1, x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 3,(pdiff1 f,3),u) & ex L being LINEAR ex R being REST st
( b1 = L . 1 & ( for z being Real st z in N holds
((SVF1 3,(pdiff1 f,3),u) . z) - ((SVF1 3,(pdiff1 f,3),u) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) )
uniqueness
for b1, b2 being Real st ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 3,(pdiff1 f,3),u) & ex L being LINEAR ex R being REST st
( b1 = L . 1 & ( for z being Real st z in N holds
((SVF1 3,(pdiff1 f,3),u) . z) - ((SVF1 3,(pdiff1 f,3),u) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) & ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 3,(pdiff1 f,3),u) & ex L being LINEAR ex R being REST st
( b2 = L . 1 & ( for z being Real st z in N holds
((SVF1 3,(pdiff1 f,3),u) . z) - ((SVF1 3,(pdiff1 f,3),u) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def10ForZForSecondOrder defines hpartdiff33 PDIFF_5:def 18 :
for
f being
PartFunc of
(REAL 3),
REAL for
u being
Element of
REAL 3 st
f is_hpartial_differentiable`33_in u holds
for
b3 being
Real holds
(
b3 = hpartdiff33 f,
u iff ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
z0 st
(
N c= dom (SVF1 3,(pdiff1 f,3),u) & ex
L being
LINEAR ex
R being
REST st
(
b3 = L . 1 & ( for
z being
Real st
z in N holds
((SVF1 3,(pdiff1 f,3),u) . z) - ((SVF1 3,(pdiff1 f,3),u) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) );
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th5:
for
x0,
y0,
z0 being
Real for
u being
Element of
REAL 3
for
f being
PartFunc of
(REAL 3),
REAL st
u = <*x0,y0,z0*> &
f is_hpartial_differentiable`11_in u holds
hpartdiff11 f,
u = diff (SVF1 1,(pdiff1 f,1),u),
x0
theorem Th6:
for
x0,
y0,
z0 being
Real for
u being
Element of
REAL 3
for
f being
PartFunc of
(REAL 3),
REAL st
u = <*x0,y0,z0*> &
f is_hpartial_differentiable`12_in u holds
hpartdiff12 f,
u = diff (SVF1 2,(pdiff1 f,1),u),
y0
theorem Th6ForZ:
for
x0,
y0,
z0 being
Real for
u being
Element of
REAL 3
for
f being
PartFunc of
(REAL 3),
REAL st
u = <*x0,y0,z0*> &
f is_hpartial_differentiable`13_in u holds
hpartdiff13 f,
u = diff (SVF1 3,(pdiff1 f,1),u),
z0
theorem Th7:
for
x0,
y0,
z0 being
Real for
u being
Element of
REAL 3
for
f being
PartFunc of
(REAL 3),
REAL st
u = <*x0,y0,z0*> &
f is_hpartial_differentiable`21_in u holds
hpartdiff21 f,
u = diff (SVF1 1,(pdiff1 f,2),u),
x0
theorem Th8:
for
x0,
y0,
z0 being
Real for
u being
Element of
REAL 3
for
f being
PartFunc of
(REAL 3),
REAL st
u = <*x0,y0,z0*> &
f is_hpartial_differentiable`22_in u holds
hpartdiff22 f,
u = diff (SVF1 2,(pdiff1 f,2),u),
y0
theorem Th8ForZ:
for
x0,
y0,
z0 being
Real for
u being
Element of
REAL 3
for
f being
PartFunc of
(REAL 3),
REAL st
u = <*x0,y0,z0*> &
f is_hpartial_differentiable`23_in u holds
hpartdiff23 f,
u = diff (SVF1 3,(pdiff1 f,2),u),
z0
theorem Th7ForSecondOrder:
for
x0,
y0,
z0 being
Real for
u being
Element of
REAL 3
for
f being
PartFunc of
(REAL 3),
REAL st
u = <*x0,y0,z0*> &
f is_hpartial_differentiable`31_in u holds
hpartdiff31 f,
u = diff (SVF1 1,(pdiff1 f,3),u),
x0
theorem Th8ForSecondOrder:
for
x0,
y0,
z0 being
Real for
u being
Element of
REAL 3
for
f being
PartFunc of
(REAL 3),
REAL st
u = <*x0,y0,z0*> &
f is_hpartial_differentiable`32_in u holds
hpartdiff32 f,
u = diff (SVF1 2,(pdiff1 f,3),u),
y0
theorem Th8ForZForSecondOrder:
for
x0,
y0,
z0 being
Real for
u being
Element of
REAL 3
for
f being
PartFunc of
(REAL 3),
REAL st
u = <*x0,y0,z0*> &
f is_hpartial_differentiable`33_in u holds
hpartdiff33 f,
u = diff (SVF1 3,(pdiff1 f,3),u),
z0
:: deftheorem Def11 defines is_hpartial_differentiable`11_on PDIFF_5:def 19 :
:: deftheorem Def12 defines is_hpartial_differentiable`12_on PDIFF_5:def 20 :
:: deftheorem Def12ForZ defines is_hpartial_differentiable`13_on PDIFF_5:def 21 :
:: deftheorem Def13 defines is_hpartial_differentiable`21_on PDIFF_5:def 22 :
:: deftheorem Def14 defines is_hpartial_differentiable`22_on PDIFF_5:def 23 :
:: deftheorem Def14ForZ defines is_hpartial_differentiable`23_on PDIFF_5:def 24 :
:: deftheorem Def13ForSecondOrder defines is_hpartial_differentiable`31_on PDIFF_5:def 25 :
:: deftheorem Def14ForSecondOrder defines is_hpartial_differentiable`32_on PDIFF_5:def 26 :
:: deftheorem Def14ForZForSecondOrder defines is_hpartial_differentiable`33_on PDIFF_5:def 27 :
:: deftheorem defines `hpartial11| PDIFF_5:def 28 :
:: deftheorem defines `hpartial12| PDIFF_5:def 29 :
:: deftheorem defines `hpartial13| PDIFF_5:def 30 :
:: deftheorem defines `hpartial21| PDIFF_5:def 31 :
:: deftheorem defines `hpartial22| PDIFF_5:def 32 :
:: deftheorem defines `hpartial23| PDIFF_5:def 33 :
:: deftheorem defines `hpartial31| PDIFF_5:def 34 :
:: deftheorem defines `hpartial32| PDIFF_5:def 35 :
:: deftheorem defines `hpartial33| PDIFF_5:def 36 :
begin
theorem Th9:
theorem Th10:
theorem Th10ForZ:
theorem Th11:
theorem Th12:
theorem Th12ForZ:
theorem Th11ForSecondOrder:
theorem Th12ForSecondOrder:
theorem Th12ForZForSecondOrder:
theorem Th17:
theorem Th18:
theorem Th18ForZ:
theorem Th19:
theorem Th20:
theorem Th20ForZ:
theorem Th19ForSecondOrder:
theorem Th20ForSecondOrder:
theorem Th20ForZForSecondOrder:
theorem
for
f being
PartFunc of
(REAL 3),
REAL for
u0 being
Element of
REAL 3
for
N being
Neighbourhood of
(proj 1,3) . u0 st
f is_hpartial_differentiable`11_in u0 &
N c= dom (SVF1 1,(pdiff1 f,1),u0) holds
for
h being
convergent_to_0 Real_Sequence for
c being
V8()
Real_Sequence st
rng c = {((proj 1,3) . u0)} &
rng (h + c) c= N holds
(
(h " ) (#) (((SVF1 1,(pdiff1 f,1),u0) /* (h + c)) - ((SVF1 1,(pdiff1 f,1),u0) /* c)) is
convergent &
hpartdiff11 f,
u0 = lim ((h " ) (#) (((SVF1 1,(pdiff1 f,1),u0) /* (h + c)) - ((SVF1 1,(pdiff1 f,1),u0) /* c))) )
theorem
for
f being
PartFunc of
(REAL 3),
REAL for
u0 being
Element of
REAL 3
for
N being
Neighbourhood of
(proj 2,3) . u0 st
f is_hpartial_differentiable`12_in u0 &
N c= dom (SVF1 2,(pdiff1 f,1),u0) holds
for
h being
convergent_to_0 Real_Sequence for
c being
V8()
Real_Sequence st
rng c = {((proj 2,3) . u0)} &
rng (h + c) c= N holds
(
(h " ) (#) (((SVF1 2,(pdiff1 f,1),u0) /* (h + c)) - ((SVF1 2,(pdiff1 f,1),u0) /* c)) is
convergent &
hpartdiff12 f,
u0 = lim ((h " ) (#) (((SVF1 2,(pdiff1 f,1),u0) /* (h + c)) - ((SVF1 2,(pdiff1 f,1),u0) /* c))) )
theorem
for
f being
PartFunc of
(REAL 3),
REAL for
u0 being
Element of
REAL 3
for
N being
Neighbourhood of
(proj 3,3) . u0 st
f is_hpartial_differentiable`13_in u0 &
N c= dom (SVF1 3,(pdiff1 f,1),u0) holds
for
h being
convergent_to_0 Real_Sequence for
c being
V8()
Real_Sequence st
rng c = {((proj 3,3) . u0)} &
rng (h + c) c= N holds
(
(h " ) (#) (((SVF1 3,(pdiff1 f,1),u0) /* (h + c)) - ((SVF1 3,(pdiff1 f,1),u0) /* c)) is
convergent &
hpartdiff13 f,
u0 = lim ((h " ) (#) (((SVF1 3,(pdiff1 f,1),u0) /* (h + c)) - ((SVF1 3,(pdiff1 f,1),u0) /* c))) )
theorem
for
f being
PartFunc of
(REAL 3),
REAL for
u0 being
Element of
REAL 3
for
N being
Neighbourhood of
(proj 1,3) . u0 st
f is_hpartial_differentiable`21_in u0 &
N c= dom (SVF1 1,(pdiff1 f,2),u0) holds
for
h being
convergent_to_0 Real_Sequence for
c being
V8()
Real_Sequence st
rng c = {((proj 1,3) . u0)} &
rng (h + c) c= N holds
(
(h " ) (#) (((SVF1 1,(pdiff1 f,2),u0) /* (h + c)) - ((SVF1 1,(pdiff1 f,2),u0) /* c)) is
convergent &
hpartdiff21 f,
u0 = lim ((h " ) (#) (((SVF1 1,(pdiff1 f,2),u0) /* (h + c)) - ((SVF1 1,(pdiff1 f,2),u0) /* c))) )
theorem
for
f being
PartFunc of
(REAL 3),
REAL for
u0 being
Element of
REAL 3
for
N being
Neighbourhood of
(proj 2,3) . u0 st
f is_hpartial_differentiable`22_in u0 &
N c= dom (SVF1 2,(pdiff1 f,2),u0) holds
for
h being
convergent_to_0 Real_Sequence for
c being
V8()
Real_Sequence st
rng c = {((proj 2,3) . u0)} &
rng (h + c) c= N holds
(
(h " ) (#) (((SVF1 2,(pdiff1 f,2),u0) /* (h + c)) - ((SVF1 2,(pdiff1 f,2),u0) /* c)) is
convergent &
hpartdiff22 f,
u0 = lim ((h " ) (#) (((SVF1 2,(pdiff1 f,2),u0) /* (h + c)) - ((SVF1 2,(pdiff1 f,2),u0) /* c))) )
theorem
for
f being
PartFunc of
(REAL 3),
REAL for
u0 being
Element of
REAL 3
for
N being
Neighbourhood of
(proj 3,3) . u0 st
f is_hpartial_differentiable`23_in u0 &
N c= dom (SVF1 3,(pdiff1 f,2),u0) holds
for
h being
convergent_to_0 Real_Sequence for
c being
V8()
Real_Sequence st
rng c = {((proj 3,3) . u0)} &
rng (h + c) c= N holds
(
(h " ) (#) (((SVF1 3,(pdiff1 f,2),u0) /* (h + c)) - ((SVF1 3,(pdiff1 f,2),u0) /* c)) is
convergent &
hpartdiff23 f,
u0 = lim ((h " ) (#) (((SVF1 3,(pdiff1 f,2),u0) /* (h + c)) - ((SVF1 3,(pdiff1 f,2),u0) /* c))) )
theorem
for
f being
PartFunc of
(REAL 3),
REAL for
u0 being
Element of
REAL 3
for
N being
Neighbourhood of
(proj 1,3) . u0 st
f is_hpartial_differentiable`31_in u0 &
N c= dom (SVF1 1,(pdiff1 f,3),u0) holds
for
h being
convergent_to_0 Real_Sequence for
c being
V8()
Real_Sequence st
rng c = {((proj 1,3) . u0)} &
rng (h + c) c= N holds
(
(h " ) (#) (((SVF1 1,(pdiff1 f,3),u0) /* (h + c)) - ((SVF1 1,(pdiff1 f,3),u0) /* c)) is
convergent &
hpartdiff31 f,
u0 = lim ((h " ) (#) (((SVF1 1,(pdiff1 f,3),u0) /* (h + c)) - ((SVF1 1,(pdiff1 f,3),u0) /* c))) )
theorem
for
f being
PartFunc of
(REAL 3),
REAL for
u0 being
Element of
REAL 3
for
N being
Neighbourhood of
(proj 2,3) . u0 st
f is_hpartial_differentiable`32_in u0 &
N c= dom (SVF1 2,(pdiff1 f,3),u0) holds
for
h being
convergent_to_0 Real_Sequence for
c being
V8()
Real_Sequence st
rng c = {((proj 2,3) . u0)} &
rng (h + c) c= N holds
(
(h " ) (#) (((SVF1 2,(pdiff1 f,3),u0) /* (h + c)) - ((SVF1 2,(pdiff1 f,3),u0) /* c)) is
convergent &
hpartdiff32 f,
u0 = lim ((h " ) (#) (((SVF1 2,(pdiff1 f,3),u0) /* (h + c)) - ((SVF1 2,(pdiff1 f,3),u0) /* c))) )
theorem
for
f being
PartFunc of
(REAL 3),
REAL for
u0 being
Element of
REAL 3
for
N being
Neighbourhood of
(proj 3,3) . u0 st
f is_hpartial_differentiable`33_in u0 &
N c= dom (SVF1 3,(pdiff1 f,3),u0) holds
for
h being
convergent_to_0 Real_Sequence for
c being
V8()
Real_Sequence st
rng c = {((proj 3,3) . u0)} &
rng (h + c) c= N holds
(
(h " ) (#) (((SVF1 3,(pdiff1 f,3),u0) /* (h + c)) - ((SVF1 3,(pdiff1 f,3),u0) /* c)) is
convergent &
hpartdiff33 f,
u0 = lim ((h " ) (#) (((SVF1 3,(pdiff1 f,3),u0) /* (h + c)) - ((SVF1 3,(pdiff1 f,3),u0) /* c))) )
theorem
for
u0 being
Element of
REAL 3
for
f1,
f2 being
PartFunc of
(REAL 3),
REAL st
f1 is_hpartial_differentiable`11_in u0 &
f2 is_hpartial_differentiable`11_in u0 holds
(
(pdiff1 f1,1) + (pdiff1 f2,1) is_partial_differentiable_in u0,1 &
partdiff ((pdiff1 f1,1) + (pdiff1 f2,1)),
u0,1
= (hpartdiff11 f1,u0) + (hpartdiff11 f2,u0) )
theorem
for
u0 being
Element of
REAL 3
for
f1,
f2 being
PartFunc of
(REAL 3),
REAL st
f1 is_hpartial_differentiable`12_in u0 &
f2 is_hpartial_differentiable`12_in u0 holds
(
(pdiff1 f1,1) + (pdiff1 f2,1) is_partial_differentiable_in u0,2 &
partdiff ((pdiff1 f1,1) + (pdiff1 f2,1)),
u0,2
= (hpartdiff12 f1,u0) + (hpartdiff12 f2,u0) )
theorem
for
u0 being
Element of
REAL 3
for
f1,
f2 being
PartFunc of
(REAL 3),
REAL st
f1 is_hpartial_differentiable`13_in u0 &
f2 is_hpartial_differentiable`13_in u0 holds
(
(pdiff1 f1,1) + (pdiff1 f2,1) is_partial_differentiable_in u0,3 &
partdiff ((pdiff1 f1,1) + (pdiff1 f2,1)),
u0,3
= (hpartdiff13 f1,u0) + (hpartdiff13 f2,u0) )
theorem
for
u0 being
Element of
REAL 3
for
f1,
f2 being
PartFunc of
(REAL 3),
REAL st
f1 is_hpartial_differentiable`21_in u0 &
f2 is_hpartial_differentiable`21_in u0 holds
(
(pdiff1 f1,2) + (pdiff1 f2,2) is_partial_differentiable_in u0,1 &
partdiff ((pdiff1 f1,2) + (pdiff1 f2,2)),
u0,1
= (hpartdiff21 f1,u0) + (hpartdiff21 f2,u0) )
theorem
for
u0 being
Element of
REAL 3
for
f1,
f2 being
PartFunc of
(REAL 3),
REAL st
f1 is_hpartial_differentiable`22_in u0 &
f2 is_hpartial_differentiable`22_in u0 holds
(
(pdiff1 f1,2) + (pdiff1 f2,2) is_partial_differentiable_in u0,2 &
partdiff ((pdiff1 f1,2) + (pdiff1 f2,2)),
u0,2
= (hpartdiff22 f1,u0) + (hpartdiff22 f2,u0) )
theorem
for
u0 being
Element of
REAL 3
for
f1,
f2 being
PartFunc of
(REAL 3),
REAL st
f1 is_hpartial_differentiable`23_in u0 &
f2 is_hpartial_differentiable`23_in u0 holds
(
(pdiff1 f1,2) + (pdiff1 f2,2) is_partial_differentiable_in u0,3 &
partdiff ((pdiff1 f1,2) + (pdiff1 f2,2)),
u0,3
= (hpartdiff23 f1,u0) + (hpartdiff23 f2,u0) )
theorem
for
u0 being
Element of
REAL 3
for
f1,
f2 being
PartFunc of
(REAL 3),
REAL st
f1 is_hpartial_differentiable`11_in u0 &
f2 is_hpartial_differentiable`11_in u0 holds
(
(pdiff1 f1,1) - (pdiff1 f2,1) is_partial_differentiable_in u0,1 &
partdiff ((pdiff1 f1,1) - (pdiff1 f2,1)),
u0,1
= (hpartdiff11 f1,u0) - (hpartdiff11 f2,u0) )
theorem
for
u0 being
Element of
REAL 3
for
f1,
f2 being
PartFunc of
(REAL 3),
REAL st
f1 is_hpartial_differentiable`12_in u0 &
f2 is_hpartial_differentiable`12_in u0 holds
(
(pdiff1 f1,1) - (pdiff1 f2,1) is_partial_differentiable_in u0,2 &
partdiff ((pdiff1 f1,1) - (pdiff1 f2,1)),
u0,2
= (hpartdiff12 f1,u0) - (hpartdiff12 f2,u0) )
theorem
for
u0 being
Element of
REAL 3
for
f1,
f2 being
PartFunc of
(REAL 3),
REAL st
f1 is_hpartial_differentiable`13_in u0 &
f2 is_hpartial_differentiable`13_in u0 holds
(
(pdiff1 f1,1) - (pdiff1 f2,1) is_partial_differentiable_in u0,3 &
partdiff ((pdiff1 f1,1) - (pdiff1 f2,1)),
u0,3
= (hpartdiff13 f1,u0) - (hpartdiff13 f2,u0) )
theorem
for
u0 being
Element of
REAL 3
for
f1,
f2 being
PartFunc of
(REAL 3),
REAL st
f1 is_hpartial_differentiable`21_in u0 &
f2 is_hpartial_differentiable`21_in u0 holds
(
(pdiff1 f1,2) - (pdiff1 f2,2) is_partial_differentiable_in u0,1 &
partdiff ((pdiff1 f1,2) - (pdiff1 f2,2)),
u0,1
= (hpartdiff21 f1,u0) - (hpartdiff21 f2,u0) )
theorem
for
u0 being
Element of
REAL 3
for
f1,
f2 being
PartFunc of
(REAL 3),
REAL st
f1 is_hpartial_differentiable`22_in u0 &
f2 is_hpartial_differentiable`22_in u0 holds
(
(pdiff1 f1,2) - (pdiff1 f2,2) is_partial_differentiable_in u0,2 &
partdiff ((pdiff1 f1,2) - (pdiff1 f2,2)),
u0,2
= (hpartdiff22 f1,u0) - (hpartdiff22 f2,u0) )
theorem
for
u0 being
Element of
REAL 3
for
f1,
f2 being
PartFunc of
(REAL 3),
REAL st
f1 is_hpartial_differentiable`23_in u0 &
f2 is_hpartial_differentiable`23_in u0 holds
(
(pdiff1 f1,2) - (pdiff1 f2,2) is_partial_differentiable_in u0,3 &
partdiff ((pdiff1 f1,2) - (pdiff1 f2,2)),
u0,3
= (hpartdiff23 f1,u0) - (hpartdiff23 f2,u0) )
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem