begin
definition
let i be
Element of
NAT ;
let n be non
empty Element of
NAT ;
let f be
PartFunc of ,;
func pdiff1 f,
i -> Function of
REAL n,
REAL means
for
z being
Element of
REAL n holds
it . z = partdiff f,
z,
i;
existence
ex b1 being Function of REAL n, REAL st
for z being Element of REAL n holds b1 . z = partdiff f,z,i
uniqueness
for b1, b2 being Function of REAL n, REAL st ( for z being Element of REAL n holds b1 . z = partdiff f,z,i ) & ( for z being Element of REAL n holds b2 . z = partdiff f,z,i ) holds
b1 = b2
end;
:: deftheorem defines pdiff1 PDIFF_3:def 1 :
definition
let f be
PartFunc of ,;
let z be
Element of
REAL 2;
pred f is_hpartial_differentiable`11_in z means :
Def2:
ex
x0,
y0 being
Real st
(
z = <*x0,y0*> & ex
N being
Neighbourhood of
x0 st
(
N c= dom (SVF1 1,(pdiff1 f,1),z) & ex
L being
LINEAR ex
R being
REST st
for
x being
Real st
x in N holds
((SVF1 1,(pdiff1 f,1),z) . x) - ((SVF1 1,(pdiff1 f,1),z) . x0) = (L . (x - x0)) + (R . (x - x0)) ) );
pred f is_hpartial_differentiable`12_in z means :
Def3:
ex
x0,
y0 being
Real st
(
z = <*x0,y0*> & ex
N being
Neighbourhood of
y0 st
(
N c= dom (SVF1 2,(pdiff1 f,1),z) & ex
L being
LINEAR ex
R being
REST st
for
y being
Real st
y in N holds
((SVF1 2,(pdiff1 f,1),z) . y) - ((SVF1 2,(pdiff1 f,1),z) . y0) = (L . (y - y0)) + (R . (y - y0)) ) );
pred f is_hpartial_differentiable`21_in z means :
Def4:
ex
x0,
y0 being
Real st
(
z = <*x0,y0*> & ex
N being
Neighbourhood of
x0 st
(
N c= dom (SVF1 1,(pdiff1 f,2),z) & ex
L being
LINEAR ex
R being
REST st
for
x being
Real st
x in N holds
((SVF1 1,(pdiff1 f,2),z) . x) - ((SVF1 1,(pdiff1 f,2),z) . x0) = (L . (x - x0)) + (R . (x - x0)) ) );
pred f is_hpartial_differentiable`22_in z means :
Def5:
ex
x0,
y0 being
Real st
(
z = <*x0,y0*> & ex
N being
Neighbourhood of
y0 st
(
N c= dom (SVF1 2,(pdiff1 f,2),z) & ex
L being
LINEAR ex
R being
REST st
for
y being
Real st
y in N holds
((SVF1 2,(pdiff1 f,2),z) . y) - ((SVF1 2,(pdiff1 f,2),z) . y0) = (L . (y - y0)) + (R . (y - y0)) ) );
end;
:: deftheorem Def2 defines is_hpartial_differentiable`11_in PDIFF_3:def 2 :
for
f being
PartFunc of ,
for
z being
Element of
REAL 2 holds
(
f is_hpartial_differentiable`11_in z iff ex
x0,
y0 being
Real st
(
z = <*x0,y0*> & ex
N being
Neighbourhood of
x0 st
(
N c= dom (SVF1 1,(pdiff1 f,1),z) & ex
L being
LINEAR ex
R being
REST st
for
x being
Real st
x in N holds
((SVF1 1,(pdiff1 f,1),z) . x) - ((SVF1 1,(pdiff1 f,1),z) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) );
:: deftheorem Def3 defines is_hpartial_differentiable`12_in PDIFF_3:def 3 :
for
f being
PartFunc of ,
for
z being
Element of
REAL 2 holds
(
f is_hpartial_differentiable`12_in z iff ex
x0,
y0 being
Real st
(
z = <*x0,y0*> & ex
N being
Neighbourhood of
y0 st
(
N c= dom (SVF1 2,(pdiff1 f,1),z) & ex
L being
LINEAR ex
R being
REST st
for
y being
Real st
y in N holds
((SVF1 2,(pdiff1 f,1),z) . y) - ((SVF1 2,(pdiff1 f,1),z) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) );
:: deftheorem Def4 defines is_hpartial_differentiable`21_in PDIFF_3:def 4 :
for
f being
PartFunc of ,
for
z being
Element of
REAL 2 holds
(
f is_hpartial_differentiable`21_in z iff ex
x0,
y0 being
Real st
(
z = <*x0,y0*> & ex
N being
Neighbourhood of
x0 st
(
N c= dom (SVF1 1,(pdiff1 f,2),z) & ex
L being
LINEAR ex
R being
REST st
for
x being
Real st
x in N holds
((SVF1 1,(pdiff1 f,2),z) . x) - ((SVF1 1,(pdiff1 f,2),z) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) );
:: deftheorem Def5 defines is_hpartial_differentiable`22_in PDIFF_3:def 5 :
for
f being
PartFunc of ,
for
z being
Element of
REAL 2 holds
(
f is_hpartial_differentiable`22_in z iff ex
x0,
y0 being
Real st
(
z = <*x0,y0*> & ex
N being
Neighbourhood of
y0 st
(
N c= dom (SVF1 2,(pdiff1 f,2),z) & ex
L being
LINEAR ex
R being
REST st
for
y being
Real st
y in N holds
((SVF1 2,(pdiff1 f,2),z) . y) - ((SVF1 2,(pdiff1 f,2),z) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) );
definition
let f be
PartFunc of ,;
let z be
Element of
REAL 2;
assume A1:
f is_hpartial_differentiable`11_in z
;
func hpartdiff11 f,
z -> Real means :
Def6:
ex
x0,
y0 being
Real st
(
z = <*x0,y0*> & ex
N being
Neighbourhood of
x0 st
(
N c= dom (SVF1 1,(pdiff1 f,1),z) & 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),z) . x) - ((SVF1 1,(pdiff1 f,1),z) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) );
existence
ex b1, x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 1,(pdiff1 f,1),z) & 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),z) . x) - ((SVF1 1,(pdiff1 f,1),z) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) )
uniqueness
for b1, b2 being Real st ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 1,(pdiff1 f,1),z) & 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),z) . x) - ((SVF1 1,(pdiff1 f,1),z) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) & ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 1,(pdiff1 f,1),z) & 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),z) . x) - ((SVF1 1,(pdiff1 f,1),z) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def6 defines hpartdiff11 PDIFF_3:def 6 :
for
f being
PartFunc of ,
for
z being
Element of
REAL 2 st
f is_hpartial_differentiable`11_in z holds
for
b3 being
Real holds
(
b3 = hpartdiff11 f,
z iff ex
x0,
y0 being
Real st
(
z = <*x0,y0*> & ex
N being
Neighbourhood of
x0 st
(
N c= dom (SVF1 1,(pdiff1 f,1),z) & 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),z) . x) - ((SVF1 1,(pdiff1 f,1),z) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) );
definition
let f be
PartFunc of ,;
let z be
Element of
REAL 2;
assume A1:
f is_hpartial_differentiable`12_in z
;
func hpartdiff12 f,
z -> Real means :
Def7:
ex
x0,
y0 being
Real st
(
z = <*x0,y0*> & ex
N being
Neighbourhood of
y0 st
(
N c= dom (SVF1 2,(pdiff1 f,1),z) & 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),z) . y) - ((SVF1 2,(pdiff1 f,1),z) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) );
existence
ex b1, x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 2,(pdiff1 f,1),z) & 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),z) . y) - ((SVF1 2,(pdiff1 f,1),z) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) )
uniqueness
for b1, b2 being Real st ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 2,(pdiff1 f,1),z) & 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),z) . y) - ((SVF1 2,(pdiff1 f,1),z) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) & ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 2,(pdiff1 f,1),z) & 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),z) . y) - ((SVF1 2,(pdiff1 f,1),z) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def7 defines hpartdiff12 PDIFF_3:def 7 :
for
f being
PartFunc of ,
for
z being
Element of
REAL 2 st
f is_hpartial_differentiable`12_in z holds
for
b3 being
Real holds
(
b3 = hpartdiff12 f,
z iff ex
x0,
y0 being
Real st
(
z = <*x0,y0*> & ex
N being
Neighbourhood of
y0 st
(
N c= dom (SVF1 2,(pdiff1 f,1),z) & 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),z) . y) - ((SVF1 2,(pdiff1 f,1),z) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) );
definition
let f be
PartFunc of ,;
let z be
Element of
REAL 2;
assume A1:
f is_hpartial_differentiable`21_in z
;
func hpartdiff21 f,
z -> Real means :
Def8:
ex
x0,
y0 being
Real st
(
z = <*x0,y0*> & ex
N being
Neighbourhood of
x0 st
(
N c= dom (SVF1 1,(pdiff1 f,2),z) & 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),z) . x) - ((SVF1 1,(pdiff1 f,2),z) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) );
existence
ex b1, x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 1,(pdiff1 f,2),z) & 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),z) . x) - ((SVF1 1,(pdiff1 f,2),z) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) )
uniqueness
for b1, b2 being Real st ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 1,(pdiff1 f,2),z) & 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),z) . x) - ((SVF1 1,(pdiff1 f,2),z) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) & ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 1,(pdiff1 f,2),z) & 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),z) . x) - ((SVF1 1,(pdiff1 f,2),z) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def8 defines hpartdiff21 PDIFF_3:def 8 :
for
f being
PartFunc of ,
for
z being
Element of
REAL 2 st
f is_hpartial_differentiable`21_in z holds
for
b3 being
Real holds
(
b3 = hpartdiff21 f,
z iff ex
x0,
y0 being
Real st
(
z = <*x0,y0*> & ex
N being
Neighbourhood of
x0 st
(
N c= dom (SVF1 1,(pdiff1 f,2),z) & 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),z) . x) - ((SVF1 1,(pdiff1 f,2),z) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) );
definition
let f be
PartFunc of ,;
let z be
Element of
REAL 2;
assume A1:
f is_hpartial_differentiable`22_in z
;
func hpartdiff22 f,
z -> Real means :
Def9:
ex
x0,
y0 being
Real st
(
z = <*x0,y0*> & ex
N being
Neighbourhood of
y0 st
(
N c= dom (SVF1 2,(pdiff1 f,2),z) & 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),z) . y) - ((SVF1 2,(pdiff1 f,2),z) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) );
existence
ex b1, x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 2,(pdiff1 f,2),z) & 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),z) . y) - ((SVF1 2,(pdiff1 f,2),z) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) )
uniqueness
for b1, b2 being Real st ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 2,(pdiff1 f,2),z) & 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),z) . y) - ((SVF1 2,(pdiff1 f,2),z) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) & ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 2,(pdiff1 f,2),z) & 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),z) . y) - ((SVF1 2,(pdiff1 f,2),z) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def9 defines hpartdiff22 PDIFF_3:def 9 :
for
f being
PartFunc of ,
for
z being
Element of
REAL 2 st
f is_hpartial_differentiable`22_in z holds
for
b3 being
Real holds
(
b3 = hpartdiff22 f,
z iff ex
x0,
y0 being
Real st
(
z = <*x0,y0*> & ex
N being
Neighbourhood of
y0 st
(
N c= dom (SVF1 2,(pdiff1 f,2),z) & 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),z) . y) - ((SVF1 2,(pdiff1 f,2),z) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) );
theorem
theorem
theorem
theorem
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
:: deftheorem Def10 defines is_hpartial_differentiable`11_on PDIFF_3:def 10 :
:: deftheorem Def11 defines is_hpartial_differentiable`12_on PDIFF_3:def 11 :
:: deftheorem Def12 defines is_hpartial_differentiable`21_on PDIFF_3:def 12 :
:: deftheorem Def13 defines is_hpartial_differentiable`22_on PDIFF_3:def 13 :
:: deftheorem defines `hpartial11| PDIFF_3:def 14 :
:: deftheorem defines `hpartial12| PDIFF_3:def 15 :
:: deftheorem defines `hpartial21| PDIFF_3:def 16 :
:: deftheorem defines `hpartial22| PDIFF_3:def 17 :
begin
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem
for
f being
PartFunc of ,
for
z0 being
Element of
REAL 2
for
N being
Neighbourhood of
(proj 1,2) . z0 st
f is_hpartial_differentiable`11_in z0 &
N c= dom (SVF1 1,(pdiff1 f,1),z0) holds
for
h being
convergent_to_0 Real_Sequence for
c being
V8()
Real_Sequence st
rng c = {((proj 1,2) . z0)} &
rng (h + c) c= N holds
(
(h " ) (#) (((SVF1 1,(pdiff1 f,1),z0) /* (h + c)) - ((SVF1 1,(pdiff1 f,1),z0) /* c)) is
convergent &
hpartdiff11 f,
z0 = lim ((h " ) (#) (((SVF1 1,(pdiff1 f,1),z0) /* (h + c)) - ((SVF1 1,(pdiff1 f,1),z0) /* c))) )
theorem
for
f being
PartFunc of ,
for
z0 being
Element of
REAL 2
for
N being
Neighbourhood of
(proj 2,2) . z0 st
f is_hpartial_differentiable`12_in z0 &
N c= dom (SVF1 2,(pdiff1 f,1),z0) holds
for
h being
convergent_to_0 Real_Sequence for
c being
V8()
Real_Sequence st
rng c = {((proj 2,2) . z0)} &
rng (h + c) c= N holds
(
(h " ) (#) (((SVF1 2,(pdiff1 f,1),z0) /* (h + c)) - ((SVF1 2,(pdiff1 f,1),z0) /* c)) is
convergent &
hpartdiff12 f,
z0 = lim ((h " ) (#) (((SVF1 2,(pdiff1 f,1),z0) /* (h + c)) - ((SVF1 2,(pdiff1 f,1),z0) /* c))) )
theorem
for
f being
PartFunc of ,
for
z0 being
Element of
REAL 2
for
N being
Neighbourhood of
(proj 1,2) . z0 st
f is_hpartial_differentiable`21_in z0 &
N c= dom (SVF1 1,(pdiff1 f,2),z0) holds
for
h being
convergent_to_0 Real_Sequence for
c being
V8()
Real_Sequence st
rng c = {((proj 1,2) . z0)} &
rng (h + c) c= N holds
(
(h " ) (#) (((SVF1 1,(pdiff1 f,2),z0) /* (h + c)) - ((SVF1 1,(pdiff1 f,2),z0) /* c)) is
convergent &
hpartdiff21 f,
z0 = lim ((h " ) (#) (((SVF1 1,(pdiff1 f,2),z0) /* (h + c)) - ((SVF1 1,(pdiff1 f,2),z0) /* c))) )
theorem
for
f being
PartFunc of ,
for
z0 being
Element of
REAL 2
for
N being
Neighbourhood of
(proj 2,2) . z0 st
f is_hpartial_differentiable`22_in z0 &
N c= dom (SVF1 2,(pdiff1 f,2),z0) holds
for
h being
convergent_to_0 Real_Sequence for
c being
V8()
Real_Sequence st
rng c = {((proj 2,2) . z0)} &
rng (h + c) c= N holds
(
(h " ) (#) (((SVF1 2,(pdiff1 f,2),z0) /* (h + c)) - ((SVF1 2,(pdiff1 f,2),z0) /* c)) is
convergent &
hpartdiff22 f,
z0 = lim ((h " ) (#) (((SVF1 2,(pdiff1 f,2),z0) /* (h + c)) - ((SVF1 2,(pdiff1 f,2),z0) /* c))) )
theorem
for
z0 being
Element of
REAL 2
for
f1,
f2 being
PartFunc of , st
f1 is_hpartial_differentiable`11_in z0 &
f2 is_hpartial_differentiable`11_in z0 holds
(
(pdiff1 f1,1) + (pdiff1 f2,1) is_partial_differentiable_in z0,1 &
partdiff ((pdiff1 f1,1) + (pdiff1 f2,1)),
z0,1
= (hpartdiff11 f1,z0) + (hpartdiff11 f2,z0) )
theorem
for
z0 being
Element of
REAL 2
for
f1,
f2 being
PartFunc of , st
f1 is_hpartial_differentiable`12_in z0 &
f2 is_hpartial_differentiable`12_in z0 holds
(
(pdiff1 f1,1) + (pdiff1 f2,1) is_partial_differentiable_in z0,2 &
partdiff ((pdiff1 f1,1) + (pdiff1 f2,1)),
z0,2
= (hpartdiff12 f1,z0) + (hpartdiff12 f2,z0) )
theorem
for
z0 being
Element of
REAL 2
for
f1,
f2 being
PartFunc of , st
f1 is_hpartial_differentiable`21_in z0 &
f2 is_hpartial_differentiable`21_in z0 holds
(
(pdiff1 f1,2) + (pdiff1 f2,2) is_partial_differentiable_in z0,1 &
partdiff ((pdiff1 f1,2) + (pdiff1 f2,2)),
z0,1
= (hpartdiff21 f1,z0) + (hpartdiff21 f2,z0) )
theorem
for
z0 being
Element of
REAL 2
for
f1,
f2 being
PartFunc of , st
f1 is_hpartial_differentiable`22_in z0 &
f2 is_hpartial_differentiable`22_in z0 holds
(
(pdiff1 f1,2) + (pdiff1 f2,2) is_partial_differentiable_in z0,2 &
partdiff ((pdiff1 f1,2) + (pdiff1 f2,2)),
z0,2
= (hpartdiff22 f1,z0) + (hpartdiff22 f2,z0) )
theorem
for
z0 being
Element of
REAL 2
for
f1,
f2 being
PartFunc of , st
f1 is_hpartial_differentiable`11_in z0 &
f2 is_hpartial_differentiable`11_in z0 holds
(
(pdiff1 f1,1) - (pdiff1 f2,1) is_partial_differentiable_in z0,1 &
partdiff ((pdiff1 f1,1) - (pdiff1 f2,1)),
z0,1
= (hpartdiff11 f1,z0) - (hpartdiff11 f2,z0) )
theorem
for
z0 being
Element of
REAL 2
for
f1,
f2 being
PartFunc of , st
f1 is_hpartial_differentiable`12_in z0 &
f2 is_hpartial_differentiable`12_in z0 holds
(
(pdiff1 f1,1) - (pdiff1 f2,1) is_partial_differentiable_in z0,2 &
partdiff ((pdiff1 f1,1) - (pdiff1 f2,1)),
z0,2
= (hpartdiff12 f1,z0) - (hpartdiff12 f2,z0) )
theorem
for
z0 being
Element of
REAL 2
for
f1,
f2 being
PartFunc of , st
f1 is_hpartial_differentiable`21_in z0 &
f2 is_hpartial_differentiable`21_in z0 holds
(
(pdiff1 f1,2) - (pdiff1 f2,2) is_partial_differentiable_in z0,1 &
partdiff ((pdiff1 f1,2) - (pdiff1 f2,2)),
z0,1
= (hpartdiff21 f1,z0) - (hpartdiff21 f2,z0) )
theorem
for
z0 being
Element of
REAL 2
for
f1,
f2 being
PartFunc of , st
f1 is_hpartial_differentiable`22_in z0 &
f2 is_hpartial_differentiable`22_in z0 holds
(
(pdiff1 f1,2) - (pdiff1 f2,2) is_partial_differentiable_in z0,2 &
partdiff ((pdiff1 f1,2) - (pdiff1 f2,2)),
z0,2
= (hpartdiff22 f1,z0) - (hpartdiff22 f2,z0) )
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem