begin
definition
let i be
Element of
NAT ;
let n be non
empty Element of
NAT ;
let f be
PartFunc of
(REAL n),
REAL;
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;
definition
let f be
PartFunc of
(REAL 2),
REAL;
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
LinearFunc ex
R being
RestFunc 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
LinearFunc ex
R being
RestFunc 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
LinearFunc ex
R being
RestFunc 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
LinearFunc ex
R being
RestFunc 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 (REAL 2),REAL
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 LinearFunc ex R being RestFunc 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 (REAL 2),REAL
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 LinearFunc ex R being RestFunc 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 (REAL 2),REAL
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 LinearFunc ex R being RestFunc 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 (REAL 2),REAL
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 LinearFunc ex R being RestFunc 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
(REAL 2),
REAL;
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
LinearFunc ex
R being
RestFunc 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 LinearFunc ex R being RestFunc 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 LinearFunc ex R being RestFunc 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 LinearFunc ex R being RestFunc 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 (REAL 2),REAL
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 LinearFunc ex R being RestFunc 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
(REAL 2),
REAL;
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
LinearFunc ex
R being
RestFunc 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 LinearFunc ex R being RestFunc 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 LinearFunc ex R being RestFunc 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 LinearFunc ex R being RestFunc 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 (REAL 2),REAL
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 LinearFunc ex R being RestFunc 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
(REAL 2),
REAL;
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
LinearFunc ex
R being
RestFunc 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 LinearFunc ex R being RestFunc 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 LinearFunc ex R being RestFunc 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 LinearFunc ex R being RestFunc 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 (REAL 2),REAL
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 LinearFunc ex R being RestFunc 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
(REAL 2),
REAL;
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
LinearFunc ex
R being
RestFunc 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 LinearFunc ex R being RestFunc 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 LinearFunc ex R being RestFunc 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 LinearFunc ex R being RestFunc 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 (REAL 2),REAL
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 LinearFunc ex R being RestFunc 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)) ) ) ) ) );
begin
theorem
for
f being
PartFunc of
(REAL 2),
REAL 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
non-zero 0 -convergent Real_Sequence for
c being
constant 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
(REAL 2),
REAL 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
non-zero 0 -convergent Real_Sequence for
c being
constant 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
(REAL 2),
REAL 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
non-zero 0 -convergent Real_Sequence for
c being
constant 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
(REAL 2),
REAL 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
non-zero 0 -convergent Real_Sequence for
c being
constant 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
(REAL 2),
REAL 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
(REAL 2),
REAL 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
(REAL 2),
REAL 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
(REAL 2),
REAL 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
(REAL 2),
REAL 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
(REAL 2),
REAL 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
(REAL 2),
REAL 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
(REAL 2),
REAL 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)) )