:: Second-order Partial Differentiation of Real Ternary Functions
:: by Takao Inou\'e
::
:: Received January 26, 2010
:: Copyright (c) 2010 Association of Mizar Users
environ
vocabularies FUNCT_1, ARYTM_1, FINSEQ_1, RELAT_1, ORDINAL2, SEQ_1, SEQ_2,
RCOMP_1, PARTFUN1, FDIFF_1, PDIFF_1, ARYTM_3, FCONT_1, PDIFF_2, PDIFF_3,
PDIFF_5, NUMBERS, SUBSET_1, CARD_1, REAL_1, TARSKI, XXREAL_0, VALUED_1,
CARD_3, FUNCT_2, ORDINAL1, XXREAL_1, XREAL_0, VALUED_0, NAT_1;
notations TARSKI, SUBSET_1, XXREAL_0, XCMPLX_0, XREAL_0, NAT_1, ORDINAL1,
NUMBERS, REAL_1, VALUED_0, FUNCT_2, RELSET_1, PARTFUN1, VALUED_1, SEQ_1,
SEQ_2, FINSEQ_1, RCOMP_1, EUCLID, FDIFF_1, FCONT_1, FINSEQ_2, PDIFF_1,
PDIFF_2, PDIFF_3;
constructors REAL_1, SEQ_2, RCOMP_1, FDIFF_1, SEQ_1, FCONT_1, PDIFF_1,
PDIFF_2, COMPLEX1, RELSET_1, PDIFF_3, RVSUM_1, BINOP_2;
registrations RELSET_1, XREAL_0, MEMBERED, FDIFF_1, FUNCT_2, NAT_1, NUMBERS,
XXREAL_0, VALUED_0, VALUED_1, PDIFF_3, EUCLID;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions RCOMP_1, XBOOLE_0;
theorems TARSKI, XBOOLE_0, XBOOLE_1, XREAL_1, RCOMP_1, SEQ_4, SEQ_1, SEQ_2,
FINSEQ_1, FINSEQ_2, RFUNCT_2, PARTFUN1, FDIFF_1, VALUED_1, XCMPLX_0,
XCMPLX_1, FUNCT_2, VALUED_0, ORDINAL1, PDIFF_1, PDIFF_4;
schemes SEQ_1;
begin :: Second-order Partial Derivatives
reserve x,x0,x1,y,y0,y1,z,z0,z1,r,r1,s,p,p1 for Real;
reserve u,u0 for Element of REAL 3;
reserve n for Element of NAT;
reserve s1 for Real_Sequence;
reserve f,f1,f2 for PartFunc of REAL 3,REAL;
reserve R,R1 for REST;
reserve L,L1 for LINEAR;
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 :Def1:
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,R st for x 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 :Def2:
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,R st for y 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 :Def3:
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,R st for z 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 :Def4:
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,R st for x 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 :Def5:
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,R st for y 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 :Def6:
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,R st for z 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 :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,3),u) &
ex L,R st for x 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 :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,3),u) &
ex L,R st for y 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 :Def9:
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,R st for z 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;
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 :Def10:
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,R st it = L.1 & for x 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
proof
consider x0,y0,z0 being Real such that
A2: u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
N c= dom SVF1(1,pdiff1(f,1),u) & ex L,R st for x 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)
by A1,Def1;
consider N being Neighbourhood of x0 such that
A3: N c= dom SVF1(1,pdiff1(f,1),u) & ex L,R st for x 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)
by A2;
consider L,R such that
A4: for x 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)
by A3;
consider r such that
A5: for p holds L.p = r*p by FDIFF_1:def 4;
take r;
L.1 = r*1 by A5
.= r;
hence thesis by A2,A3,A4;
end;
uniqueness
proof
let r,s;
assume that
A6: 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,R st r = L.1 & for x 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) and
A7: 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,R st s = L.1 & for x 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);
consider x0,y0,z0 being Real such that
A8: u = <*x0,y0,z0*> &
ex N being Neighbourhood of x0 st N c= dom SVF1(1,pdiff1(f,1),u) &
ex L,R st r = L.1 & for x 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)
by A6;
consider N being Neighbourhood of x0 such that
A9: N c= dom SVF1(1,pdiff1(f,1),u) & ex L,R st r = L.1 & for x 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) by A8;
consider L,R such that
A10: r = L.1 & for x 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) by A9;
consider x1,y1,z1 being Real such that
A11: u = <*x1,y1,z1*> &
ex N being Neighbourhood of x1 st N c= dom SVF1(1,pdiff1(f,1),u) &
ex L,R st s = L.1 & for x st x in N holds
SVF1(1,pdiff1(f,1),u).x - SVF1(1,pdiff1(f,1),u).x1
= L.(x-x1) + R.(x-x1) by A7;
consider N1 being Neighbourhood of x1 such that
A12: N1 c= dom SVF1(1,pdiff1(f,1),u) &
ex L,R st s = L.1 & for x st x in N1 holds
SVF1(1,pdiff1(f,1),u).x - SVF1(1,pdiff1(f,1),u).x1
= L.(x-x1) + R.(x-x1) by A11;
consider L1,R1 such that
A13: s = L1.1 & for x st x in N1 holds
SVF1(1,pdiff1(f,1),u).x - SVF1(1,pdiff1(f,1),u).x1 = L1.(x-x1) + R1.(x-x1)
by A12;
consider r1 such that
A14: for p holds L.p = r1*p by FDIFF_1:def 4;
consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 4;
A16: r = r1*1 by A10,A14;
A17: s = p1*1 by A13,A15;
A18: x0 = x1 & y0 = y1 & z0 = z1 by A8,A11,FINSEQ_1:99;
A19: now let x;
assume
A20: x in N & x in N1;
then SVF1(1,pdiff1(f,1),u).x - SVF1(1,pdiff1(f,1),u).x0
= L.(x-x0) + R.(x-x0) by A10;
then L.(x-x0) + R.(x-x0) = L1.(x-x0) + R1.(x-x0) by A13,A18,A20;
then r1*(x-x0) + R.(x-x0) = L1.(x-x0) + R1.(x-x0) by A14;
hence r*(x-x0) + R.(x-x0) = s*(x-x0) + R1.(x-x0) by A15,A16,A17;
end;
consider N0 be Neighbourhood of x0 such that
A21: N0 c= N & N0 c= N1 by A18,RCOMP_1:38;
consider g be real number such that
A22: 0 < g & N0 = ].x0-g,x0+g.[ by RCOMP_1:def 7;
deffunc F(Element of NAT) = g/($1+2);
consider s1 such that
A23: for n holds s1.n = F(n) from SEQ_1:sch 1;
now let n;
g/(n+2) <> 0 by A22,XREAL_1:141;
hence s1.n <> 0 by A23;
end;
then
A24: s1 is non-zero by SEQ_1:7;
s1 is convergent & lim s1 = 0 by A23,SEQ_4:46;
then reconsider h = s1 as convergent_to_0 Real_Sequence
by A24,FDIFF_1:def 1;
A25: for n ex x st x in N & x in N1 & h.n = x-x0
proof
let n;
A26: g/(n+2) > 0 by A22,XREAL_1:141;
0+1 < n+1+1 by XREAL_1:8;
then g/(n+2) < g/1 by A22,XREAL_1:78;then
A27: x0+g/(n+2) < x0+g by XREAL_1:8;
x0+-g < x0+g/(n+2) by A22,A26,XREAL_1:8;
then A28: x0+g/(n+2) in ].x0-g,x0+g.[ by A27;
take x0+g/(n+2);
thus thesis by A21,A22,A23,A28;
end;
A29: for n being Nat holds r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n
proof let n be Nat;
A30: n in NAT by ORDINAL1:def 13; then
ex x st x in N & x in N1 & h.n = x-x0 by A25;then
A31: r*(h.n) + R.(h.n) = s*(h.n) + R1.(h.n) by A19;
h is non-zero by FDIFF_1:def 1;then
A32: h.n <> 0 by SEQ_1:7,A30;
A33: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (s*(h.n) + R1.(h.n))/(h.n)
by A31,XCMPLX_1:63;
A34: (r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:75
.= r*1 by A32,XCMPLX_1:60
.= r;
(s*(h.n))/(h.n) = s*((h.n)/(h.n)) by XCMPLX_1:75
.= s*1 by A32,XCMPLX_1:60
.= s;then
A35: r + (R.(h.n))/(h.n) = s + (R1.(h.n))/(h.n) by A33,A34,XCMPLX_1:63;
dom R = REAL by PARTFUN1:def 4;then
A36: rng h c= dom R;
dom R1 = REAL by PARTFUN1:def 4;then
A37: rng h c= dom R1;
A38: (R.(h.n))/(h.n) = (R.(h.n))*(h.n)" by XCMPLX_0:def 9
.= (R.(h.n))*(h".n) by VALUED_1:10
.= ((R/*h).n)*(h".n) by A36,FUNCT_2:185,A30
.= ((h")(#)(R/*h)).n by VALUED_1:5;
(R1.(h.n))/(h.n) = (R1.(h.n))*(h.n)" by XCMPLX_0:def 9
.= (R1.(h.n))*(h".n) by VALUED_1:10
.= ((R1/*h).n)*(h".n) by A37,FUNCT_2:185,A30
.= ((h")(#)(R1/*h)).n by VALUED_1:5;
then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by A35,A38;
hence thesis by A30,RFUNCT_2:6;
end; then
A39: ((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant by VALUED_0:def 18;
(((h")(#)(R1/*h))-((h")(#)(R/*h))).1 = r-s by A29;then
A40: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-s by A39,SEQ_4:40;
A41: (h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0 by FDIFF_1:def 3;
(h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by FDIFF_1:def 3;
then r-s = 0-0 by A40,A41,SEQ_2:26;
hence thesis;
end;
end;
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 :Def11:
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,R st it = L.1 & for y 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
proof
consider x0,y0,z0 being Real such that
A2: u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
N c= dom SVF1(2,pdiff1(f,1),u) & ex L,R st for y 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)
by A1,Def2;
consider N being Neighbourhood of y0 such that
A3: N c= dom SVF1(2,pdiff1(f,1),u) & ex L,R st for y 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)
by A2;
consider L,R such that
A4: for y 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)
by A3;
consider r such that
A5: for p holds L.p = r*p by FDIFF_1:def 4;
take r;
L.1 = r*1 by A5 .= r;
hence thesis by A2,A3,A4;
end;
uniqueness
proof
let r,s;
assume that
A6: 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,R st r = L.1 & for y 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) and
A7: 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,R st s = L.1 & for y 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);
consider x0,y0,z0 being Real such that
A8: u = <*x0,y0,z0*> &
ex N being Neighbourhood of y0 st N c= dom SVF1(2,pdiff1(f,1),u) &
ex L,R st r = L.1 & for y 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)
by A6;
consider N being Neighbourhood of y0 such that
A9: N c= dom SVF1(2,pdiff1(f,1),u) & ex L,R st r = L.1 & for y 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) by A8;
consider L,R such that
A10: r = L.1 & for y 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) by A9;
consider x1,y1,z1 being Real such that
A11: u = <*x1,y1,z1*> &
ex N being Neighbourhood of y1 st N c= dom SVF1(2,pdiff1(f,1),u) &
ex L,R st s = L.1 & for y st y in N holds
SVF1(2,pdiff1(f,1),u).y - SVF1(2,pdiff1(f,1),u).y1
= L.(y-y1) + R.(y-y1) by A7;
consider N1 being Neighbourhood of y1 such that
A12: N1 c= dom SVF1(2,pdiff1(f,1),u) &
ex L,R st s = L.1 & for y st y in N1 holds
SVF1(2,pdiff1(f,1),u).y - SVF1(2,pdiff1(f,1),u).y1
= L.(y-y1) + R.(y-y1) by A11;
consider L1,R1 such that
A13: s = L1.1 & for y st y in N1 holds
SVF1(2,pdiff1(f,1),u).y - SVF1(2,pdiff1(f,1),u).y1
= L1.(y-y1) + R1.(y-y1) by A12;
consider r1 such that
A14: for p holds L.p = r1*p by FDIFF_1:def 4;
consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 4;
A16: r = r1*1 by A10,A14;
A17: s = p1*1 by A13,A15;
A18: x0 = x1 & y0 = y1 & z0 = z1 by A8,A11,FINSEQ_1:99;
A19: now let y;
assume
A20: y in N & y in N1;
then SVF1(2,pdiff1(f,1),u).y - SVF1(2,pdiff1(f,1),u).y0
= L.(y-y0) + R.(y-y0) by A10;
then L.(y-y0) + R.(y-y0) = L1.(y-y0) + R1.(y-y0) by A13,A18,A20;
then r1*(y-y0) + R.(y-y0) = L1.(y-y0) + R1.(y-y0) by A14;
hence r*(y-y0) + R.(y-y0) = s*(y-y0) + R1.(y-y0) by A15,A16,A17;
end;
consider N0 be Neighbourhood of y0 such that
A21: N0 c= N & N0 c= N1 by A18,RCOMP_1:38;
consider g be real number such that
A22: 0 < g & N0 = ].y0-g,y0+g.[ by RCOMP_1:def 7;
deffunc F(Element of NAT) = g/($1+2);
consider s1 such that
A23: for n holds s1.n = F(n) from SEQ_1:sch 1;
now let n;
g/(n+2) <> 0 by A22,XREAL_1:141;
hence s1.n <> 0 by A23;
end; then
A24: s1 is non-zero by SEQ_1:7;
s1 is convergent & lim s1 = 0 by A23,SEQ_4:46;
then reconsider h = s1 as convergent_to_0 Real_Sequence
by A24,FDIFF_1:def 1;
A25: for n ex y st y in N & y in N1 & h.n = y-y0
proof
let n;
A26: g/(n+2) > 0 by A22,XREAL_1:141;
0+1 < n+1+1 by XREAL_1:8;
then g/(n+2) < g/1 by A22,XREAL_1:78;then
A27: y0+g/(n+2) < y0+g by XREAL_1:8;
y0+-g < y0+g/(n+2) by A22,A26,XREAL_1:8;
then A28: y0+g/(n+2) in ].y0-g,y0+g.[ by A27;
take y0+g/(n+2);
thus thesis by A21,A22,A23,A28;
end;
A29: now let n be Nat;
A30: n in NAT by ORDINAL1:def 13; then
ex y st y in N & y in N1 & h.n = y-y0 by A25;then
A31: r*(h.n) + R.(h.n) = s*(h.n) + R1.(h.n) by A19;
h is non-zero by FDIFF_1:def 1;then
A32: h.n <> 0 by A30,SEQ_1:7;
A33: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (s*(h.n) + R1.(h.n))/(h.n)
by A31,XCMPLX_1:63;
A34: (r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:75
.= r*1 by A32,XCMPLX_1:60
.= r;
(s*(h.n))/(h.n) = s*((h.n)/(h.n)) by XCMPLX_1:75
.= s*1 by A32,XCMPLX_1:60
.= s;then
A35: r + (R.(h.n))/(h.n) = s + (R1.(h.n))/(h.n) by A33,A34,XCMPLX_1:63;
dom R = REAL by PARTFUN1:def 4;then
A36: rng h c= dom R;
dom R1 = REAL by PARTFUN1:def 4;then
A37: rng h c= dom R1;
A38: (R.(h.n))/(h.n) = (R.(h.n))*(h.n)" by XCMPLX_0:def 9
.= (R.(h.n))*(h".n) by VALUED_1:10
.= ((R/*h).n)*(h".n) by A36,FUNCT_2:185,A30
.= ((h")(#)(R/*h)).n by VALUED_1:5;
(R1.(h.n))/(h.n) = (R1.(h.n))*(h.n)" by XCMPLX_0:def 9
.= (R1.(h.n))*(h".n) by VALUED_1:10
.= ((R1/*h).n)*(h".n) by A37,FUNCT_2:185,A30
.= ((h")(#)(R1/*h)).n by VALUED_1:5;
then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by A35,A38;
hence r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n by A30,RFUNCT_2:6;
end; then
A39: ((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant by VALUED_0:def 18;
(((h")(#)(R1/*h))-((h")(#)(R/*h))).1 = r-s by A29;then
A40: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-s by A39,SEQ_4:40;
A41: (h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0 by FDIFF_1:def 3;
(h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by FDIFF_1:def 3;
then r-s = 0-0 by A40,A41,SEQ_2:26;
hence thesis;
end;
end;
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 :Def12:
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,R st it = L.1 & for z 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
proof
consider x0,y0,z0 being Real such that
A2: u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
N c= dom SVF1(3,pdiff1(f,1),u) & ex L,R st for z 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)
by A1,Def3;
consider N being Neighbourhood of z0 such that
A3: N c= dom SVF1(3,pdiff1(f,1),u) & ex L,R st for z 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)
by A2;
consider L,R such that
A4: for z 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)
by A3;
consider r such that
A5: for p holds L.p = r*p by FDIFF_1:def 4;
take r;
L.1 = r*1 by A5 .= r;
hence thesis by A2,A3,A4;
end;
uniqueness
proof
let r,s;
assume that
A6: 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,R st r = L.1 & for z 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) and
A7: 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,R st s = L.1 & for z 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);
consider x0,y0,z0 being Real such that
A8: u = <*x0,y0,z0*> &
ex N being Neighbourhood of z0 st N c= dom SVF1(3,pdiff1(f,1),u) &
ex L,R st r = L.1 & for z 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)
by A6;
consider N being Neighbourhood of z0 such that
A9: N c= dom SVF1(3,pdiff1(f,1),u) & ex L,R st r = L.1 & for z 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) by A8;
consider L,R such that
A10: r = L.1 & for z 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) by A9;
consider x1,y1,z1 being Real such that
A11: u = <*x1,y1,z1*> &
ex N being Neighbourhood of z1 st N c= dom SVF1(3,pdiff1(f,1),u) &
ex L,R st s = L.1 & for z st z in N holds
SVF1(3,pdiff1(f,1),u).z - SVF1(3,pdiff1(f,1),u).z1
= L.(z-z1) + R.(z-z1) by A7;
consider N1 being Neighbourhood of z1 such that
A12: N1 c= dom SVF1(3,pdiff1(f,1),u) &
ex L,R st s = L.1 & for z st z in N1 holds
SVF1(3,pdiff1(f,1),u).z - SVF1(3,pdiff1(f,1),u).z1
= L.(z-z1) + R.(z-z1) by A11;
consider L1,R1 such that
A13: s = L1.1 & for z st z in N1 holds
SVF1(3,pdiff1(f,1),u).z - SVF1(3,pdiff1(f,1),u).z1
= L1.(z-z1) + R1.(z-z1) by A12;
consider r1 such that
A14: for p holds L.p = r1*p by FDIFF_1:def 4;
consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 4;
A16: r = r1*1 by A10,A14;
A17: s = p1*1 by A13,A15;
A18: x0 = x1 & y0 = y1 & z0 = z1 by A8,A11,FINSEQ_1:99;
A19: now let z;
assume
A20: z in N & z in N1;
then SVF1(3,pdiff1(f,1),u).z - SVF1(3,pdiff1(f,1),u).z0
= L.(z-z0) + R.(z-z0) by A10;
then L.(z-z0) + R.(z-z0) = L1.(z-z0) + R1.(z-z0) by A13,A18,A20;
then r1*(z-z0) + R.(z-z0) = L1.(z-z0) + R1.(z-z0) by A14;
hence r*(z-z0) + R.(z-z0) = s*(z-z0) + R1.(z-z0) by A15,A16,A17;
end;
consider N0 be Neighbourhood of z0 such that
A21: N0 c= N & N0 c= N1 by A18,RCOMP_1:38;
consider g be real number such that
A22: 0 < g & N0 = ].z0-g,z0+g.[ by RCOMP_1:def 7;
deffunc F(Element of NAT) = g/($1+2);
consider s1 such that
A23: for n holds s1.n = F(n) from SEQ_1:sch 1;
now let n;
g/(n+2) <> 0 by A22,XREAL_1:141;
hence s1.n <> 0 by A23;
end; then
A24: s1 is non-zero by SEQ_1:7;
s1 is convergent & lim s1 = 0 by A23,SEQ_4:46;
then reconsider h = s1 as convergent_to_0 Real_Sequence
by A24,FDIFF_1:def 1;
A25: for n ex z st z in N & z in N1 & h.n = z-z0
proof
let n;
A26: g/(n+2) > 0 by A22,XREAL_1:141;
0+1 < n+1+1 by XREAL_1:8;
then g/(n+2) < g/1 by A22,XREAL_1:78;then
A27: z0+g/(n+2) < z0+g by XREAL_1:8;
z0+-g < z0+g/(n+2) by A22,A26,XREAL_1:8;
then A28: z0+g/(n+2) in ].z0-g,z0+g.[ by A27;
take z0+g/(n+2);
thus thesis by A21,A22,A23,A28;
end;
A29: now let n be Nat;
A30: n in NAT by ORDINAL1:def 13; then
ex z st z in N & z in N1 & h.n = z-z0 by A25;then
A31: r*(h.n) + R.(h.n) = s*(h.n) + R1.(h.n) by A19;
h is non-zero by FDIFF_1:def 1;then
A32: h.n <> 0 by A30,SEQ_1:7;
A33: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (s*(h.n) + R1.(h.n))/(h.n)
by A31,XCMPLX_1:63;
A34: (r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:75
.= r*1 by A32,XCMPLX_1:60
.= r;
(s*(h.n))/(h.n) = s*((h.n)/(h.n)) by XCMPLX_1:75
.= s*1 by A32,XCMPLX_1:60
.= s;then
A35: r + (R.(h.n))/(h.n) = s + (R1.(h.n))/(h.n) by A33,A34,XCMPLX_1:63;
dom R = REAL by PARTFUN1:def 4;then
A36: rng h c= dom R;
dom R1 = REAL by PARTFUN1:def 4;then
A37: rng h c= dom R1;
A38: (R.(h.n))/(h.n) = (R.(h.n))*(h.n)" by XCMPLX_0:def 9
.= (R.(h.n))*(h".n) by VALUED_1:10
.= ((R/*h).n)*(h".n) by A36,FUNCT_2:185,A30
.= ((h")(#)(R/*h)).n by VALUED_1:5;
(R1.(h.n))/(h.n) = (R1.(h.n))*(h.n)" by XCMPLX_0:def 9
.= (R1.(h.n))*(h".n) by VALUED_1:10
.= ((R1/*h).n)*(h".n) by A37,FUNCT_2:185,A30
.= ((h")(#)(R1/*h)).n by VALUED_1:5;
then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by A35,A38;
hence r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n by A30,RFUNCT_2:6;
end; then
A39: ((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant by VALUED_0:def 18;
(((h")(#)(R1/*h))-((h")(#)(R/*h))).1 = r-s by A29;then
A40: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-s by A39,SEQ_4:40;
A41: (h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0 by FDIFF_1:def 3;
(h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by FDIFF_1:def 3;
then r-s = 0-0 by A40,A41,SEQ_2:26;
hence thesis;
end;
end;
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 :Def13:
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,R st it = L.1 & for x 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
proof
consider x0,y0,z0 being Real such that
A2: u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
N c= dom SVF1(1,pdiff1(f,2),u) & ex L,R st for x 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)
by A1,Def4;
consider N being Neighbourhood of x0 such that
A3: N c= dom SVF1(1,pdiff1(f,2),u) & ex L,R st for x 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)
by A2;
consider L,R such that
A4: for x 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)
by A3;
consider r such that
A5: for p holds L.p = r*p by FDIFF_1:def 4;
take r;
L.1 = r*1 by A5
.= r;
hence thesis by A2,A3,A4;
end;
uniqueness
proof
let r,s;
assume that
A6: 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,R st r = L.1 & for x 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) and
A7: 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,R st s = L.1 & for x 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);
consider x0,y0,z0 being Real such that
A8: u = <*x0,y0,z0*> &
ex N being Neighbourhood of x0 st N c= dom SVF1(1,pdiff1(f,2),u) &
ex L,R st r = L.1 & for x 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)
by A6;
consider N being Neighbourhood of x0 such that
A9: N c= dom SVF1(1,pdiff1(f,2),u) & ex L,R st r = L.1 & for x 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) by A8;
consider L,R such that
A10: r = L.1 & for x 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) by A9;
consider x1,y1, z1 being Real such that
A11: u = <*x1,y1, z1*> &
ex N being Neighbourhood of x1 st N c= dom SVF1(1,pdiff1(f,2),u) &
ex L,R st s = L.1 & for x st x in N holds
SVF1(1,pdiff1(f,2),u).x - SVF1(1,pdiff1(f,2),u).x1
= L.(x-x1) + R.(x-x1) by A7;
consider N1 being Neighbourhood of x1 such that
A12: N1 c= dom SVF1(1,pdiff1(f,2),u) &
ex L,R st s = L.1 & for x st x in N1 holds
SVF1(1,pdiff1(f,2),u).x - SVF1(1,pdiff1(f,2),u).x1
= L.(x-x1) + R.(x-x1) by A11;
consider L1,R1 such that
A13: s = L1.1 & for x st x in N1 holds
SVF1(1,pdiff1(f,2),u).x - SVF1(1,pdiff1(f,2),u).x1
= L1.(x-x1) + R1.(x-x1) by A12;
consider r1 such that
A14: for p holds L.p = r1*p by FDIFF_1:def 4;
consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 4;
A16: r = r1*1 by A10,A14;
A17: s = p1*1 by A13,A15;
A18: x0 = x1 & y0 = y1 & z0 = z1 by A8,A11,FINSEQ_1:99;
A19: now let x;
assume
A20: x in N & x in N1;
then SVF1(1,pdiff1(f,2),u).x - SVF1(1,pdiff1(f,2),u).x0
= L.(x-x0) + R.(x-x0) by A10;
then L.(x-x0) + R.(x-x0) = L1.(x-x0) + R1.(x-x0) by A13,A18,A20;
then r1*(x-x0) + R.(x-x0) = L1.(x-x0) + R1.(x-x0) by A14;
hence r*(x-x0) + R.(x-x0) = s*(x-x0) + R1.(x-x0) by A15,A16,A17;
end;
consider N0 be Neighbourhood of x0 such that
A21: N0 c= N & N0 c= N1 by A18,RCOMP_1:38;
consider g be real number such that
A22: 0 < g & N0 = ].x0-g,x0+g.[ by RCOMP_1:def 7;
deffunc F(Element of NAT) = g/($1+2);
consider s1 such that
A23: for n holds s1.n = F(n) from SEQ_1:sch 1;
now let n;
g/(n+2) <> 0 by A22,XREAL_1:141;
hence s1.n <> 0 by A23;
end; then
A24: s1 is non-zero by SEQ_1:7;
s1 is convergent & lim s1 = 0 by A23,SEQ_4:46;
then reconsider h = s1 as convergent_to_0 Real_Sequence
by A24,FDIFF_1:def 1;
A25: for n ex x st x in N & x in N1 & h.n = x-x0
proof
let n;
A26: g/(n+2) > 0 by A22,XREAL_1:141;
0+1 < n+1+1 by XREAL_1:8;
then g/(n+2) < g/1 by A22,XREAL_1:78;then
A27: x0+g/(n+2) < x0+g by XREAL_1:8;
x0+-g < x0+g/(n+2) by A22,A26,XREAL_1:8;
then A28: x0+g/(n+2) in ].x0-g,x0+g.[ by A27;
take x0+g/(n+2);
thus thesis by A21,A22,A23,A28;
end;
A29: now let n be Nat;
A30: n in NAT by ORDINAL1:def 13; then
ex x st x in N & x in N1 & h.n = x-x0 by A25;then
A31: r*(h.n) + R.(h.n) = s*(h.n) + R1.(h.n) by A19;
h is non-zero by FDIFF_1:def 1;then
A32: h.n <> 0 by A30,SEQ_1:7;
A33: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (s*(h.n) + R1.(h.n))/(h.n)
by A31,XCMPLX_1:63;
A34: (r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:75
.= r*1 by A32,XCMPLX_1:60
.= r;
(s*(h.n))/(h.n) = s*((h.n)/(h.n)) by XCMPLX_1:75
.= s*1 by A32,XCMPLX_1:60
.= s;then
A35: r + (R.(h.n))/(h.n) = s + (R1.(h.n))/(h.n) by A33,A34,XCMPLX_1:63;
dom R = REAL by PARTFUN1:def 4;then
A36: rng h c= dom R;
dom R1 = REAL by PARTFUN1:def 4;then
A37: rng h c= dom R1;
A38: (R.(h.n))/(h.n) = (R.(h.n))*(h.n)" by XCMPLX_0:def 9
.= (R.(h.n))*(h".n) by VALUED_1:10
.= ((R/*h).n)*(h".n) by A36,FUNCT_2:185,A30
.= ((h")(#)(R/*h)).n by VALUED_1:5;
(R1.(h.n))/(h.n) = (R1.(h.n))*(h.n)" by XCMPLX_0:def 9
.= (R1.(h.n))*(h".n) by VALUED_1:10
.= ((R1/*h).n)*(h".n) by A37,FUNCT_2:185,A30
.= ((h")(#)(R1/*h)).n by VALUED_1:5;
then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by A35,A38;
hence r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n by VALUED_1:15,A30;
end; then
A39: ((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant by VALUED_0:def 18;
(((h")(#)(R1/*h))-((h")(#)(R/*h))).1 = r-s by A29;then
A40: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-s by A39,SEQ_4:40;
A41: (h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0 by FDIFF_1:def 3;
(h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by FDIFF_1:def 3;
then r-s = 0-0 by A40,A41,SEQ_2:26;
hence thesis;
end;
end;
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 :Def14:
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,R st it = L.1 & for y 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
proof
consider x0,y0,z0 being Real such that
A2: u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
N c= dom SVF1(2,pdiff1(f,2),u) & ex L,R st for y 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)
by A1,Def5;
consider N being Neighbourhood of y0 such that
A3: N c= dom SVF1(2,pdiff1(f,2),u) & ex L,R st for y 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)
by A2;
consider L,R such that
A4: for y 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)
by A3;
consider r such that
A5: for p holds L.p = r*p by FDIFF_1:def 4;
take r;
L.1 = r*1 by A5 .= r;
hence thesis by A2,A3,A4;
end;
uniqueness
proof
let r,s;
assume that
A6: 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,R st r = L.1 & for y 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) and
A7: 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,R st s = L.1 & for y 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);
consider x0,y0,z0 being Real such that
A8: u = <*x0,y0,z0*> &
ex N being Neighbourhood of y0 st N c= dom SVF1(2,pdiff1(f,2),u) &
ex L,R st r = L.1 & for y 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)
by A6;
consider N being Neighbourhood of y0 such that
A9: N c= dom SVF1(2,pdiff1(f,2),u) & ex L,R st r = L.1 & for y 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) by A8;
consider L,R such that
A10: r = L.1 & for y 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) by A9;
consider x1,y1, z1 being Real such that
A11: u = <*x1,y1, z1*> &
ex N being Neighbourhood of y1 st N c= dom SVF1(2,pdiff1(f,2),u) &
ex L,R st s = L.1 & for y st y in N holds
SVF1(2,pdiff1(f,2),u).y - SVF1(2,pdiff1(f,2),u).y1
= L.(y-y1) + R.(y-y1) by A7;
consider N1 being Neighbourhood of y1 such that
A12: N1 c= dom SVF1(2,pdiff1(f,2),u) &
ex L,R st s = L.1 & for y st y in N1 holds
SVF1(2,pdiff1(f,2),u).y - SVF1(2,pdiff1(f,2),u).y1
= L.(y-y1) + R.(y-y1) by A11;
consider L1,R1 such that
A13: s = L1.1 & for y st y in N1 holds
SVF1(2,pdiff1(f,2),u).y - SVF1(2,pdiff1(f,2),u).y1
= L1.(y-y1) + R1.(y-y1) by A12;
consider r1 such that
A14: for p holds L.p = r1*p by FDIFF_1:def 4;
consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 4;
A16: r = r1*1 by A10,A14;
A17: s = p1*1 by A13,A15;
A18: x0 = x1 & y0 = y1 & z0 = z1 by A8,A11,FINSEQ_1:99;
A19: now let y;
assume
A20: y in N & y in N1;
then SVF1(2,pdiff1(f,2),u).y - SVF1(2,pdiff1(f,2),u).y0
= L.(y-y0) + R.(y-y0) by A10;
then L.(y-y0) + R.(y-y0) = L1.(y-y0) + R1.(y-y0) by A13,A18,A20;
then r1*(y-y0) + R.(y-y0) = L1.(y-y0) + R1.(y-y0) by A14;
hence r*(y-y0) + R.(y-y0) = s*(y-y0) + R1.(y-y0) by A15,A16,A17;
end;
consider N0 be Neighbourhood of y0 such that
A21: N0 c= N & N0 c= N1 by A18,RCOMP_1:38;
consider g be real number such that
A22: 0 < g & N0 = ].y0-g,y0+g.[ by RCOMP_1:def 7;
deffunc F(Element of NAT) = g/($1+2);
consider s1 such that
A23: for n holds s1.n = F(n) from SEQ_1:sch 1;
now let n;
g/(n+2) <> 0 by A22,XREAL_1:141;
hence s1.n <> 0 by A23;
end; then
A24: s1 is non-zero by SEQ_1:7;
s1 is convergent & lim s1 = 0 by A23,SEQ_4:46;
then reconsider h = s1 as convergent_to_0 Real_Sequence
by A24,FDIFF_1:def 1;
A25: for n ex y st y in N & y in N1 & h.n = y-y0
proof
let n;
A26: g/(n+2) > 0 by A22,XREAL_1:141;
0+1 < n+1+1 by XREAL_1:8;
then g/(n+2) < g/1 by A22,XREAL_1:78;then
A27: y0+g/(n+2) < y0+g by XREAL_1:8;
y0+-g < y0+g/(n+2) by A22,A26,XREAL_1:8;
then A28: y0+g/(n+2) in ].y0-g,y0+g.[ by A27;
take y0+g/(n+2);
thus thesis by A21,A22,A23,A28;
end;
A29: now let n be Nat;
A30: n in NAT by ORDINAL1:def 13; then
ex y st y in N & y in N1 & h.n = y-y0 by A25;then
A31: r*(h.n) + R.(h.n) = s*(h.n) + R1.(h.n) by A19;
h is non-zero by FDIFF_1:def 1;then
A32: h.n <> 0 by SEQ_1:7,A30;
A33: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (s*(h.n) + R1.(h.n))/(h.n)
by A31,XCMPLX_1:63;
A34: (r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:75
.= r*1 by A32,XCMPLX_1:60
.= r;
(s*(h.n))/(h.n) = s*((h.n)/(h.n)) by XCMPLX_1:75
.= s*1 by A32,XCMPLX_1:60
.= s;then
A35: r + (R.(h.n))/(h.n) = s + (R1.(h.n))/(h.n) by A33,A34,XCMPLX_1:63;
dom R = REAL by PARTFUN1:def 4;then
A36: rng h c= dom R;
dom R1 = REAL by PARTFUN1:def 4;then
A37: rng h c= dom R1;
A38: (R.(h.n))/(h.n) = (R.(h.n))*(h.n)" by XCMPLX_0:def 9
.= (R.(h.n))*(h".n) by VALUED_1:10
.= ((R/*h).n)*(h".n) by A36,FUNCT_2:185,A30
.= ((h")(#)(R/*h)).n by VALUED_1:5;
(R1.(h.n))/(h.n) = (R1.(h.n))*(h.n)" by XCMPLX_0:def 9
.= (R1.(h.n))*(h".n) by VALUED_1:10
.= ((R1/*h).n)*(h".n) by A37,FUNCT_2:185,A30
.= ((h")(#)(R1/*h)).n by VALUED_1:5;
then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by A35,A38;
hence r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n by RFUNCT_2:6,A30;
end; then
A39: ((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant by VALUED_0:def 18;
(((h")(#)(R1/*h))-((h")(#)(R/*h))).1 = r-s by A29;then
A40: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-s by A39,SEQ_4:40;
A41: (h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0 by FDIFF_1:def 3;
(h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by FDIFF_1:def 3;
then r-s = 0-0 by A40,A41,SEQ_2:26;
hence thesis;
end;
end;
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 :Def15:
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,R st it = L.1 & for z 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
proof
consider x0,y0,z0 being Real such that
A2: u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
N c= dom SVF1(3,pdiff1(f,2),u) & ex L,R st for z 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)
by A1,Def6;
consider N being Neighbourhood of z0 such that
A3: N c= dom SVF1(3,pdiff1(f,2),u) & ex L,R st for z 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)
by A2;
consider L,R such that
A4: for z 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)
by A3;
consider r such that
A5: for p holds L.p = r*p by FDIFF_1:def 4;
take r;
L.1 = r*1 by A5 .= r;
hence thesis by A2,A3,A4;
end;
uniqueness
proof
let r,s;
assume that
A6: 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,R st r = L.1 & for z 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) and
A7: 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,R st s = L.1 & for z 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);
consider x0,y0,z0 being Real such that
A8: u = <*x0,y0,z0*> &
ex N being Neighbourhood of z0 st N c= dom SVF1(3,pdiff1(f,2),u) &
ex L,R st r = L.1 & for z 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)
by A6;
consider N being Neighbourhood of z0 such that
A9: N c= dom SVF1(3,pdiff1(f,2),u) & ex L,R st r = L.1 & for z 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) by A8;
consider L,R such that
A10: r = L.1 & for z 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) by A9;
consider x1,y1,z1 being Real such that
A11: u = <*x1,y1,z1*> &
ex N being Neighbourhood of z1 st N c= dom SVF1(3,pdiff1(f,2),u) &
ex L,R st s = L.1 & for z st z in N holds
SVF1(3,pdiff1(f,2),u).z - SVF1(3,pdiff1(f,2),u).z1
= L.(z-z1) + R.(z-z1) by A7;
consider N1 being Neighbourhood of z1 such that
A12: N1 c= dom SVF1(3,pdiff1(f,2),u) &
ex L,R st s = L.1 & for z st z in N1 holds
SVF1(3,pdiff1(f,2),u).z - SVF1(3,pdiff1(f,2),u).z1
= L.(z-z1) + R.(z-z1) by A11;
consider L1,R1 such that
A13: s = L1.1 & for z st z in N1 holds
SVF1(3,pdiff1(f,2),u).z - SVF1(3,pdiff1(f,2),u).z1
= L1.(z-z1) + R1.(z-z1) by A12;
consider r1 such that
A14: for p holds L.p = r1*p by FDIFF_1:def 4;
consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 4;
A16: r = r1*1 by A10,A14;
A17: s = p1*1 by A13,A15;
A18: x0 = x1 & y0 = y1 & z0 = z1 by A8,A11,FINSEQ_1:99;
A19: now let z;
assume
A20: z in N & z in N1;
then SVF1(3,pdiff1(f,2),u).z - SVF1(3,pdiff1(f,2),u).z0
= L.(z-z0) + R.(z-z0) by A10;
then L.(z-z0) + R.(z-z0) = L1.(z-z0) + R1.(z-z0) by A13,A18,A20;
then r1*(z-z0) + R.(z-z0) = L1.(z-z0) + R1.(z-z0) by A14;
hence r*(z-z0) + R.(z-z0) = s*(z-z0) + R1.(z-z0) by A15,A16,A17;
end;
consider N0 be Neighbourhood of z0 such that
A21: N0 c= N & N0 c= N1 by A18,RCOMP_1:38;
consider g be real number such that
A22: 0 < g & N0 = ].z0-g,z0+g.[ by RCOMP_1:def 7;
deffunc F(Element of NAT) = g/($1+2);
consider s1 such that
A23: for n holds s1.n = F(n) from SEQ_1:sch 1;
now let n;
g/(n+2) <> 0 by A22,XREAL_1:141;
hence s1.n <> 0 by A23;
end; then
A24: s1 is non-zero by SEQ_1:7;
s1 is convergent & lim s1 = 0 by A23,SEQ_4:46;
then reconsider h = s1 as convergent_to_0 Real_Sequence
by A24,FDIFF_1:def 1;
A25: for n ex z st z in N & z in N1 & h.n = z-z0
proof
let n;
A26: g/(n+2) > 0 by A22,XREAL_1:141;
0+1 < n+1+1 by XREAL_1:8;
then g/(n+2) < g/1 by A22,XREAL_1:78;then
A27: z0+g/(n+2) < z0+g by XREAL_1:8;
z0+-g < z0+g/(n+2) by A22,A26,XREAL_1:8;
then A28: z0+g/(n+2) in ].z0-g,z0+g.[ by A27;
take z0+g/(n+2);
thus thesis by A21,A22,A23,A28;
end;
A29: now let n be Nat;
A30: n in NAT by ORDINAL1:def 13; then
ex z st z in N & z in N1 & h.n = z-z0 by A25;then
A31: r*(h.n) + R.(h.n) = s*(h.n) + R1.(h.n) by A19;
h is non-zero by FDIFF_1:def 1;then
A32: h.n <> 0 by SEQ_1:7,A30;
A33: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (s*(h.n) + R1.(h.n))/(h.n)
by A31,XCMPLX_1:63;
A34: (r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:75
.= r*1 by A32,XCMPLX_1:60
.= r;
(s*(h.n))/(h.n) = s*((h.n)/(h.n)) by XCMPLX_1:75
.= s*1 by A32,XCMPLX_1:60
.= s;then
A35: r + (R.(h.n))/(h.n) = s + (R1.(h.n))/(h.n) by A33,A34,XCMPLX_1:63;
dom R = REAL by PARTFUN1:def 4;then
A36: rng h c= dom R;
dom R1 = REAL by PARTFUN1:def 4;then
A37: rng h c= dom R1;
A38: (R.(h.n))/(h.n) = (R.(h.n))*(h.n)" by XCMPLX_0:def 9
.= (R.(h.n))*(h".n) by VALUED_1:10
.= ((R/*h).n)*(h".n) by A36,FUNCT_2:185,A30
.= ((h")(#)(R/*h)).n by VALUED_1:5;
(R1.(h.n))/(h.n) = (R1.(h.n))*(h.n)" by XCMPLX_0:def 9
.= (R1.(h.n))*(h".n) by VALUED_1:10
.= ((R1/*h).n)*(h".n) by A37,FUNCT_2:185,A30
.= ((h")(#)(R1/*h)).n by VALUED_1:5;
then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by A35,A38;
hence r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n by RFUNCT_2:6,A30;
end; then
A39: ((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant by VALUED_0:def 18;
(((h")(#)(R1/*h))-((h")(#)(R/*h))).1 = r-s by A29;then
A40: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-s by A39,SEQ_4:40;
A41: (h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0 by FDIFF_1:def 3;
(h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by FDIFF_1:def 3;
then r-s = 0-0 by A40,A41,SEQ_2:26;
hence thesis;
end;
end;
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 :Def16:
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,R st it = L.1 & for x 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
proof
consider x0,y0,z0 being Real such that
A2: u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
N c= dom SVF1(1,pdiff1(f,3),u) & ex L,R st for x 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)
by A1,Def7;
consider N being Neighbourhood of x0 such that
A3: N c= dom SVF1(1,pdiff1(f,3),u) & ex L,R st for x 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)
by A2;
consider L,R such that
A4: for x 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)
by A3;
consider r such that
A5: for p holds L.p = r*p by FDIFF_1:def 4;
take r;
L.1 = r*1 by A5
.= r;
hence thesis by A2,A3,A4;
end;
uniqueness
proof
let r,s;
assume that
A6: 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,R st r = L.1 & for x 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) and
A7: 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,R st s = L.1 & for x 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);
consider x0,y0,z0 being Real such that
A8: u = <*x0,y0,z0*> &
ex N being Neighbourhood of x0 st N c= dom SVF1(1,pdiff1(f,3),u) &
ex L,R st r = L.1 & for x 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)
by A6;
consider N being Neighbourhood of x0 such that
A9: N c= dom SVF1(1,pdiff1(f,3),u) & ex L,R st r = L.1 & for x 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) by A8;
consider L,R such that
A10: r = L.1 & for x 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) by A9;
consider x1,y1, z1 being Real such that
A11: u = <*x1,y1, z1*> &
ex N being Neighbourhood of x1 st N c= dom SVF1(1,pdiff1(f,3),u) &
ex L,R st s = L.1 & for x st x in N holds
SVF1(1,pdiff1(f,3),u).x - SVF1(1,pdiff1(f,3),u).x1
= L.(x-x1) + R.(x-x1) by A7;
consider N1 being Neighbourhood of x1 such that
A12: N1 c= dom SVF1(1,pdiff1(f,3),u) &
ex L,R st s = L.1 & for x st x in N1 holds
SVF1(1,pdiff1(f,3),u).x - SVF1(1,pdiff1(f,3),u).x1
= L.(x-x1) + R.(x-x1) by A11;
consider L1,R1 such that
A13: s = L1.1 & for x st x in N1 holds
SVF1(1,pdiff1(f,3),u).x - SVF1(1,pdiff1(f,3),u).x1
= L1.(x-x1) + R1.(x-x1) by A12;
consider r1 such that
A14: for p holds L.p = r1*p by FDIFF_1:def 4;
consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 4;
A16: r = r1*1 by A10,A14;
A17: s = p1*1 by A13,A15;
A18: x0 = x1 & y0 = y1 & z0 = z1 by A8,A11,FINSEQ_1:99;
A19: now let x;
assume
A20: x in N & x in N1;
then SVF1(1,pdiff1(f,3),u).x - SVF1(1,pdiff1(f,3),u).x0
= L.(x-x0) + R.(x-x0) by A10;
then L.(x-x0) + R.(x-x0) = L1.(x-x0) + R1.(x-x0) by A13,A18,A20;
then r1*(x-x0) + R.(x-x0) = L1.(x-x0) + R1.(x-x0) by A14;
hence r*(x-x0) + R.(x-x0) = s*(x-x0) + R1.(x-x0) by A15,A16,A17;
end;
consider N0 be Neighbourhood of x0 such that
A21: N0 c= N & N0 c= N1 by A18,RCOMP_1:38;
consider g be real number such that
A22: 0 < g & N0 = ].x0-g,x0+g.[ by RCOMP_1:def 7;
deffunc F(Element of NAT) = g/($1+2);
consider s1 such that
A23: for n holds s1.n = F(n) from SEQ_1:sch 1;
now let n;
g/(n+2) <> 0 by A22,XREAL_1:141;
hence s1.n <> 0 by A23;
end; then
A24: s1 is non-zero by SEQ_1:7;
s1 is convergent & lim s1 = 0 by A23,SEQ_4:46;
then reconsider h = s1 as convergent_to_0 Real_Sequence
by A24,FDIFF_1:def 1;
A25: for n ex x st x in N & x in N1 & h.n = x-x0
proof
let n;
A26: g/(n+2) > 0 by A22,XREAL_1:141;
0+1 < n+1+1 by XREAL_1:8;
then g/(n+2) < g/1 by A22,XREAL_1:78;then
A27: x0+g/(n+2) < x0+g by XREAL_1:8;
x0+-g < x0+g/(n+2) by A22,A26,XREAL_1:8;
then A28: x0+g/(n+2) in ].x0-g,x0+g.[ by A27;
take x0+g/(n+2);
thus thesis by A21,A22,A23,A28;
end;
A29: now let n be Nat;
A30: n in NAT by ORDINAL1:def 13; then
ex x st x in N & x in N1 & h.n = x-x0 by A25;then
A31: r*(h.n) + R.(h.n) = s*(h.n) + R1.(h.n) by A19;
h is non-zero by FDIFF_1:def 1;then
A32: h.n <> 0 by A30,SEQ_1:7;
A33: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (s*(h.n) + R1.(h.n))/(h.n)
by A31,XCMPLX_1:63;
A34: (r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:75
.= r*1 by A32,XCMPLX_1:60
.= r;
(s*(h.n))/(h.n) = s*((h.n)/(h.n)) by XCMPLX_1:75
.= s*1 by A32,XCMPLX_1:60
.= s;then
A35: r + (R.(h.n))/(h.n) = s + (R1.(h.n))/(h.n) by A33,A34,XCMPLX_1:63;
dom R = REAL by PARTFUN1:def 4;then
A36: rng h c= dom R;
dom R1 = REAL by PARTFUN1:def 4;then
A37: rng h c= dom R1;
A38: (R.(h.n))/(h.n) = (R.(h.n))*(h.n)" by XCMPLX_0:def 9
.= (R.(h.n))*(h".n) by VALUED_1:10
.= ((R/*h).n)*(h".n) by A36,FUNCT_2:185,A30
.= ((h")(#)(R/*h)).n by VALUED_1:5;
(R1.(h.n))/(h.n) = (R1.(h.n))*(h.n)" by XCMPLX_0:def 9
.= (R1.(h.n))*(h".n) by VALUED_1:10
.= ((R1/*h).n)*(h".n) by A37,FUNCT_2:185,A30
.= ((h")(#)(R1/*h)).n by VALUED_1:5;
then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by A35,A38;
hence r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n by VALUED_1:15,A30;
end; then
A39: ((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant by VALUED_0:def 18;
(((h")(#)(R1/*h))-((h")(#)(R/*h))).1 = r-s by A29;then
A40: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-s by A39,SEQ_4:40;
A41: (h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0 by FDIFF_1:def 3;
(h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by FDIFF_1:def 3;
then r-s = 0-0 by A40,A41,SEQ_2:26;
hence thesis;
end;
end;
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 :Def17:
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,R st it = L.1 & for y 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
proof
consider x0,y0,z0 being Real such that
A2: u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
N c= dom SVF1(2,pdiff1(f,3),u) & ex L,R st for y 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)
by A1,Def8;
consider N being Neighbourhood of y0 such that
A3: N c= dom SVF1(2,pdiff1(f,3),u) & ex L,R st for y 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)
by A2;
consider L,R such that
A4: for y 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)
by A3;
consider r such that
A5: for p holds L.p = r*p by FDIFF_1:def 4;
take r;
L.1 = r*1 by A5 .= r;
hence thesis by A2,A3,A4;
end;
uniqueness
proof
let r,s;
assume that
A6: 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,R st r = L.1 & for y 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) and
A7: 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,R st s = L.1 & for y 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);
consider x0,y0,z0 being Real such that
A8: u = <*x0,y0,z0*> &
ex N being Neighbourhood of y0 st N c= dom SVF1(2,pdiff1(f,3),u) &
ex L,R st r = L.1 & for y 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)
by A6;
consider N being Neighbourhood of y0 such that
A9: N c= dom SVF1(2,pdiff1(f,3),u) & ex L,R st r = L.1 & for y 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) by A8;
consider L,R such that
A10: r = L.1 & for y 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) by A9;
consider x1,y1, z1 being Real such that
A11: u = <*x1,y1, z1*> &
ex N being Neighbourhood of y1 st N c= dom SVF1(2,pdiff1(f,3),u) &
ex L,R st s = L.1 & for y st y in N holds
SVF1(2,pdiff1(f,3),u).y - SVF1(2,pdiff1(f,3),u).y1
= L.(y-y1) + R.(y-y1) by A7;
consider N1 being Neighbourhood of y1 such that
A12: N1 c= dom SVF1(2,pdiff1(f,3),u) &
ex L,R st s = L.1 & for y st y in N1 holds
SVF1(2,pdiff1(f,3),u).y - SVF1(2,pdiff1(f,3),u).y1
= L.(y-y1) + R.(y-y1) by A11;
consider L1,R1 such that
A13: s = L1.1 & for y st y in N1 holds
SVF1(2,pdiff1(f,3),u).y - SVF1(2,pdiff1(f,3),u).y1
= L1.(y-y1) + R1.(y-y1) by A12;
consider r1 such that
A14: for p holds L.p = r1*p by FDIFF_1:def 4;
consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 4;
A16: r = r1*1 by A10,A14;
A17: s = p1*1 by A13,A15;
A18: x0 = x1 & y0 = y1 & z0 = z1 by A8,A11,FINSEQ_1:99;
A19: now let y;
assume
A20: y in N & y in N1;
then SVF1(2,pdiff1(f,3),u).y - SVF1(2,pdiff1(f,3),u).y0
= L.(y-y0) + R.(y-y0) by A10;
then L.(y-y0) + R.(y-y0) = L1.(y-y0) + R1.(y-y0) by A13,A18,A20;
then r1*(y-y0) + R.(y-y0) = L1.(y-y0) + R1.(y-y0) by A14;
hence r*(y-y0) + R.(y-y0) = s*(y-y0) + R1.(y-y0) by A15,A16,A17;
end;
consider N0 be Neighbourhood of y0 such that
A21: N0 c= N & N0 c= N1 by A18,RCOMP_1:38;
consider g be real number such that
A22: 0 < g & N0 = ].y0-g,y0+g.[ by RCOMP_1:def 7;
deffunc F(Element of NAT) = g/($1+2);
consider s1 such that
A23: for n holds s1.n = F(n) from SEQ_1:sch 1;
now let n;
g/(n+2) <> 0 by A22,XREAL_1:141;
hence s1.n <> 0 by A23;
end; then
A24: s1 is non-zero by SEQ_1:7;
s1 is convergent & lim s1 = 0 by A23,SEQ_4:46;
then reconsider h = s1 as convergent_to_0 Real_Sequence
by A24,FDIFF_1:def 1;
A25: for n ex y st y in N & y in N1 & h.n = y-y0
proof
let n;
A26: g/(n+2) > 0 by A22,XREAL_1:141;
0+1 < n+1+1 by XREAL_1:8;
then g/(n+2) < g/1 by A22,XREAL_1:78;then
A27: y0+g/(n+2) < y0+g by XREAL_1:8;
y0+-g < y0+g/(n+2) by A22,A26,XREAL_1:8;
then A28: y0+g/(n+2) in ].y0-g,y0+g.[ by A27;
take y0+g/(n+2);
thus thesis by A21,A22,A23,A28;
end;
A29: now let n be Nat;
A30: n in NAT by ORDINAL1:def 13; then
ex y st y in N & y in N1 & h.n = y-y0 by A25;then
A31: r*(h.n) + R.(h.n) = s*(h.n) + R1.(h.n) by A19;
h is non-zero by FDIFF_1:def 1;then
A32: h.n <> 0 by SEQ_1:7,A30;
A33: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (s*(h.n) + R1.(h.n))/(h.n)
by A31,XCMPLX_1:63;
A34: (r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:75
.= r*1 by A32,XCMPLX_1:60
.= r;
(s*(h.n))/(h.n) = s*((h.n)/(h.n)) by XCMPLX_1:75
.= s*1 by A32,XCMPLX_1:60
.= s;then
A35: r + (R.(h.n))/(h.n) = s + (R1.(h.n))/(h.n) by A33,A34,XCMPLX_1:63;
dom R = REAL by PARTFUN1:def 4;then
A36: rng h c= dom R;
dom R1 = REAL by PARTFUN1:def 4;then
A37: rng h c= dom R1;
A38: (R.(h.n))/(h.n) = (R.(h.n))*(h.n)" by XCMPLX_0:def 9
.= (R.(h.n))*(h".n) by VALUED_1:10
.= ((R/*h).n)*(h".n) by A36,FUNCT_2:185,A30
.= ((h")(#)(R/*h)).n by VALUED_1:5;
(R1.(h.n))/(h.n) = (R1.(h.n))*(h.n)" by XCMPLX_0:def 9
.= (R1.(h.n))*(h".n) by VALUED_1:10
.= ((R1/*h).n)*(h".n) by A37,FUNCT_2:185,A30
.= ((h")(#)(R1/*h)).n by VALUED_1:5;
then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by A35,A38;
hence r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n by RFUNCT_2:6,A30;
end; then
A39: ((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant by VALUED_0:def 18;
(((h")(#)(R1/*h))-((h")(#)(R/*h))).1 = r-s by A29;then
A40: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-s by A39,SEQ_4:40;
A41: (h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0 by FDIFF_1:def 3;
(h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by FDIFF_1:def 3;
then r-s = 0-0 by A40,A41,SEQ_2:26;
hence thesis;
end;
end;
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 :Def18:
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,R st it = L.1 & for z 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
proof
consider x0,y0,z0 being Real such that
A2: u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
N c= dom SVF1(3,pdiff1(f,3),u) & ex L,R st for z 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)
by A1,Def9;
consider N being Neighbourhood of z0 such that
A3: N c= dom SVF1(3,pdiff1(f,3),u) & ex L,R st for z 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)
by A2;
consider L,R such that
A4: for z 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)
by A3;
consider r such that
A5: for p holds L.p = r*p by FDIFF_1:def 4;
take r;
L.1 = r*1 by A5 .= r;
hence thesis by A2,A3,A4;
end;
uniqueness
proof
let r,s;
assume that
A6: 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,R st r = L.1 & for z 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) and
A7: 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,R st s = L.1 & for z 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);
consider x0,y0,z0 being Real such that
A8: u = <*x0,y0,z0*> &
ex N being Neighbourhood of z0 st N c= dom SVF1(3,pdiff1(f,3),u) &
ex L,R st r = L.1 & for z 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)
by A6;
consider N being Neighbourhood of z0 such that
A9: N c= dom SVF1(3,pdiff1(f,3),u) & ex L,R st r = L.1 & for z 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) by A8;
consider L,R such that
A10: r = L.1 & for z 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) by A9;
consider x1,y1,z1 being Real such that
A11: u = <*x1,y1,z1*> &
ex N being Neighbourhood of z1 st N c= dom SVF1(3,pdiff1(f,3),u) &
ex L,R st s = L.1 & for z st z in N holds
SVF1(3,pdiff1(f,3),u).z - SVF1(3,pdiff1(f,3),u).z1
= L.(z-z1) + R.(z-z1) by A7;
consider N1 being Neighbourhood of z1 such that
A12: N1 c= dom SVF1(3,pdiff1(f,3),u) &
ex L,R st s = L.1 & for z st z in N1 holds
SVF1(3,pdiff1(f,3),u).z - SVF1(3,pdiff1(f,3),u).z1
= L.(z-z1) + R.(z-z1) by A11;
consider L1,R1 such that
A13: s = L1.1 & for z st z in N1 holds
SVF1(3,pdiff1(f,3),u).z - SVF1(3,pdiff1(f,3),u).z1
= L1.(z-z1) + R1.(z-z1) by A12;
consider r1 such that
A14: for p holds L.p = r1*p by FDIFF_1:def 4;
consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 4;
A16: r = r1*1 by A10,A14;
A17: s = p1*1 by A13,A15;
A18: x0 = x1 & y0 = y1 & z0 = z1 by A8,A11,FINSEQ_1:99;
A19: now let z;
assume
A20: z in N & z in N1;
then SVF1(3,pdiff1(f,3),u).z - SVF1(3,pdiff1(f,3),u).z0
= L.(z-z0) + R.(z-z0) by A10;
then L.(z-z0) + R.(z-z0) = L1.(z-z0) + R1.(z-z0) by A13,A18,A20;
then r1*(z-z0) + R.(z-z0) = L1.(z-z0) + R1.(z-z0) by A14;
hence r*(z-z0) + R.(z-z0) = s*(z-z0) + R1.(z-z0) by A15,A16,A17;
end;
consider N0 be Neighbourhood of z0 such that
A21: N0 c= N & N0 c= N1 by A18,RCOMP_1:38;
consider g be real number such that
A22: 0 < g & N0 = ].z0-g,z0+g.[ by RCOMP_1:def 7;
deffunc F(Element of NAT) = g/($1+2);
consider s1 such that
A23: for n holds s1.n = F(n) from SEQ_1:sch 1;
now let n;
g/(n+2) <> 0 by A22,XREAL_1:141;
hence s1.n <> 0 by A23;
end; then
A24: s1 is non-zero by SEQ_1:7;
s1 is convergent & lim s1 = 0 by A23,SEQ_4:46;
then reconsider h = s1 as convergent_to_0 Real_Sequence
by A24,FDIFF_1:def 1;
A25: for n ex z st z in N & z in N1 & h.n = z-z0
proof
let n;
A26: g/(n+2) > 0 by A22,XREAL_1:141;
0+1 < n+1+1 by XREAL_1:8;
then g/(n+2) < g/1 by A22,XREAL_1:78;then
A27: z0+g/(n+2) < z0+g by XREAL_1:8;
z0+-g < z0+g/(n+2) by A22,A26,XREAL_1:8;
then A28: z0+g/(n+2) in ].z0-g,z0+g.[ by A27;
take z0+g/(n+2);
thus thesis by A21,A22,A23,A28;
end;
A29: now let n be Nat;
A30: n in NAT by ORDINAL1:def 13; then
ex z st z in N & z in N1 & h.n = z-z0 by A25;then
A31: r*(h.n) + R.(h.n) = s*(h.n) + R1.(h.n) by A19;
h is non-zero by FDIFF_1:def 1;then
A32: h.n <> 0 by SEQ_1:7,A30;
A33: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (s*(h.n) + R1.(h.n))/(h.n)
by A31,XCMPLX_1:63;
A34: (r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:75
.= r*1 by A32,XCMPLX_1:60
.= r;
(s*(h.n))/(h.n) = s*((h.n)/(h.n)) by XCMPLX_1:75
.= s*1 by A32,XCMPLX_1:60
.= s;then
A35: r + (R.(h.n))/(h.n) = s + (R1.(h.n))/(h.n) by A33,A34,XCMPLX_1:63;
dom R = REAL by PARTFUN1:def 4;then
A36: rng h c= dom R;
dom R1 = REAL by PARTFUN1:def 4;then
A37: rng h c= dom R1;
A38: (R.(h.n))/(h.n) = (R.(h.n))*(h.n)" by XCMPLX_0:def 9
.= (R.(h.n))*(h".n) by VALUED_1:10
.= ((R/*h).n)*(h".n) by A36,FUNCT_2:185,A30
.= ((h")(#)(R/*h)).n by VALUED_1:5;
(R1.(h.n))/(h.n) = (R1.(h.n))*(h.n)" by XCMPLX_0:def 9
.= (R1.(h.n))*(h".n) by VALUED_1:10
.= ((R1/*h).n)*(h".n) by A37,FUNCT_2:185,A30
.= ((h")(#)(R1/*h)).n by VALUED_1:5;
then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by A35,A38;
hence r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n by RFUNCT_2:6,A30;
end; then
A39: ((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant by VALUED_0:def 18;
(((h")(#)(R1/*h))-((h")(#)(R/*h))).1 = r-s by A29;then
A40: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-s by A39,SEQ_4:40;
A41: (h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0 by FDIFF_1:def 3;
(h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by FDIFF_1:def 3;
then r-s = 0-0 by A40,A41,SEQ_2:26;
hence thesis;
end;
end;
theorem
u = <*x0,y0,z0*> & f is_hpartial_differentiable`11_in u implies
SVF1(1,pdiff1(f,1),u) is_differentiable_in x0
proof
assume that
A1: u = <*x0,y0,z0*> and
A2: f is_hpartial_differentiable`11_in u;
consider x1,y1,z1 such that
A3: u = <*x1,y1,z1*> & ex N being Neighbourhood of x1 st
N c= dom SVF1(1,pdiff1(f,1),u) & ex L,R st for x st x in N holds
SVF1(1,pdiff1(f,1),u).x - SVF1(1,pdiff1(f,1),u).x1 = L.(x-x1) + R.(x-x1)
by A2,Def1;
x0 = x1 by A1,A3,FINSEQ_1:99;
hence thesis by A3,FDIFF_1:def 5;
end;
theorem
u = <*x0,y0,z0*> & f is_hpartial_differentiable`12_in u implies
SVF1(2,pdiff1(f,1),u) is_differentiable_in y0
proof
assume that
A1: u = <*x0,y0,z0*> and
A2: f is_hpartial_differentiable`12_in u;
consider x1,y1,z1 such that
A3: u = <*x1,y1,z1*> & ex N being Neighbourhood of y1 st
N c= dom SVF1(2,pdiff1(f,1),u) & ex L,R st for y st y in N holds
SVF1(2,pdiff1(f,1),u).y - SVF1(2,pdiff1(f,1),u).y1 = L.(y-y1) + R.(y-y1)
by A2,Def2;
y0 = y1 by A1,A3,FINSEQ_1:99;
hence thesis by A3,FDIFF_1:def 5;
end;
theorem
u = <*x0,y0,z0*> & f is_hpartial_differentiable`13_in u implies
SVF1(3,pdiff1(f,1),u) is_differentiable_in z0
proof
assume that
A1: u = <*x0,y0,z0*> and
A2: f is_hpartial_differentiable`13_in u;
consider x1,y1,z1 such that
A3: u = <*x1,y1,z1*> & ex N being Neighbourhood of z1 st
N c= dom SVF1(3,pdiff1(f,1),u) & ex L,R st for z st z in N holds
SVF1(3,pdiff1(f,1),u).z - SVF1(3,pdiff1(f,1),u).z1 = L.(z-z1) + R.(z-z1)
by A2,Def3;
z0 = z1 by A1,A3,FINSEQ_1:99;
hence thesis by A3,FDIFF_1:def 5;
end;
theorem
u = <*x0,y0,z0*> & f is_hpartial_differentiable`21_in u implies
SVF1(1,pdiff1(f,2),u) is_differentiable_in x0
proof
assume that
A1: u = <*x0,y0,z0*> and
A2: f is_hpartial_differentiable`21_in u;
consider x1,y1,z1 such that
A3: u = <*x1,y1,z1*> & ex N being Neighbourhood of x1 st
N c= dom SVF1(1,pdiff1(f,2),u) & ex L,R st for x st x in N holds
SVF1(1,pdiff1(f,2),u).x - SVF1(1,pdiff1(f,2),u).x1 = L.(x-x1) + R.(x-x1)
by A2,Def4;
x0 = x1 by A1,A3,FINSEQ_1:99;
hence thesis by A3,FDIFF_1:def 5;
end;
theorem
u = <*x0,y0,z0*> & f is_hpartial_differentiable`22_in u implies
SVF1(2,pdiff1(f,2),u) is_differentiable_in y0
proof
assume that
A1: u = <*x0,y0,z0*> and
A2: f is_hpartial_differentiable`22_in u;
consider x1,y1,z1 such that
A3: u = <*x1,y1,z1*> & ex N being Neighbourhood of y1 st
N c= dom SVF1(2,pdiff1(f,2),u) & ex L,R st for y st y in N holds
SVF1(2,pdiff1(f,2),u).y - SVF1(2,pdiff1(f,2),u).y1 = L.(y-y1) + R.(y-y1)
by A2,Def5;
y0 = y1 by A1,A3,FINSEQ_1:99;
hence thesis by A3,FDIFF_1:def 5;
end;
theorem
u = <*x0,y0,z0*> & f is_hpartial_differentiable`23_in u implies
SVF1(3,pdiff1(f,2),u) is_differentiable_in z0
proof
assume that
A1: u = <*x0,y0,z0*> and
A2: f is_hpartial_differentiable`23_in u;
consider x1,y1,z1 such that
A3: u = <*x1,y1,z1*> & ex N being Neighbourhood of z1 st
N c= dom SVF1(3,pdiff1(f,2),u) & ex L,R st for z st z in N holds
SVF1(3,pdiff1(f,2),u).z - SVF1(3,pdiff1(f,2),u).z1 = L.(z-z1) + R.(z-z1)
by A2,Def6;
z0 = z1 by A1,A3,FINSEQ_1:99;
hence thesis by A3,FDIFF_1:def 5;
end;
theorem
u = <*x0,y0,z0*> & f is_hpartial_differentiable`31_in u implies
SVF1(1,pdiff1(f,3),u) is_differentiable_in x0
proof
assume that
A1: u = <*x0,y0,z0*> and
A2: f is_hpartial_differentiable`31_in u;
consider x1,y1,z1 such that
A3: u = <*x1,y1,z1*> & ex N being Neighbourhood of x1 st
N c= dom SVF1(1,pdiff1(f,3),u) & ex L,R st for x st x in N holds
SVF1(1,pdiff1(f,3),u).x - SVF1(1,pdiff1(f,3),u).x1 = L.(x-x1) + R.(x-x1)
by A2,Def7;
x0 = x1 by A1,A3,FINSEQ_1:99;
hence thesis by A3,FDIFF_1:def 5;
end;
theorem
u = <*x0,y0,z0*> & f is_hpartial_differentiable`32_in u implies
SVF1(2,pdiff1(f,3),u) is_differentiable_in y0
proof
assume that
A1: u = <*x0,y0,z0*> and
A2: f is_hpartial_differentiable`32_in u;
consider x1,y1,z1 such that
A3: u = <*x1,y1,z1*> & ex N being Neighbourhood of y1 st
N c= dom SVF1(2,pdiff1(f,3),u) & ex L,R st for y st y in N holds
SVF1(2,pdiff1(f,3),u).y - SVF1(2,pdiff1(f,3),u).y1 = L.(y-y1) + R.(y-y1)
by A2,Def8;
y0 = y1 by A1,A3,FINSEQ_1:99;
hence thesis by A3,FDIFF_1:def 5;
end;
theorem
u = <*x0,y0,z0*> & f is_hpartial_differentiable`33_in u implies
SVF1(3,pdiff1(f,3),u) is_differentiable_in z0
proof
assume that
A1: u = <*x0,y0,z0*> and
A2: f is_hpartial_differentiable`33_in u;
consider x1,y1,z1 such that
A3: u = <*x1,y1,z1*> & ex N being Neighbourhood of z1 st
N c= dom SVF1(3,pdiff1(f,3),u) & ex L,R st for z st z in N holds
SVF1(3,pdiff1(f,3),u).z - SVF1(3,pdiff1(f,3),u).z1 = L.(z-z1) + R.(z-z1)
by A2,Def9;
z0 = z1 by A1,A3,FINSEQ_1:99;
hence thesis by A3,FDIFF_1:def 5;
end;
theorem Th10:
u = <*x0,y0,z0*> & f is_hpartial_differentiable`11_in u implies
hpartdiff11(f,u) = diff(SVF1(1,pdiff1(f,1),u),x0)
proof
set r = hpartdiff11(f,u);
assume that
A1: u = <*x0,y0,z0*> and
A2: f is_hpartial_differentiable`11_in u;
consider x1,y1,z1 being Real such that
A3: u = <*x1,y1,z1*> & ex N being Neighbourhood of x1 st
N c= dom SVF1(1,pdiff1(f,1),u) & ex L,R st for x st x in N holds
SVF1(1,pdiff1(f,1),u).x - SVF1(1,pdiff1(f,1),u).x1 = L.(x-x1) + R.(x-x1)
by A2,Def1;
consider N being Neighbourhood of x1 such that
A4: N c= dom SVF1(1,pdiff1(f,1),u) & ex L,R st for x st x in N holds
SVF1(1,pdiff1(f,1),u).x - SVF1(1,pdiff1(f,1),u).x1 = L.(x-x1) + R.(x-x1)
by A3;
consider L,R such that
A5: for x st x in N holds
SVF1(1,pdiff1(f,1),u).x - SVF1(1,pdiff1(f,1),u).x1 = L.(x-x1) + R.(x-x1)
by A4;
A6: x0 = x1 & y0 = y1 & z0 = z1 by A1,A3,FINSEQ_1:99;
A7: r = L.1 by A2,A3,A4,A5,Def10;
SVF1(1,pdiff1(f,1),u) is_differentiable_in x0 by A4,A6,FDIFF_1:def 5;
hence thesis by A4,A5,A6,A7,FDIFF_1:def 6;
end;
theorem Th11:
u = <*x0,y0,z0*> & f is_hpartial_differentiable`12_in u implies
hpartdiff12(f,u) = diff(SVF1(2,pdiff1(f,1),u),y0)
proof
set r = hpartdiff12(f,u);
assume that
A1: u = <*x0,y0,z0*> and
A2: f is_hpartial_differentiable`12_in u;
consider x1,y1,z1 being Real such that
A3: u = <*x1,y1,z1*> & ex N being Neighbourhood of y1 st
N c= dom SVF1(2,pdiff1(f,1),u) & ex L,R st for y st y in N holds
SVF1(2,pdiff1(f,1),u).y - SVF1(2,pdiff1(f,1),u).y1 = L.(y-y1) + R.(y-y1)
by A2,Def2;
consider N being Neighbourhood of y1 such that
A4: N c= dom SVF1(2,pdiff1(f,1),u) & ex L,R st for y st y in N holds
SVF1(2,pdiff1(f,1),u).y - SVF1(2,pdiff1(f,1),u).y1 = L.(y-y1) + R.(y-y1)
by A3;
consider L,R such that
A5: for y st y in N holds
SVF1(2,pdiff1(f,1),u).y - SVF1(2,pdiff1(f,1),u).y1 = L.(y-y1) + R.(y-y1)
by A4;
A6: x0 = x1 & y0 = y1 & z0 = z1 by A1,A3,FINSEQ_1:99;
A7: r = L.1 by A2,A3,A4,A5,Def11;
SVF1(2,pdiff1(f,1),u) is_differentiable_in y0 by A4,A6,FDIFF_1:def 5;
hence thesis by A4,A5,A6,A7,FDIFF_1:def 6;
end;
theorem Th12:
u = <*x0,y0,z0*> & f is_hpartial_differentiable`13_in u implies
hpartdiff13(f,u) = diff(SVF1(3,pdiff1(f,1),u),z0)
proof
set r = hpartdiff13(f,u);
assume that
A1: u = <*x0,y0,z0*> and
A2: f is_hpartial_differentiable`13_in u;
consider x1,y1,z1 being Real such that
A3: u = <*x1,y1,z1*> & ex N being Neighbourhood of z1 st
N c= dom SVF1(3,pdiff1(f,1),u) & ex L,R st for z st z in N holds
SVF1(3,pdiff1(f,1),u).z - SVF1(3,pdiff1(f,1),u).z1 = L.(z-z1) + R.(z-z1)
by A2,Def3;
consider N being Neighbourhood of z1 such that
A4: N c= dom SVF1(3,pdiff1(f,1),u) & ex L,R st for z st z in N holds
SVF1(3,pdiff1(f,1),u).z - SVF1(3,pdiff1(f,1),u).z1 = L.(z-z1) + R.(z-z1)
by A3;
consider L,R such that
A5: for z st z in N holds
SVF1(3,pdiff1(f,1),u).z - SVF1(3,pdiff1(f,1),u).z1 = L.(z-z1) + R.(z-z1)
by A4;
A6: x0 = x1 & y0 = y1 & z0 = z1 by A1,A3,FINSEQ_1:99;
A7: r = L.1 by A2,A3,A4,A5,Def12;
SVF1(3,pdiff1(f,1),u) is_differentiable_in z0 by A4,A6,FDIFF_1:def 5;
hence thesis by A4,A5,A6,A7,FDIFF_1:def 6;
end;
theorem Th13:
u = <*x0,y0,z0*> & f is_hpartial_differentiable`21_in u implies
hpartdiff21(f,u) = diff(SVF1(1,pdiff1(f,2),u),x0)
proof
set r = hpartdiff21(f,u);
assume that
A1: u = <*x0,y0,z0*> and
A2: f is_hpartial_differentiable`21_in u;
consider x1,y1,z1 being Real such that
A3: u = <*x1,y1,z1*> & ex N being Neighbourhood of x1 st
N c= dom SVF1(1,pdiff1(f,2),u) & ex L,R st for x st x in N holds
SVF1(1,pdiff1(f,2),u).x - SVF1(1,pdiff1(f,2),u).x1 = L.(x-x1) + R.(x-x1)
by A2,Def4;
consider N being Neighbourhood of x1 such that
A4: N c= dom SVF1(1,pdiff1(f,2),u) & ex L,R st for x st x in N holds
SVF1(1,pdiff1(f,2),u).x - SVF1(1,pdiff1(f,2),u).x1 = L.(x-x1) + R.(x-x1)
by A3;
consider L,R such that
A5: for x st x in N holds
SVF1(1,pdiff1(f,2),u).x - SVF1(1,pdiff1(f,2),u).x1 = L.(x-x1) + R.(x-x1)
by A4;
A6: x0 = x1 & y0 = y1 & z0 = z1 by A1,A3,FINSEQ_1:99;
A7: r = L.1 by A2,A3,A4,A5,Def13;
SVF1(1,pdiff1(f,2),u) is_differentiable_in x0 by A4,A6,FDIFF_1:def 5;
hence thesis by A4,A5,A6,A7,FDIFF_1:def 6;
end;
theorem Th14:
u = <*x0,y0,z0*> & f is_hpartial_differentiable`22_in u implies
hpartdiff22(f,u) = diff(SVF1(2,pdiff1(f,2),u),y0)
proof
set r = hpartdiff22(f,u);
assume that
A1: u = <*x0,y0,z0*> and
A2: f is_hpartial_differentiable`22_in u;
consider x1,y1,z1 being Real such that
A3: u = <*x1,y1,z1*> & ex N being Neighbourhood of y1 st
N c= dom SVF1(2,pdiff1(f,2),u) & ex L,R st for y st y in N holds
SVF1(2,pdiff1(f,2),u).y - SVF1(2,pdiff1(f,2),u).y1 = L.(y-y1) + R.(y-y1)
by A2,Def5;
consider N being Neighbourhood of y1 such that
A4: N c= dom SVF1(2,pdiff1(f,2),u) & ex L,R st for y st y in N holds
SVF1(2,pdiff1(f,2),u).y - SVF1(2,pdiff1(f,2),u).y1 = L.(y-y1) + R.(y-y1)
by A3;
consider L,R such that
A5: for y st y in N holds
SVF1(2,pdiff1(f,2),u).y - SVF1(2,pdiff1(f,2),u).y1 = L.(y-y1) + R.(y-y1)
by A4;
A6: x0 = x1 & y0 = y1 & z0 = z1 by A1,A3,FINSEQ_1:99;
A7: r = L.1 by A2,A3,A4,A5,Def14;
SVF1(2,pdiff1(f,2),u) is_differentiable_in y0 by A4,A6,FDIFF_1:def 5;
hence thesis by A4,A5,A6,A7,FDIFF_1:def 6;
end;
theorem Th15:
u = <*x0,y0,z0*> & f is_hpartial_differentiable`23_in u implies
hpartdiff23(f,u) = diff(SVF1(3,pdiff1(f,2),u),z0)
proof
set r = hpartdiff23(f,u);
assume that
A1: u = <*x0,y0,z0*> and
A2: f is_hpartial_differentiable`23_in u;
consider x1,y1,z1 being Real such that
A3: u = <*x1,y1,z1*> & ex N being Neighbourhood of z1 st
N c= dom SVF1(3,pdiff1(f,2),u) & ex L,R st for z st z in N holds
SVF1(3,pdiff1(f,2),u).z - SVF1(3,pdiff1(f,2),u).z1 = L.(z-z1) + R.(z-z1)
by A2,Def6;
consider N being Neighbourhood of z1 such that
A4: N c= dom SVF1(3,pdiff1(f,2),u) & ex L,R st for z st z in N holds
SVF1(3,pdiff1(f,2),u).z - SVF1(3,pdiff1(f,2),u).z1 = L.(z-z1) + R.(z-z1)
by A3;
consider L,R such that
A5: for z st z in N holds
SVF1(3,pdiff1(f,2),u).z - SVF1(3,pdiff1(f,2),u).z1 = L.(z-z1) + R.(z-z1)
by A4;
A6: x0 = x1 & y0 = y1 & z0 = z1 by A1,A3,FINSEQ_1:99;
A7: r = L.1 by A2,A3,A4,A5,Def15;
SVF1(3,pdiff1(f,2),u) is_differentiable_in z0 by A4,A6,FDIFF_1:def 5;
hence thesis by A4,A5,A6,A7,FDIFF_1:def 6;
end;
theorem Th16:
u = <*x0,y0,z0*> & f is_hpartial_differentiable`31_in u implies
hpartdiff31(f,u) = diff(SVF1(1,pdiff1(f,3),u),x0)
proof
set r = hpartdiff31(f,u);
assume that
A1: u = <*x0,y0,z0*> and
A2: f is_hpartial_differentiable`31_in u;
consider x1,y1,z1 being Real such that
A3: u = <*x1,y1,z1*> & ex N being Neighbourhood of x1 st
N c= dom SVF1(1,pdiff1(f,3),u) & ex L,R st for x st x in N holds
SVF1(1,pdiff1(f,3),u).x - SVF1(1,pdiff1(f,3),u).x1 = L.(x-x1) + R.(x-x1)
by A2,Def7;
consider N being Neighbourhood of x1 such that
A4: N c= dom SVF1(1,pdiff1(f,3),u) & ex L,R st for x st x in N holds
SVF1(1,pdiff1(f,3),u).x - SVF1(1,pdiff1(f,3),u).x1 = L.(x-x1) + R.(x-x1)
by A3;
consider L,R such that
A5: for x st x in N holds
SVF1(1,pdiff1(f,3),u).x - SVF1(1,pdiff1(f,3),u).x1 = L.(x-x1) + R.(x-x1)
by A4;
A6: x0 = x1 & y0 = y1 & z0 = z1 by A1,A3,FINSEQ_1:99;
A7: r = L.1 by A2,A3,A4,A5,Def16;
SVF1(1,pdiff1(f,3),u) is_differentiable_in x0 by A4,A6,FDIFF_1:def 5;
hence thesis by A4,A5,A6,A7,FDIFF_1:def 6;
end;
theorem Th17:
u = <*x0,y0,z0*> & f is_hpartial_differentiable`32_in u implies
hpartdiff32(f,u) = diff(SVF1(2,pdiff1(f,3),u),y0)
proof
set r = hpartdiff32(f,u);
assume that
A1: u = <*x0,y0,z0*> and
A2: f is_hpartial_differentiable`32_in u;
consider x1,y1,z1 being Real such that
A3: u = <*x1,y1,z1*> & ex N being Neighbourhood of y1 st
N c= dom SVF1(2,pdiff1(f,3),u) & ex L,R st for y st y in N holds
SVF1(2,pdiff1(f,3),u).y - SVF1(2,pdiff1(f,3),u).y1 = L.(y-y1) + R.(y-y1)
by A2,Def8;
consider N being Neighbourhood of y1 such that
A4: N c= dom SVF1(2,pdiff1(f,3),u) & ex L,R st for y st y in N holds
SVF1(2,pdiff1(f,3),u).y - SVF1(2,pdiff1(f,3),u).y1 = L.(y-y1) + R.(y-y1)
by A3;
consider L,R such that
A5: for y st y in N holds
SVF1(2,pdiff1(f,3),u).y - SVF1(2,pdiff1(f,3),u).y1 = L.(y-y1) + R.(y-y1)
by A4;
A6: x0 = x1 & y0 = y1 & z0 = z1 by A1,A3,FINSEQ_1:99;
A7: r = L.1 by A2,A3,A4,A5,Def17;
SVF1(2,pdiff1(f,3),u) is_differentiable_in y0 by A4,A6,FDIFF_1:def 5;
hence thesis by A4,A5,A6,A7,FDIFF_1:def 6;
end;
theorem Th18:
u = <*x0,y0,z0*> & f is_hpartial_differentiable`33_in u implies
hpartdiff33(f,u) = diff(SVF1(3,pdiff1(f,3),u),z0)
proof
set r = hpartdiff33(f,u);
assume that
A1: u = <*x0,y0,z0*> and
A2: f is_hpartial_differentiable`33_in u;
consider x1,y1,z1 being Real such that
A3: u = <*x1,y1,z1*> & ex N being Neighbourhood of z1 st
N c= dom SVF1(3,pdiff1(f,3),u) & ex L,R st for z st z in N holds
SVF1(3,pdiff1(f,3),u).z - SVF1(3,pdiff1(f,3),u).z1 = L.(z-z1) + R.(z-z1)
by A2,Def9;
consider N being Neighbourhood of z1 such that
A4: N c= dom SVF1(3,pdiff1(f,3),u) & ex L,R st for z st z in N holds
SVF1(3,pdiff1(f,3),u).z - SVF1(3,pdiff1(f,3),u).z1 = L.(z-z1) + R.(z-z1)
by A3;
consider L,R such that
A5: for z st z in N holds
SVF1(3,pdiff1(f,3),u).z - SVF1(3,pdiff1(f,3),u).z1 = L.(z-z1) + R.(z-z1)
by A4;
A6: x0 = x1 & y0 = y1 & z0 = z1 by A1,A3,FINSEQ_1:99;
A7: r = L.1 by A2,A3,A4,A5,Def18;
SVF1(3,pdiff1(f,3),u) is_differentiable_in z0 by A4,A6,FDIFF_1:def 5;
hence thesis by A4,A5,A6,A7,FDIFF_1:def 6;
end;
definition
let f be PartFunc of REAL 3,REAL;
let D be set;
pred f is_hpartial_differentiable`11_on D means :Def19:
D c= dom f & for u be Element of REAL 3 st u in D holds
f|D is_hpartial_differentiable`11_in u;
pred f is_hpartial_differentiable`12_on D means :Def20:
D c= dom f & for u be Element of REAL 3 st u in D holds
f|D is_hpartial_differentiable`12_in u;
pred f is_hpartial_differentiable`13_on D means :Def21:
D c= dom f & for u be Element of REAL 3 st u in D holds
f|D is_hpartial_differentiable`13_in u;
pred f is_hpartial_differentiable`21_on D means :Def22:
D c= dom f & for u be Element of REAL 3 st u in D holds
f|D is_hpartial_differentiable`21_in u;
pred f is_hpartial_differentiable`22_on D means :Def23:
D c= dom f & for u be Element of REAL 3 st u in D holds
f|D is_hpartial_differentiable`22_in u;
pred f is_hpartial_differentiable`23_on D means :Def24:
D c= dom f & for u be Element of REAL 3 st u in D holds
f|D is_hpartial_differentiable`23_in u;
pred f is_hpartial_differentiable`31_on D means :Def25:
D c= dom f & for u be Element of REAL 3 st u in D holds
f|D is_hpartial_differentiable`31_in u;
pred f is_hpartial_differentiable`32_on D means :Def26:
D c= dom f & for u be Element of REAL 3 st u in D holds
f|D is_hpartial_differentiable`32_in u;
pred f is_hpartial_differentiable`33_on D means :Def27:
D c= dom f & for u be Element of REAL 3 st u in D holds
f|D is_hpartial_differentiable`33_in u;
end;
definition
let f be PartFunc of REAL 3,REAL;
let D be set;
assume A1: f is_hpartial_differentiable`11_on D;
func f`hpartial11|D -> PartFunc of REAL 3,REAL means
dom it = D & for u be Element of REAL 3 st u in D holds
it.u = hpartdiff11(f,u);
existence
proof
defpred P[Element of REAL 3] means $1 in D;
deffunc F(Element of REAL 3) = hpartdiff11(f,$1);
consider F being PartFunc of REAL 3,REAL such that
A2: (for u be Element of REAL 3 holds u in dom F iff P[u]) &
for u be Element of REAL 3 st u in dom F holds F.u = F(u)
from SEQ_1:sch 3;
take F;
for y be set st y in dom F holds y in D by A2;then
A3: dom F c= D by TARSKI:def 3;
now
let y be set such that
A4: y in D;
D c= dom f by A1,Def19;
then D is Subset of REAL 3 by XBOOLE_1:1;
hence y in dom F by A2,A4;
end;
then D c= dom F by TARSKI:def 3;
hence dom F = D by A3,XBOOLE_0:def 10;
hereby
let u be Element of REAL 3;
assume u in D;then
u in dom F by A2;
hence F.u = hpartdiff11(f,u) by A2;
end;
end;
uniqueness
proof
let F,G be PartFunc of REAL 3,REAL;
assume that
A5: dom F = D & for u be Element of REAL 3 st u in D holds
F.u = hpartdiff11(f,u) and
A6: dom G = D & for u be Element of REAL 3 st u in D holds
G.u = hpartdiff11(f,u);
now
let u be Element of REAL 3;
assume
A7: u in dom F;
then F.u = hpartdiff11(f,u) by A5;
hence F.u = G.u by A5,A6,A7;
end;
hence thesis by A5,A6,PARTFUN1:34;
end;
end;
definition
let f be PartFunc of REAL 3,REAL;
let D be set;
assume A1: f is_hpartial_differentiable`12_on D;
func f`hpartial12|D -> PartFunc of REAL 3,REAL means
dom it = D & for u be Element of REAL 3 st u in D holds
it.u = hpartdiff12(f,u);
existence
proof
defpred P[Element of REAL 3] means $1 in D;
deffunc F(Element of REAL 3) = hpartdiff12(f,$1);
consider F being PartFunc of REAL 3,REAL such that
A2: (for u be Element of REAL 3 holds u in dom F iff P[u]) &
for u be Element of REAL 3 st u in dom F holds F.u = F(u)
from SEQ_1:sch 3;
take F;
for y be set st y in dom F holds y in D by A2;then
A3: dom F c= D by TARSKI:def 3;
now
let y be set such that
A4: y in D;
D c= dom f by A1,Def20;
then D is Subset of REAL 3 by XBOOLE_1:1;
hence y in dom F by A2,A4;
end;
then D c= dom F by TARSKI:def 3;
hence dom F = D by A3,XBOOLE_0:def 10;
hereby
let u be Element of REAL 3;
assume u in D;then
u in dom F by A2;
hence F.u = hpartdiff12(f,u) by A2;
end;
end;
uniqueness
proof
let F,G be PartFunc of REAL 3,REAL;
assume that
A5: dom F = D & for u be Element of REAL 3 st u in D holds
F.u = hpartdiff12(f,u) and
A6: dom G = D & for u be Element of REAL 3 st u in D holds
G.u = hpartdiff12(f,u);
now
let u be Element of REAL 3;
assume
A7: u in dom F;
then F.u = hpartdiff12(f,u) by A5;
hence F.u = G.u by A5,A6,A7;
end;
hence thesis by A5,A6,PARTFUN1:34;
end;
end;
definition
let f be PartFunc of REAL 3,REAL;
let D be set;
assume A1: f is_hpartial_differentiable`13_on D;
func f`hpartial13|D -> PartFunc of REAL 3,REAL means
dom it = D & for u be Element of REAL 3 st u in D holds
it.u = hpartdiff13(f,u);
existence
proof
defpred P[Element of REAL 3] means $1 in D;
deffunc F(Element of REAL 3) = hpartdiff13(f,$1);
consider F being PartFunc of REAL 3,REAL such that
A2: (for u be Element of REAL 3 holds u in dom F iff P[u]) &
for u be Element of REAL 3 st u in dom F holds F.u = F(u)
from SEQ_1:sch 3;
take F;
for y be set st y in dom F holds y in D by A2;then
A3: dom F c= D by TARSKI:def 3;
now
let y be set such that
A4: y in D;
D c= dom f by A1,Def21;
then D is Subset of REAL 3 by XBOOLE_1:1;
hence y in dom F by A2,A4;
end;
then D c= dom F by TARSKI:def 3;
hence dom F = D by A3,XBOOLE_0:def 10;
hereby
let u be Element of REAL 3;
assume u in D;then
u in dom F by A2;
hence F.u = hpartdiff13(f,u) by A2;
end;
end;
uniqueness
proof
let F,G be PartFunc of REAL 3,REAL;
assume that
A5: dom F = D & for u be Element of REAL 3 st u in D holds
F.u = hpartdiff13(f,u) and
A6: dom G = D & for u be Element of REAL 3 st u in D holds
G.u = hpartdiff13(f,u);
now
let u be Element of REAL 3;
assume
A7: u in dom F;
then F.u = hpartdiff13(f,u) by A5;
hence F.u = G.u by A5,A6,A7;
end;
hence thesis by A5,A6,PARTFUN1:34;
end;
end;
definition
let f be PartFunc of REAL 3,REAL;
let D be set;
assume A1: f is_hpartial_differentiable`21_on D;
func f`hpartial21|D -> PartFunc of REAL 3,REAL means
dom it = D & for u be Element of REAL 3 st u in D holds
it.u = hpartdiff21(f,u);
existence
proof
defpred P[Element of REAL 3] means $1 in D;
deffunc F(Element of REAL 3) = hpartdiff21(f,$1);
consider F being PartFunc of REAL 3,REAL such that
A2: (for u be Element of REAL 3 holds u in dom F iff P[u]) &
for u be Element of REAL 3 st u in dom F holds F.u = F(u)
from SEQ_1:sch 3;
take F;
for y be set st y in dom F holds y in D by A2;then
A3: dom F c= D by TARSKI:def 3;
now
let y be set such that
A4: y in D;
D c= dom f by A1,Def22;
then D is Subset of REAL 3 by XBOOLE_1:1;
hence y in dom F by A2,A4;
end;
then D c= dom F by TARSKI:def 3;
hence dom F = D by A3,XBOOLE_0:def 10;
hereby
let u be Element of REAL 3;
assume u in D;then
u in dom F by A2;
hence F.u = hpartdiff21(f,u) by A2;
end;
end;
uniqueness
proof
let F,G be PartFunc of REAL 3,REAL;
assume that
A5: dom F = D & for u be Element of REAL 3 st u in D holds
F.u = hpartdiff21(f,u) and
A6: dom G = D & for u be Element of REAL 3 st u in D holds
G.u = hpartdiff21(f,u);
now
let u be Element of REAL 3;
assume
A7: u in dom F;
then F.u = hpartdiff21(f,u) by A5;
hence F.u = G.u by A5,A6,A7;
end;
hence thesis by A5,A6,PARTFUN1:34;
end;
end;
definition
let f be PartFunc of REAL 3,REAL;
let D be set;
assume A1: f is_hpartial_differentiable`22_on D;
func f`hpartial22|D -> PartFunc of REAL 3,REAL means
dom it = D & for u be Element of REAL 3 st u in D holds
it.u = hpartdiff22(f,u);
existence
proof
defpred P[Element of REAL 3] means $1 in D;
deffunc F(Element of REAL 3) = hpartdiff22(f,$1);
consider F being PartFunc of REAL 3,REAL such that
A2: (for u be Element of REAL 3 holds u in dom F iff P[u]) &
for u be Element of REAL 3 st u in dom F holds F.u = F(u)
from SEQ_1:sch 3;
take F;
for y be set st y in dom F holds y in D by A2;then
A3: dom F c= D by TARSKI:def 3;
now
let y be set such that
A4: y in D;
D c= dom f by A1,Def23;
then D is Subset of REAL 3 by XBOOLE_1:1;
hence y in dom F by A2,A4;
end;
then D c= dom F by TARSKI:def 3;
hence dom F = D by A3,XBOOLE_0:def 10;
hereby
let u be Element of REAL 3;
assume u in D;then
u in dom F by A2;
hence F.u = hpartdiff22(f,u) by A2;
end;
end;
uniqueness
proof
let F,G be PartFunc of REAL 3,REAL;
assume that
A5: dom F = D & for u be Element of REAL 3 st u in D holds
F.u = hpartdiff22(f,u) and
A6: dom G = D & for u be Element of REAL 3 st u in D holds
G.u = hpartdiff22(f,u);
now
let u be Element of REAL 3;
assume
A7: u in dom F;
then F.u = hpartdiff22(f,u) by A5;
hence F.u = G.u by A5,A6,A7;
end;
hence thesis by A5,A6,PARTFUN1:34;
end;
end;
definition
let f be PartFunc of REAL 3,REAL;
let D be set;
assume A1: f is_hpartial_differentiable`23_on D;
func f`hpartial23|D -> PartFunc of REAL 3,REAL means
dom it = D & for u be Element of REAL 3 st u in D holds
it.u = hpartdiff23(f,u);
existence
proof
defpred P[Element of REAL 3] means $1 in D;
deffunc F(Element of REAL 3) = hpartdiff23(f,$1);
consider F being PartFunc of REAL 3,REAL such that
A2: (for u be Element of REAL 3 holds u in dom F iff P[u]) &
for u be Element of REAL 3 st u in dom F holds F.u = F(u)
from SEQ_1:sch 3;
take F;
for y be set st y in dom F holds y in D by A2;then
A3: dom F c= D by TARSKI:def 3;
now
let y be set such that
A4: y in D;
D c= dom f by A1,Def24;
then D is Subset of REAL 3 by XBOOLE_1:1;
hence y in dom F by A2,A4;
end;
then D c= dom F by TARSKI:def 3;
hence dom F = D by A3,XBOOLE_0:def 10;
hereby
let u be Element of REAL 3;
assume u in D;then
u in dom F by A2;
hence F.u = hpartdiff23(f,u) by A2;
end;
end;
uniqueness
proof
let F,G be PartFunc of REAL 3,REAL;
assume that
A5: dom F = D & for u be Element of REAL 3 st u in D holds
F.u = hpartdiff23(f,u) and
A6: dom G = D & for u be Element of REAL 3 st u in D holds
G.u = hpartdiff23(f,u);
now
let u be Element of REAL 3;
assume
A7: u in dom F;
then F.u = hpartdiff23(f,u) by A5;
hence F.u = G.u by A5,A6,A7;
end;
hence thesis by A5,A6,PARTFUN1:34;
end;
end;
definition
let f be PartFunc of REAL 3,REAL;
let D be set;
assume A1: f is_hpartial_differentiable`31_on D;
func f`hpartial31|D -> PartFunc of REAL 3,REAL means
dom it = D & for u be Element of REAL 3 st u in D holds
it.u = hpartdiff31(f,u);
existence
proof
defpred P[Element of REAL 3] means $1 in D;
deffunc F(Element of REAL 3) = hpartdiff31(f,$1);
consider F being PartFunc of REAL 3,REAL such that
A2: (for u be Element of REAL 3 holds u in dom F iff P[u]) &
for u be Element of REAL 3 st u in dom F holds F.u = F(u)
from SEQ_1:sch 3;
take F;
for y be set st y in dom F holds y in D by A2;then
A3: dom F c= D by TARSKI:def 3;
now
let y be set such that
A4: y in D;
D c= dom f by A1,Def25;
then D is Subset of REAL 3 by XBOOLE_1:1;
hence y in dom F by A2,A4;
end;
then D c= dom F by TARSKI:def 3;
hence dom F = D by A3,XBOOLE_0:def 10;
hereby
let u be Element of REAL 3;
assume u in D;then
u in dom F by A2;
hence F.u = hpartdiff31(f,u) by A2;
end;
end;
uniqueness
proof
let F,G be PartFunc of REAL 3,REAL;
assume that
A5: dom F = D & for u be Element of REAL 3 st u in D holds
F.u = hpartdiff31(f,u) and
A6: dom G = D & for u be Element of REAL 3 st u in D holds
G.u = hpartdiff31(f,u);
now
let u be Element of REAL 3;
assume
A7: u in dom F;
then F.u = hpartdiff31(f,u) by A5;
hence F.u = G.u by A5,A6,A7;
end;
hence thesis by A5,A6,PARTFUN1:34;
end;
end;
definition
let f be PartFunc of REAL 3,REAL;
let D be set;
assume A1: f is_hpartial_differentiable`32_on D;
func f`hpartial32|D -> PartFunc of REAL 3,REAL means
dom it = D & for u be Element of REAL 3 st u in D holds
it.u = hpartdiff32(f,u);
existence
proof
defpred P[Element of REAL 3] means $1 in D;
deffunc F(Element of REAL 3) = hpartdiff32(f,$1);
consider F being PartFunc of REAL 3,REAL such that
A2: (for u be Element of REAL 3 holds u in dom F iff P[u]) &
for u be Element of REAL 3 st u in dom F holds F.u = F(u)
from SEQ_1:sch 3;
take F;
for y be set st y in dom F holds y in D by A2;then
A3: dom F c= D by TARSKI:def 3;
now
let y be set such that
A4: y in D;
D c= dom f by A1,Def26;
then D is Subset of REAL 3 by XBOOLE_1:1;
hence y in dom F by A2,A4;
end;
then D c= dom F by TARSKI:def 3;
hence dom F = D by A3,XBOOLE_0:def 10;
hereby
let u be Element of REAL 3;
assume u in D;then
u in dom F by A2;
hence F.u = hpartdiff32(f,u) by A2;
end;
end;
uniqueness
proof
let F,G be PartFunc of REAL 3,REAL;
assume that
A5: dom F = D & for u be Element of REAL 3 st u in D holds
F.u = hpartdiff32(f,u) and
A6: dom G = D & for u be Element of REAL 3 st u in D holds
G.u = hpartdiff32(f,u);
now
let u be Element of REAL 3;
assume
A7: u in dom F;
then F.u = hpartdiff32(f,u) by A5;
hence F.u = G.u by A5,A6,A7;
end;
hence thesis by A5,A6,PARTFUN1:34;
end;
end;
definition
let f be PartFunc of REAL 3,REAL;
let D be set;
assume A1: f is_hpartial_differentiable`33_on D;
func f`hpartial33|D -> PartFunc of REAL 3,REAL means
dom it = D & for u be Element of REAL 3 st u in D holds
it.u = hpartdiff33(f,u);
existence
proof
defpred P[Element of REAL 3] means $1 in D;
deffunc F(Element of REAL 3) = hpartdiff33(f,$1);
consider F being PartFunc of REAL 3,REAL such that
A2: (for u be Element of REAL 3 holds u in dom F iff P[u]) &
for u be Element of REAL 3 st u in dom F holds F.u = F(u)
from SEQ_1:sch 3;
take F;
for y be set st y in dom F holds y in D by A2;then
A3: dom F c= D by TARSKI:def 3;
now
let y be set such that
A4: y in D;
D c= dom f by A1,Def27;
then D is Subset of REAL 3 by XBOOLE_1:1;
hence y in dom F by A2,A4;
end;
then D c= dom F by TARSKI:def 3;
hence dom F = D by A3,XBOOLE_0:def 10;
hereby
let u be Element of REAL 3;
assume u in D;then
u in dom F by A2;
hence F.u = hpartdiff33(f,u) by A2;
end;
end;
uniqueness
proof
let F,G be PartFunc of REAL 3,REAL;
assume that
A5: dom F = D & for u be Element of REAL 3 st u in D holds
F.u = hpartdiff33(f,u) and
A6: dom G = D & for u be Element of REAL 3 st u in D holds
G.u = hpartdiff33(f,u);
now
let u be Element of REAL 3;
assume
A7: u in dom F;
then F.u = hpartdiff33(f,u) by A5;
hence F.u = G.u by A5,A6,A7;
end;
hence thesis by A5,A6,PARTFUN1:34;
end;
end;
begin :: Main Properties of Second-order Partial Derivatives
theorem Th19:
f is_hpartial_differentiable`11_in u iff
pdiff1(f,1) is_partial_differentiable_in u,1
proof
thus f is_hpartial_differentiable`11_in u implies
pdiff1(f,1) is_partial_differentiable_in u,1
proof
assume f is_hpartial_differentiable`11_in u;
then consider x0,y0,z0 being Real such that
A1: u = <*x0,y0,z0*> & ex N being Neighbourhood of x0
st N c= dom SVF1(1,pdiff1(f,1),u) & ex L,R st for x 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)
by Def1;
thus thesis by A1,PDIFF_4:13;
end;
assume pdiff1(f,1) is_partial_differentiable_in u,1;
then consider x0,y0,z0 being Real such that
A2: u = <*x0,y0,z0*> & ex N being Neighbourhood of x0
st N c= dom SVF1(1,pdiff1(f,1),u) & ex L,R st for x 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)
by PDIFF_4:13;
thus thesis by A2,Def1;
end;
theorem Th20:
f is_hpartial_differentiable`12_in u iff
pdiff1(f,1) is_partial_differentiable_in u,2
proof
thus f is_hpartial_differentiable`12_in u implies
pdiff1(f,1) is_partial_differentiable_in u,2
proof
assume f is_hpartial_differentiable`12_in u;
then consider x0,y0,z0 being Real such that
A1: u = <*x0,y0,z0*> & ex N being Neighbourhood of y0
st N c= dom SVF1(2,pdiff1(f,1),u) & ex L,R st for y 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)
by Def2;
thus thesis by A1,PDIFF_4:14;
end;
assume pdiff1(f,1) is_partial_differentiable_in u,2;
then consider x0,y0,z0 being Real such that
A2: u = <*x0,y0,z0*> & ex N being Neighbourhood of y0
st N c= dom SVF1(2,pdiff1(f,1),u) & ex L,R st for y 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)
by PDIFF_4:14;
thus thesis by A2,Def2;
end;
theorem Th21:
f is_hpartial_differentiable`13_in u iff
pdiff1(f,1) is_partial_differentiable_in u,3
proof
thus f is_hpartial_differentiable`13_in u implies
pdiff1(f,1) is_partial_differentiable_in u,3
proof
assume f is_hpartial_differentiable`13_in u;
then consider x0,y0,z0 being Real such that
A1: u = <*x0,y0,z0*> & ex N being Neighbourhood of z0
st N c= dom SVF1(3,pdiff1(f,1),u) & ex L,R st for z 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)
by Def3;
thus thesis by A1,PDIFF_4:15;
end;
assume pdiff1(f,1) is_partial_differentiable_in u,3;
then consider x0,y0,z0 being Real such that
A2: u = <*x0,y0,z0*> & ex N being Neighbourhood of z0
st N c= dom SVF1(3,pdiff1(f,1),u) & ex L,R st for z 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)
by PDIFF_4:15;
thus thesis by A2,Def3;
end;
theorem Th22:
f is_hpartial_differentiable`21_in u iff
pdiff1(f,2) is_partial_differentiable_in u,1
proof
thus f is_hpartial_differentiable`21_in u implies
pdiff1(f,2) is_partial_differentiable_in u,1
proof
assume f is_hpartial_differentiable`21_in u;
then consider x0,y0,z0 being Real such that
A1: u = <*x0,y0,z0*> & ex N being Neighbourhood of x0
st N c= dom SVF1(1,pdiff1(f,2),u) & ex L,R st for x 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)
by Def4;
thus thesis by A1,PDIFF_4:13;
end;
assume pdiff1(f,2) is_partial_differentiable_in u,1;
then consider x0,y0,z0 being Real such that
A2: u = <*x0,y0,z0*> & ex N being Neighbourhood of x0
st N c= dom SVF1(1,pdiff1(f,2),u) & ex L,R st for x 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)
by PDIFF_4:13;
thus thesis by A2,Def4;
end;
theorem Th23:
f is_hpartial_differentiable`22_in u iff
pdiff1(f,2) is_partial_differentiable_in u,2
proof
thus f is_hpartial_differentiable`22_in u implies
pdiff1(f,2) is_partial_differentiable_in u,2
proof
assume f is_hpartial_differentiable`22_in u;
then consider x0,y0,z0 being Real such that
A1: u = <*x0,y0,z0*> & ex N being Neighbourhood of y0
st N c= dom SVF1(2,pdiff1(f,2),u) & ex L,R st for y 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)
by Def5;
thus thesis by A1,PDIFF_4:14;
end;
assume pdiff1(f,2) is_partial_differentiable_in u,2;
then consider x0,y0,z0 being Real such that
A2: u = <*x0,y0,z0*> & ex N being Neighbourhood of y0
st N c= dom SVF1(2,pdiff1(f,2),u) & ex L,R st for y 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)
by PDIFF_4:14;
thus thesis by A2,Def5;
end;
theorem Th24:
f is_hpartial_differentiable`23_in u iff
pdiff1(f,2) is_partial_differentiable_in u,3
proof
thus f is_hpartial_differentiable`23_in u implies
pdiff1(f,2) is_partial_differentiable_in u,3
proof
assume f is_hpartial_differentiable`23_in u;
then consider x0,y0,z0 being Real such that
A1: u = <*x0,y0,z0*> & ex N being Neighbourhood of z0
st N c= dom SVF1(3,pdiff1(f,2),u) & ex L,R st for z 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)
by Def6;
thus thesis by A1,PDIFF_4:15;
end;
assume pdiff1(f,2) is_partial_differentiable_in u,3;
then consider x0,y0,z0 being Real such that
A2: u = <*x0,y0,z0*> & ex N being Neighbourhood of z0
st N c= dom SVF1(3,pdiff1(f,2),u) & ex L,R st for z 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)
by PDIFF_4:15;
thus thesis by A2,Def6;
end;
theorem Th25:
f is_hpartial_differentiable`31_in u iff
pdiff1(f,3) is_partial_differentiable_in u,1
proof
thus f is_hpartial_differentiable`31_in u implies
pdiff1(f,3) is_partial_differentiable_in u,1
proof
assume f is_hpartial_differentiable`31_in u;
then consider x0,y0,z0 being Real such that
A1: u = <*x0,y0,z0*> & ex N being Neighbourhood of x0
st N c= dom SVF1(1,pdiff1(f,3),u) & ex L,R st for x 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)
by Def7;
thus thesis by A1,PDIFF_4:13;
end;
assume pdiff1(f,3) is_partial_differentiable_in u,1;
then consider x0,y0,z0 being Real such that
A2: u = <*x0,y0,z0*> & ex N being Neighbourhood of x0
st N c= dom SVF1(1,pdiff1(f,3),u) & ex L,R st for x 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)
by PDIFF_4:13;
thus thesis by A2,Def7;
end;
theorem Th26:
f is_hpartial_differentiable`32_in u iff
pdiff1(f,3) is_partial_differentiable_in u,2
proof
thus f is_hpartial_differentiable`32_in u implies
pdiff1(f,3) is_partial_differentiable_in u,2
proof
assume f is_hpartial_differentiable`32_in u;
then consider x0,y0,z0 being Real such that
A1: u = <*x0,y0,z0*> & ex N being Neighbourhood of y0
st N c= dom SVF1(2,pdiff1(f,3),u) & ex L,R st for y 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)
by Def8;
thus thesis by A1,PDIFF_4:14;
end;
assume pdiff1(f,3) is_partial_differentiable_in u,2;
then consider x0,y0,z0 being Real such that
A2: u = <*x0,y0,z0*> & ex N being Neighbourhood of y0
st N c= dom SVF1(2,pdiff1(f,3),u) & ex L,R st for y 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)
by PDIFF_4:14;
thus thesis by A2,Def8;
end;
theorem Th27:
f is_hpartial_differentiable`33_in u iff
pdiff1(f,3) is_partial_differentiable_in u,3
proof
thus f is_hpartial_differentiable`33_in u implies
pdiff1(f,3) is_partial_differentiable_in u,3
proof
assume f is_hpartial_differentiable`33_in u;
then consider x0,y0,z0 being Real such that
A1: u = <*x0,y0,z0*> & ex N being Neighbourhood of z0
st N c= dom SVF1(3,pdiff1(f,3),u) & ex L,R st for z 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)
by Def9;
thus thesis by A1,PDIFF_4:15;
end;
assume pdiff1(f,3) is_partial_differentiable_in u,3;
then consider x0,y0,z0 being Real such that
A2: u = <*x0,y0,z0*> & ex N being Neighbourhood of z0
st N c= dom SVF1(3,pdiff1(f,3),u) & ex L,R st for z 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)
by PDIFF_4:15;
thus thesis by A2,Def9;
end;
theorem Th28:
f is_hpartial_differentiable`11_in u implies
hpartdiff11(f,u) = partdiff(pdiff1(f,1),u,1)
proof
assume
A1: f is_hpartial_differentiable`11_in u;
consider x0,y0,z0 being Real such that
A2: u = <*x0,y0,z0*> by FINSEQ_2:123;
hpartdiff11(f,u) = diff(SVF1(1,pdiff1(f,1),u),x0) by A1,A2,Th10
.= partdiff(pdiff1(f,1),u,1) by A2,PDIFF_4:19;
hence thesis;
end;
theorem Th29:
f is_hpartial_differentiable`12_in u implies
hpartdiff12(f,u) = partdiff(pdiff1(f,1),u,2)
proof
assume
A1: f is_hpartial_differentiable`12_in u;
consider x0,y0,z0 being Real such that
A2: u = <*x0,y0,z0*> by FINSEQ_2:123;
hpartdiff12(f,u) = diff(SVF1(2,pdiff1(f,1),u),y0) by A1,A2,Th11
.= partdiff(pdiff1(f,1),u,2) by A2,PDIFF_4:20;
hence thesis;
end;
theorem Th30:
f is_hpartial_differentiable`13_in u implies
hpartdiff13(f,u) = partdiff(pdiff1(f,1),u,3)
proof
assume
A1: f is_hpartial_differentiable`13_in u;
consider x0,y0,z0 being Real such that
A2: u = <*x0,y0,z0*> by FINSEQ_2:123;
hpartdiff13(f,u) = diff(SVF1(3,pdiff1(f,1),u),z0) by A1,A2,Th12
.= partdiff(pdiff1(f,1),u,3) by A2,PDIFF_4:21;
hence thesis;
end;
theorem Th31:
f is_hpartial_differentiable`21_in u implies
hpartdiff21(f,u) = partdiff(pdiff1(f,2),u,1)
proof
assume
A1: f is_hpartial_differentiable`21_in u;
consider x0,y0,z0 being Real such that
A2: u = <*x0,y0,z0*> by FINSEQ_2:123;
hpartdiff21(f,u) = diff(SVF1(1,pdiff1(f,2),u),x0) by A1,A2,Th13
.= partdiff(pdiff1(f,2),u,1) by A2,PDIFF_4:19;
hence thesis;
end;
theorem Th32:
f is_hpartial_differentiable`22_in u implies
hpartdiff22(f,u) = partdiff(pdiff1(f,2),u,2)
proof
assume
A1: f is_hpartial_differentiable`22_in u;
consider x0,y0,z0 being Real such that
A2: u = <*x0,y0,z0*> by FINSEQ_2:123;
hpartdiff22(f,u) = diff(SVF1(2,pdiff1(f,2),u),y0) by A1,A2,Th14
.= partdiff(pdiff1(f,2),u,2) by A2,PDIFF_4:20;
hence thesis;
end;
theorem Th33:
f is_hpartial_differentiable`23_in u implies
hpartdiff23(f,u) = partdiff(pdiff1(f,2),u,3)
proof
assume
A1: f is_hpartial_differentiable`23_in u;
consider x0,y0,z0 being Real such that
A2: u = <*x0,y0,z0*> by FINSEQ_2:123;
hpartdiff23(f,u) = diff(SVF1(3,pdiff1(f,2),u),z0) by A1,A2,Th15
.= partdiff(pdiff1(f,2),u,3) by A2,PDIFF_4:21;
hence thesis;
end;
theorem Th34:
f is_hpartial_differentiable`31_in u implies
hpartdiff31(f,u) = partdiff(pdiff1(f,3),u,1)
proof
assume
A1: f is_hpartial_differentiable`31_in u;
consider x0,y0,z0 being Real such that
A2: u = <*x0,y0,z0*> by FINSEQ_2:123;
hpartdiff31(f,u) = diff(SVF1(1,pdiff1(f,3),u),x0)
by A1,A2,Th16
.= partdiff(pdiff1(f,3),u,1) by A2,PDIFF_4:19;
hence thesis;
end;
theorem Th35:
f is_hpartial_differentiable`32_in u implies
hpartdiff32(f,u) = partdiff(pdiff1(f,3),u,2)
proof
assume
A1: f is_hpartial_differentiable`32_in u;
consider x0,y0,z0 being Real such that
A2: u = <*x0,y0,z0*> by FINSEQ_2:123;
hpartdiff32(f,u) = diff(SVF1(2,pdiff1(f,3),u),y0)
by A1,A2,Th17
.= partdiff(pdiff1(f,3),u,2) by A2,PDIFF_4:20;
hence thesis;
end;
theorem Th36:
f is_hpartial_differentiable`33_in u implies
hpartdiff33(f,u) = partdiff(pdiff1(f,3),u,3)
proof
assume
A1: f is_hpartial_differentiable`33_in u;
consider x0,y0,z0 being Real such that
A2: u = <*x0,y0,z0*> by FINSEQ_2:123;
hpartdiff33(f,u) = diff(SVF1(3,pdiff1(f,3),u),z0)
by A1,A2,Th18
.= partdiff(pdiff1(f,3),u,3) by A2,PDIFF_4:21;
hence thesis;
end;
theorem
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 be convergent_to_0 Real_Sequence, c be constant 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))
proof
let u0 be Element of REAL 3;
let N be Neighbourhood of proj(1,3).u0;
assume
A1: f is_hpartial_differentiable`11_in u0 & N c= dom SVF1(1,pdiff1(f,1),u0);
let h be convergent_to_0 Real_Sequence,
c be constant Real_Sequence such that
A2: rng c = {proj(1,3).u0} & rng (h+c) c= N;
A3: pdiff1(f,1) is_partial_differentiable_in u0,1 by A1,Th19;
consider x0,y0,z0 being Real such that
A4: u0 = <*x0,y0,z0*> by FINSEQ_2:123;
partdiff(pdiff1(f,1),u0,1)
= diff(SVF1(1,pdiff1(f,1),u0),x0) by A4,PDIFF_4:19
.= hpartdiff11(f,u0) by A1,A4,Th10;
hence thesis by A1,A2,A3,PDIFF_4:25;
end;
theorem
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 be convergent_to_0 Real_Sequence, c be constant 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))
proof
let u0 be Element of REAL 3;
let N be Neighbourhood of proj(2,3).u0;
assume
A1: f is_hpartial_differentiable`12_in u0 & N c= dom SVF1(2,pdiff1(f,1),u0);
let h be convergent_to_0 Real_Sequence,
c be constant Real_Sequence such that
A2: rng c = {proj(2,3).u0} & rng (h+c) c= N;
A3: pdiff1(f,1) is_partial_differentiable_in u0,2 by A1,Th20;
consider x0,y0,z0 being Real such that
A4: u0 = <*x0,y0,z0*> by FINSEQ_2:123;
partdiff(pdiff1(f,1),u0,2)
= diff(SVF1(2,pdiff1(f,1),u0),y0) by A4,PDIFF_4:20
.= hpartdiff12(f,u0) by A1,A4,Th11;
hence thesis by A1,A2,A3,PDIFF_4:26;
end;
theorem
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 be convergent_to_0 Real_Sequence, c be constant 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))
proof
let u0 be Element of REAL 3;
let N be Neighbourhood of proj(3,3).u0;
assume
A1: f is_hpartial_differentiable`13_in u0 & N c= dom SVF1(3,pdiff1(f,1),u0);
let h be convergent_to_0 Real_Sequence,
c be constant Real_Sequence such that
A2: rng c = {proj(3,3).u0} & rng (h+c) c= N;
A3: pdiff1(f,1) is_partial_differentiable_in u0,3 by A1,Th21;
consider x0,y0,z0 being Real such that
A4: u0 = <*x0,y0,z0*> by FINSEQ_2:123;
partdiff(pdiff1(f,1),u0,3)
= diff(SVF1(3,pdiff1(f,1),u0),z0) by A4,PDIFF_4:21
.= hpartdiff13(f,u0) by A1,A4,Th12;
hence thesis by A1,A2,A3,PDIFF_4:27;
end;
theorem
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 be convergent_to_0 Real_Sequence, c be constant 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))
proof
let u0 be Element of REAL 3;
let N be Neighbourhood of proj(1,3).u0;
assume
A1: f is_hpartial_differentiable`21_in u0 & N c= dom SVF1(1,pdiff1(f,2),u0);
let h be convergent_to_0 Real_Sequence,
c be constant Real_Sequence such that
A2: rng c = {proj(1,3).u0} & rng (h+c) c= N;
A3: pdiff1(f,2) is_partial_differentiable_in u0,1 by A1,Th22;
consider x0,y0,z0 being Real such that
A4: u0 = <*x0,y0,z0*> by FINSEQ_2:123;
partdiff(pdiff1(f,2),u0,1)
= diff(SVF1(1,pdiff1(f,2),u0),x0) by A4,PDIFF_4:19
.= hpartdiff21(f,u0) by A1,A4,Th13;
hence thesis by A1,A2,A3,PDIFF_4:25;
end;
theorem
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 be convergent_to_0 Real_Sequence, c be constant 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))
proof
let u0 be Element of REAL 3;
let N be Neighbourhood of proj(2,3).u0;
assume
A1: f is_hpartial_differentiable`22_in u0 & N c= dom SVF1(2,pdiff1(f,2),u0);
let h be convergent_to_0 Real_Sequence,
c be constant Real_Sequence such that
A2: rng c = {proj(2,3).u0} & rng (h+c) c= N;
A3: pdiff1(f,2) is_partial_differentiable_in u0,2 by A1,Th23;
consider x0,y0,z0 being Real such that
A4: u0 = <*x0,y0,z0*> by FINSEQ_2:123;
partdiff(pdiff1(f,2),u0,2)
= diff(SVF1(2,pdiff1(f,2),u0),y0) by A4,PDIFF_4:20
.= hpartdiff22(f,u0) by A1,A4,Th14;
hence thesis by A1,A2,A3,PDIFF_4:26;
end;
theorem
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 be convergent_to_0 Real_Sequence, c be constant 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))
proof
let u0 be Element of REAL 3;
let N be Neighbourhood of proj(3,3).u0;
assume
A1: f is_hpartial_differentiable`23_in u0 & N c= dom SVF1(3,pdiff1(f,2),u0);
let h be convergent_to_0 Real_Sequence,
c be constant Real_Sequence such that
A2: rng c = {proj(3,3).u0} & rng (h+c) c= N;
A3: pdiff1(f,2) is_partial_differentiable_in u0,3 by A1,Th24;
consider x0,y0,z0 being Real such that
A4: u0 = <*x0,y0,z0*> by FINSEQ_2:123;
partdiff(pdiff1(f,2),u0,3)
= diff(SVF1(3,pdiff1(f,2),u0),z0) by A4,PDIFF_4:21
.= hpartdiff23(f,u0) by A1,A4,Th15;
hence thesis by A1,A2,A3,PDIFF_4:27;
end;
theorem
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 be convergent_to_0 Real_Sequence, c be constant 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))
proof
let u0 be Element of REAL 3;
let N be Neighbourhood of proj(1,3).u0;
assume
A1: f is_hpartial_differentiable`31_in u0 & N c= dom SVF1(1,pdiff1(f,3),u0);
let h be convergent_to_0 Real_Sequence,
c be constant Real_Sequence such that
A2: rng c = {proj(1,3).u0} & rng (h+c) c= N;
A3: pdiff1(f,3) is_partial_differentiable_in u0,1 by A1,Th25;
consider x0,y0,z0 being Real such that
A4: u0 = <*x0,y0,z0*> by FINSEQ_2:123;
partdiff(pdiff1(f,3),u0,1)
= diff(SVF1(1,pdiff1(f,3),u0),x0) by A4,PDIFF_4:19
.= hpartdiff31(f,u0) by A1,A4,Th16;
hence thesis by A1,A2,A3,PDIFF_4:25;
end;
theorem
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 be convergent_to_0 Real_Sequence, c be constant 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))
proof
let u0 be Element of REAL 3;
let N be Neighbourhood of proj(2,3).u0;
assume
A1: f is_hpartial_differentiable`32_in u0 & N c= dom SVF1(2,pdiff1(f,3),u0);
let h be convergent_to_0 Real_Sequence,
c be constant Real_Sequence such that
A2: rng c = {proj(2,3).u0} & rng (h+c) c= N;
A3: pdiff1(f,3) is_partial_differentiable_in u0,2 by A1,Th26;
consider x0,y0,z0 being Real such that
A4: u0 = <*x0,y0,z0*> by FINSEQ_2:123;
partdiff(pdiff1(f,3),u0,2)
= diff(SVF1(2,pdiff1(f,3),u0),y0) by A4,PDIFF_4:20
.= hpartdiff32(f,u0) by A1,A4,Th17;
hence thesis by A1,A2,A3,PDIFF_4:26;
end;
theorem
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 be convergent_to_0 Real_Sequence, c be constant 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))
proof
let u0 be Element of REAL 3;
let N be Neighbourhood of proj(3,3).u0;
assume
A1: f is_hpartial_differentiable`33_in u0 & N c= dom SVF1(3,pdiff1(f,3),u0);
let h be convergent_to_0 Real_Sequence,
c be constant Real_Sequence such that
A2: rng c = {proj(3,3).u0} & rng (h+c) c= N;
A3: pdiff1(f,3) is_partial_differentiable_in u0,3 by A1,Th27;
consider x0,y0,z0 being Real such that
A4: u0 = <*x0,y0,z0*> by FINSEQ_2:123;
partdiff(pdiff1(f,3),u0,3)
= diff(SVF1(3,pdiff1(f,3),u0),z0) by A4,PDIFF_4:21
.= hpartdiff33(f,u0) by A1,A4,Th18;
hence thesis by A1,A2,A3,PDIFF_4:27;
end;
theorem
f1 is_hpartial_differentiable`11_in u0 &
f2 is_hpartial_differentiable`11_in u0 implies
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)
proof
assume that
A1: f1 is_hpartial_differentiable`11_in u0 and
A2: f2 is_hpartial_differentiable`11_in u0;
A3: pdiff1(f1,1) is_partial_differentiable_in u0,1 by A1,Th19;
A4: pdiff1(f2,1) is_partial_differentiable_in u0,1 by A2,Th19;then
pdiff1(f1,1)+pdiff1(f2,1) is_partial_differentiable_in u0,1 &
partdiff(pdiff1(f1,1)+pdiff1(f2,1),u0,1)
= partdiff(pdiff1(f1,1),u0,1) + partdiff(pdiff1(f2,1),u0,1)
by A3,PDIFF_1:29;
then partdiff(pdiff1(f1,1)+pdiff1(f2,1),u0,1)
= hpartdiff11(f1,u0) + partdiff(pdiff1(f2,1),u0,1) by A1,Th28
.= hpartdiff11(f1,u0) + hpartdiff11(f2,u0) by A2,Th28;
hence thesis by A3,A4,PDIFF_1:29;
end;
theorem
f1 is_hpartial_differentiable`12_in u0 &
f2 is_hpartial_differentiable`12_in u0 implies
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)
proof
assume that
A1: f1 is_hpartial_differentiable`12_in u0 and
A2: f2 is_hpartial_differentiable`12_in u0;
A3: pdiff1(f1,1) is_partial_differentiable_in u0,2 by A1,Th20;
A4: pdiff1(f2,1) is_partial_differentiable_in u0,2 by A2,Th20;then
pdiff1(f1,1)+pdiff1(f2,1) is_partial_differentiable_in u0,2 &
partdiff(pdiff1(f1,1)+pdiff1(f2,1),u0,2)
= partdiff(pdiff1(f1,1),u0,2) + partdiff(pdiff1(f2,1),u0,2)
by A3,PDIFF_1:29;
then partdiff(pdiff1(f1,1)+pdiff1(f2,1),u0,2)
= hpartdiff12(f1,u0) + partdiff(pdiff1(f2,1),u0,2) by A1,Th29
.= hpartdiff12(f1,u0) + hpartdiff12(f2,u0) by A2,Th29;
hence thesis by A3,A4,PDIFF_1:29;
end;
theorem
f1 is_hpartial_differentiable`13_in u0 &
f2 is_hpartial_differentiable`13_in u0 implies
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)
proof
assume that
A1: f1 is_hpartial_differentiable`13_in u0 and
A2: f2 is_hpartial_differentiable`13_in u0;
A3: pdiff1(f1,1) is_partial_differentiable_in u0,3 by A1,Th21;
A4: pdiff1(f2,1) is_partial_differentiable_in u0,3 by A2,Th21;then
pdiff1(f1,1)+pdiff1(f2,1) is_partial_differentiable_in u0,3 &
partdiff(pdiff1(f1,1)+pdiff1(f2,1),u0,3)
= partdiff(pdiff1(f1,1),u0,3) + partdiff(pdiff1(f2,1),u0,3)
by A3,PDIFF_1:29;
then partdiff(pdiff1(f1,1)+pdiff1(f2,1),u0,3)
= hpartdiff13(f1,u0) + partdiff(pdiff1(f2,1),u0,3) by A1,Th30
.= hpartdiff13(f1,u0) + hpartdiff13(f2,u0) by A2,Th30;
hence thesis by A3,A4,PDIFF_1:29;
end;
theorem
f1 is_hpartial_differentiable`21_in u0 &
f2 is_hpartial_differentiable`21_in u0 implies
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)
proof
assume that
A1: f1 is_hpartial_differentiable`21_in u0 and
A2: f2 is_hpartial_differentiable`21_in u0;
A3: pdiff1(f1,2) is_partial_differentiable_in u0,1 by A1,Th22;
A4: pdiff1(f2,2) is_partial_differentiable_in u0,1 by A2,Th22;then
pdiff1(f1,2)+pdiff1(f2,2) is_partial_differentiable_in u0,1 &
partdiff(pdiff1(f1,2)+pdiff1(f2,2),u0,1)
= partdiff(pdiff1(f1,2),u0,1) + partdiff(pdiff1(f2,2),u0,1)
by A3,PDIFF_1:29;
then partdiff(pdiff1(f1,2)+pdiff1(f2,2),u0,1)
= hpartdiff21(f1,u0) + partdiff(pdiff1(f2,2),u0,1) by A1,Th31
.= hpartdiff21(f1,u0) + hpartdiff21(f2,u0) by A2,Th31;
hence thesis by A3,A4,PDIFF_1:29;
end;
theorem
f1 is_hpartial_differentiable`22_in u0 &
f2 is_hpartial_differentiable`22_in u0 implies
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)
proof
assume that
A1: f1 is_hpartial_differentiable`22_in u0 and
A2: f2 is_hpartial_differentiable`22_in u0;
A3: pdiff1(f1,2) is_partial_differentiable_in u0,2 by A1,Th23;
A4: pdiff1(f2,2) is_partial_differentiable_in u0,2 by A2,Th23;then
pdiff1(f1,2)+pdiff1(f2,2) is_partial_differentiable_in u0,2 &
partdiff(pdiff1(f1,2)+pdiff1(f2,2),u0,2)
= partdiff(pdiff1(f1,2),u0,2) + partdiff(pdiff1(f2,2),u0,2)
by A3,PDIFF_1:29;
then partdiff(pdiff1(f1,2)+pdiff1(f2,2),u0,2)
= hpartdiff22(f1,u0) + partdiff(pdiff1(f2,2),u0,2) by A1,Th32
.= hpartdiff22(f1,u0) + hpartdiff22(f2,u0) by A2,Th32;
hence thesis by A3,A4,PDIFF_1:29;
end;
theorem
f1 is_hpartial_differentiable`23_in u0 &
f2 is_hpartial_differentiable`23_in u0 implies
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)
proof
assume that
A1: f1 is_hpartial_differentiable`23_in u0 and
A2: f2 is_hpartial_differentiable`23_in u0;
A3: pdiff1(f1,2) is_partial_differentiable_in u0,3 by A1,Th24;
A4: pdiff1(f2,2) is_partial_differentiable_in u0,3 by A2,Th24;then
pdiff1(f1,2)+pdiff1(f2,2) is_partial_differentiable_in u0,3 &
partdiff(pdiff1(f1,2)+pdiff1(f2,2),u0,3)
= partdiff(pdiff1(f1,2),u0,3) + partdiff(pdiff1(f2,2),u0,3)
by A3,PDIFF_1:29;
then partdiff(pdiff1(f1,2)+pdiff1(f2,2),u0,3)
= hpartdiff23(f1,u0) + partdiff(pdiff1(f2,2),u0,3) by A1,Th33
.= hpartdiff23(f1,u0) + hpartdiff23(f2,u0) by A2,Th33;
hence thesis by A3,A4,PDIFF_1:29;
end;
theorem
f1 is_hpartial_differentiable`11_in u0 &
f2 is_hpartial_differentiable`11_in u0 implies
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)
proof
assume that
A1: f1 is_hpartial_differentiable`11_in u0 and
A2: f2 is_hpartial_differentiable`11_in u0;
A3: pdiff1(f1,1) is_partial_differentiable_in u0,1 by A1,Th19;
A4: pdiff1(f2,1) is_partial_differentiable_in u0,1 by A2,Th19;then
pdiff1(f1,1)-pdiff1(f2,1) is_partial_differentiable_in u0,1 &
partdiff(pdiff1(f1,1)-pdiff1(f2,1),u0,1)
= partdiff(pdiff1(f1,1),u0,1) - partdiff(pdiff1(f2,1),u0,1)
by A3,PDIFF_1:31;
then partdiff(pdiff1(f1,1)-pdiff1(f2,1),u0,1)
= hpartdiff11(f1,u0) - partdiff(pdiff1(f2,1),u0,1) by A1,Th28
.= hpartdiff11(f1,u0) - hpartdiff11(f2,u0) by A2,Th28;
hence thesis by A3,A4,PDIFF_1:31;
end;
theorem
f1 is_hpartial_differentiable`12_in u0 &
f2 is_hpartial_differentiable`12_in u0 implies
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)
proof
assume that
A1: f1 is_hpartial_differentiable`12_in u0 and
A2: f2 is_hpartial_differentiable`12_in u0;
A3: pdiff1(f1,1) is_partial_differentiable_in u0,2 by A1,Th20;
A4: pdiff1(f2,1) is_partial_differentiable_in u0,2 by A2,Th20;then
pdiff1(f1,1)-pdiff1(f2,1) is_partial_differentiable_in u0,2 &
partdiff(pdiff1(f1,1)-pdiff1(f2,1),u0,2)
= partdiff(pdiff1(f1,1),u0,2) - partdiff(pdiff1(f2,1),u0,2)
by A3,PDIFF_1:31;
then partdiff(pdiff1(f1,1)-pdiff1(f2,1),u0,2)
= hpartdiff12(f1,u0) - partdiff(pdiff1(f2,1),u0,2) by A1,Th29
.= hpartdiff12(f1,u0) - hpartdiff12(f2,u0) by A2,Th29;
hence thesis by A3,A4,PDIFF_1:31;
end;
theorem
f1 is_hpartial_differentiable`13_in u0 &
f2 is_hpartial_differentiable`13_in u0 implies
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)
proof
assume that
A1: f1 is_hpartial_differentiable`13_in u0 and
A2: f2 is_hpartial_differentiable`13_in u0;
A3: pdiff1(f1,1) is_partial_differentiable_in u0,3 by A1,Th21;
A4: pdiff1(f2,1) is_partial_differentiable_in u0,3 by A2,Th21;then
pdiff1(f1,1)-pdiff1(f2,1) is_partial_differentiable_in u0,3 &
partdiff(pdiff1(f1,1)-pdiff1(f2,1),u0,3)
= partdiff(pdiff1(f1,1),u0,3) - partdiff(pdiff1(f2,1),u0,3)
by A3,PDIFF_1:31;
then partdiff(pdiff1(f1,1)-pdiff1(f2,1),u0,3)
= hpartdiff13(f1,u0) - partdiff(pdiff1(f2,1),u0,3) by A1,Th30
.= hpartdiff13(f1,u0) - hpartdiff13(f2,u0) by A2,Th30;
hence thesis by A3,A4,PDIFF_1:31;
end;
theorem
f1 is_hpartial_differentiable`21_in u0 &
f2 is_hpartial_differentiable`21_in u0 implies
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)
proof
assume that
A1: f1 is_hpartial_differentiable`21_in u0 and
A2: f2 is_hpartial_differentiable`21_in u0;
A3: pdiff1(f1,2) is_partial_differentiable_in u0,1 by A1,Th22;
A4: pdiff1(f2,2) is_partial_differentiable_in u0,1 by A2,Th22;then
pdiff1(f1,2)-pdiff1(f2,2) is_partial_differentiable_in u0,1 &
partdiff(pdiff1(f1,2)-pdiff1(f2,2),u0,1)
= partdiff(pdiff1(f1,2),u0,1) - partdiff(pdiff1(f2,2),u0,1)
by A3,PDIFF_1:31;
then partdiff(pdiff1(f1,2)-pdiff1(f2,2),u0,1)
= hpartdiff21(f1,u0) - partdiff(pdiff1(f2,2),u0,1) by A1,Th31
.= hpartdiff21(f1,u0) - hpartdiff21(f2,u0) by A2,Th31;
hence thesis by A3,A4,PDIFF_1:31;
end;
theorem
f1 is_hpartial_differentiable`22_in u0 &
f2 is_hpartial_differentiable`22_in u0 implies
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)
proof
assume that
A1: f1 is_hpartial_differentiable`22_in u0 and
A2: f2 is_hpartial_differentiable`22_in u0;
A3: pdiff1(f1,2) is_partial_differentiable_in u0,2 by A1,Th23;
A4: pdiff1(f2,2) is_partial_differentiable_in u0,2 by A2,Th23;then
pdiff1(f1,2)-pdiff1(f2,2) is_partial_differentiable_in u0,2 &
partdiff(pdiff1(f1,2)-pdiff1(f2,2),u0,2)
= partdiff(pdiff1(f1,2),u0,2) - partdiff(pdiff1(f2,2),u0,2)
by A3,PDIFF_1:31;
then partdiff(pdiff1(f1,2)-pdiff1(f2,2),u0,2)
= hpartdiff22(f1,u0) - partdiff(pdiff1(f2,2),u0,2) by A1,Th32
.= hpartdiff22(f1,u0) - hpartdiff22(f2,u0) by A2,Th32;
hence thesis by A3,A4,PDIFF_1:31;
end;
theorem
f1 is_hpartial_differentiable`23_in u0 &
f2 is_hpartial_differentiable`23_in u0 implies
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)
proof
assume that
A1: f1 is_hpartial_differentiable`23_in u0 and
A2: f2 is_hpartial_differentiable`23_in u0;
A3: pdiff1(f1,2) is_partial_differentiable_in u0,3 by A1,Th24;
A4: pdiff1(f2,2) is_partial_differentiable_in u0,3 by A2,Th24;then
pdiff1(f1,2)-pdiff1(f2,2) is_partial_differentiable_in u0,3 &
partdiff(pdiff1(f1,2)-pdiff1(f2,2),u0,3)
= partdiff(pdiff1(f1,2),u0,3) - partdiff(pdiff1(f2,2),u0,3)
by A3,PDIFF_1:31;
then partdiff(pdiff1(f1,2)-pdiff1(f2,2),u0,3)
= hpartdiff23(f1,u0) - partdiff(pdiff1(f2,2),u0,3) by A1,Th33
.= hpartdiff23(f1,u0) - hpartdiff23(f2,u0) by A2,Th33;
hence thesis by A3,A4,PDIFF_1:31;
end;
theorem
f is_hpartial_differentiable`11_in u0 implies
r(#)pdiff1(f,1) is_partial_differentiable_in u0,1 &
partdiff((r(#)pdiff1(f,1)),u0,1) = r*hpartdiff11(f,u0)
proof
assume
A1: f is_hpartial_differentiable`11_in u0;
then pdiff1(f,1) is_partial_differentiable_in u0,1 by Th19;then
r(#)pdiff1(f,1) is_partial_differentiable_in u0,1 &
partdiff((r(#)pdiff1(f,1)),u0,1) = r*partdiff(pdiff1(f,1),u0,1)
by PDIFF_1:33;
hence thesis by A1,Th28;
end;
theorem
f is_hpartial_differentiable`12_in u0 implies
r(#)pdiff1(f,1) is_partial_differentiable_in u0,2 &
partdiff((r(#)pdiff1(f,1)),u0,2) = r*hpartdiff12(f,u0)
proof
assume
A1: f is_hpartial_differentiable`12_in u0;
then pdiff1(f,1) is_partial_differentiable_in u0,2 by Th20;then
r(#)pdiff1(f,1) is_partial_differentiable_in u0,2 &
partdiff((r(#)pdiff1(f,1)),u0,2) = r*partdiff(pdiff1(f,1),u0,2)
by PDIFF_1:33;
hence thesis by A1,Th29;
end;
theorem
f is_hpartial_differentiable`13_in u0 implies
r(#)pdiff1(f,1) is_partial_differentiable_in u0,3 &
partdiff((r(#)pdiff1(f,1)),u0,3) = r*hpartdiff13(f,u0)
proof
assume
A1: f is_hpartial_differentiable`13_in u0;
then pdiff1(f,1) is_partial_differentiable_in u0,3 by Th21;then
r(#)pdiff1(f,1) is_partial_differentiable_in u0,3 &
partdiff((r(#)pdiff1(f,1)),u0,3) = r*partdiff(pdiff1(f,1),u0,3)
by PDIFF_1:33;
hence thesis by A1,Th30;
end;
theorem
f is_hpartial_differentiable`21_in u0 implies
r(#)pdiff1(f,2) is_partial_differentiable_in u0,1 &
partdiff((r(#)pdiff1(f,2)),u0,1) = r*hpartdiff21(f,u0)
proof
assume
A1: f is_hpartial_differentiable`21_in u0;
then pdiff1(f,2) is_partial_differentiable_in u0,1 by Th22;then
r(#)pdiff1(f,2) is_partial_differentiable_in u0,1 &
partdiff((r(#)pdiff1(f,2)),u0,1) = r*partdiff(pdiff1(f,2),u0,1)
by PDIFF_1:33;
hence thesis by A1,Th31;
end;
theorem
f is_hpartial_differentiable`22_in u0 implies
r(#)pdiff1(f,2) is_partial_differentiable_in u0,2 &
partdiff((r(#)pdiff1(f,2)),u0,2) = r*hpartdiff22(f,u0)
proof
assume
A1: f is_hpartial_differentiable`22_in u0;
then pdiff1(f,2) is_partial_differentiable_in u0,2 by Th23;then
r(#)pdiff1(f,2) is_partial_differentiable_in u0,2 &
partdiff((r(#)pdiff1(f,2)),u0,2) = r*partdiff(pdiff1(f,2),u0,2)
by PDIFF_1:33;
hence thesis by A1,Th32;
end;
theorem
f is_hpartial_differentiable`23_in u0 implies
r(#)pdiff1(f,2) is_partial_differentiable_in u0,3 &
partdiff((r(#)pdiff1(f,2)),u0,3) = r*hpartdiff23(f,u0)
proof
assume
A1: f is_hpartial_differentiable`23_in u0;
then pdiff1(f,2) is_partial_differentiable_in u0,3 by Th24;then
r(#)pdiff1(f,2) is_partial_differentiable_in u0,3 &
partdiff((r(#)pdiff1(f,2)),u0,3) = r*partdiff(pdiff1(f,2),u0,3)
by PDIFF_1:33;
hence thesis by A1,Th33;
end;
theorem
f is_hpartial_differentiable`31_in u0 implies
r(#)pdiff1(f,3) is_partial_differentiable_in u0,1 &
partdiff((r(#)pdiff1(f,3)),u0,1) = r*hpartdiff31(f,u0)
proof
assume
A1: f is_hpartial_differentiable`31_in u0;
then pdiff1(f,3) is_partial_differentiable_in u0,1
by Th25;then
r(#)pdiff1(f,3) is_partial_differentiable_in u0,1 &
partdiff((r(#)pdiff1(f,3)),u0,1) = r*partdiff(pdiff1(f,3),u0,1)
by PDIFF_1:33;
hence thesis by A1,Th34;
end;
theorem
f is_hpartial_differentiable`32_in u0 implies
r(#)pdiff1(f,3) is_partial_differentiable_in u0,2 &
partdiff((r(#)pdiff1(f,3)),u0,2) = r*hpartdiff32(f,u0)
proof
assume
A1: f is_hpartial_differentiable`32_in u0;
then pdiff1(f,3) is_partial_differentiable_in u0,2
by Th26;then
r(#)pdiff1(f,3) is_partial_differentiable_in u0,2 &
partdiff((r(#)pdiff1(f,3)),u0,2) = r*partdiff(pdiff1(f,3),u0,2)
by PDIFF_1:33;
hence thesis by A1,Th35;
end;
theorem
f is_hpartial_differentiable`33_in u0 implies
r(#)pdiff1(f,3) is_partial_differentiable_in u0,3 &
partdiff((r(#)pdiff1(f,3)),u0,3) = r*hpartdiff33(f,u0)
proof
assume
A1: f is_hpartial_differentiable`33_in u0;
then pdiff1(f,3) is_partial_differentiable_in u0,3
by Th27;then
r(#)pdiff1(f,3) is_partial_differentiable_in u0,3 &
partdiff((r(#)pdiff1(f,3)),u0,3) = r*partdiff(pdiff1(f,3),u0,3)
by PDIFF_1:33;
hence thesis by A1,Th36;
end;
theorem
f1 is_hpartial_differentiable`11_in u0 &
f2 is_hpartial_differentiable`11_in u0 implies
pdiff1(f1,1)(#)pdiff1(f2,1) is_partial_differentiable_in u0,1
proof
assume f1 is_hpartial_differentiable`11_in u0 &
f2 is_hpartial_differentiable`11_in u0;
then pdiff1(f1,1) is_partial_differentiable_in u0,1 &
pdiff1(f2,1) is_partial_differentiable_in u0,1 by Th19;
hence thesis by PDIFF_4:28;
end;
theorem
f1 is_hpartial_differentiable`12_in u0 &
f2 is_hpartial_differentiable`12_in u0 implies
pdiff1(f1,1)(#)pdiff1(f2,1) is_partial_differentiable_in u0,2
proof
assume f1 is_hpartial_differentiable`12_in u0 &
f2 is_hpartial_differentiable`12_in u0;
then pdiff1(f1,1) is_partial_differentiable_in u0,2 &
pdiff1(f2,1) is_partial_differentiable_in u0,2 by Th20;
hence thesis by PDIFF_4:29;
end;
theorem
f1 is_hpartial_differentiable`13_in u0 &
f2 is_hpartial_differentiable`13_in u0 implies
pdiff1(f1,1)(#)pdiff1(f2,1) is_partial_differentiable_in u0,3
proof
assume f1 is_hpartial_differentiable`13_in u0 &
f2 is_hpartial_differentiable`13_in u0;
then pdiff1(f1,1) is_partial_differentiable_in u0,3 &
pdiff1(f2,1) is_partial_differentiable_in u0,3 by Th21;
hence thesis by PDIFF_4:30;
end;
theorem
f1 is_hpartial_differentiable`21_in u0 &
f2 is_hpartial_differentiable`21_in u0 implies
pdiff1(f1,2)(#)pdiff1(f2,2) is_partial_differentiable_in u0,1
proof
assume f1 is_hpartial_differentiable`21_in u0 &
f2 is_hpartial_differentiable`21_in u0;
then pdiff1(f1,2) is_partial_differentiable_in u0,1 &
pdiff1(f2,2) is_partial_differentiable_in u0,1 by Th22;
hence thesis by PDIFF_4:28;
end;
theorem
f1 is_hpartial_differentiable`22_in u0 &
f2 is_hpartial_differentiable`22_in u0 implies
pdiff1(f1,2)(#)pdiff1(f2,2) is_partial_differentiable_in u0,2
proof
assume f1 is_hpartial_differentiable`22_in u0 &
f2 is_hpartial_differentiable`22_in u0;
then pdiff1(f1,2) is_partial_differentiable_in u0,2 &
pdiff1(f2,2) is_partial_differentiable_in u0,2 by Th23;
hence thesis by PDIFF_4:29;
end;
theorem
f1 is_hpartial_differentiable`23_in u0 &
f2 is_hpartial_differentiable`23_in u0 implies
pdiff1(f1,2)(#)pdiff1(f2,2) is_partial_differentiable_in u0,3
proof
assume f1 is_hpartial_differentiable`23_in u0 &
f2 is_hpartial_differentiable`23_in u0;
then pdiff1(f1,2) is_partial_differentiable_in u0,3 &
pdiff1(f2,2) is_partial_differentiable_in u0,3 by Th24;
hence thesis by PDIFF_4:30;
end;
theorem
f1 is_hpartial_differentiable`31_in u0 &
f2 is_hpartial_differentiable`31_in u0 implies
pdiff1(f1,3)(#)pdiff1(f2,3) is_partial_differentiable_in u0,1
proof
assume f1 is_hpartial_differentiable`31_in u0 &
f2 is_hpartial_differentiable`31_in u0;
then pdiff1(f1,3) is_partial_differentiable_in u0,1 &
pdiff1(f2,3) is_partial_differentiable_in u0,1
by Th25;
hence thesis by PDIFF_4:28;
end;
theorem
f1 is_hpartial_differentiable`32_in u0 &
f2 is_hpartial_differentiable`32_in u0 implies
pdiff1(f1,3)(#)pdiff1(f2,3) is_partial_differentiable_in u0,2
proof
assume f1 is_hpartial_differentiable`32_in u0 &
f2 is_hpartial_differentiable`32_in u0;
then pdiff1(f1,3) is_partial_differentiable_in u0,2 &
pdiff1(f2,3) is_partial_differentiable_in u0,2 by Th26;
hence thesis by PDIFF_4:29;
end;
theorem
f1 is_hpartial_differentiable`33_in u0 &
f2 is_hpartial_differentiable`33_in u0 implies
pdiff1(f1,3)(#)pdiff1(f2,3) is_partial_differentiable_in u0,3
proof
assume f1 is_hpartial_differentiable`33_in u0 &
f2 is_hpartial_differentiable`33_in u0;
then pdiff1(f1,3) is_partial_differentiable_in u0,3 &
pdiff1(f2,3) is_partial_differentiable_in u0,3
by Th27;
hence thesis by PDIFF_4:30;
end;
theorem
for u0 being Element of REAL 3 holds f is_hpartial_differentiable`11_in u0
implies SVF1(1,pdiff1(f,1),u0) is_continuous_in proj(1,3).u0
proof
let u0 be Element of REAL 3;
assume f is_hpartial_differentiable`11_in u0;
then pdiff1(f,1) is_partial_differentiable_in u0,1 by Th19;
hence thesis by PDIFF_4:31;
end;
theorem
for u0 being Element of REAL 3 holds f is_hpartial_differentiable`12_in u0
implies SVF1(2,pdiff1(f,1),u0) is_continuous_in proj(2,3).u0
proof
let u0 be Element of REAL 3;
assume f is_hpartial_differentiable`12_in u0;
then pdiff1(f,1) is_partial_differentiable_in u0,2 by Th20;
hence thesis by PDIFF_4:32;
end;
theorem
for u0 being Element of REAL 3 holds f is_hpartial_differentiable`13_in u0
implies SVF1(3,pdiff1(f,1),u0) is_continuous_in proj(3,3).u0
proof
let u0 be Element of REAL 3;
assume f is_hpartial_differentiable`13_in u0;
then pdiff1(f,1) is_partial_differentiable_in u0,3 by Th21;
hence thesis by PDIFF_4:33;
end;
theorem
for u0 being Element of REAL 3 holds f is_hpartial_differentiable`21_in u0
implies SVF1(1,pdiff1(f,2),u0) is_continuous_in proj(1,3).u0
proof
let u0 be Element of REAL 3;
assume f is_hpartial_differentiable`21_in u0;
then pdiff1(f,2) is_partial_differentiable_in u0,1 by Th22;
hence thesis by PDIFF_4:31;
end;
theorem
for u0 being Element of REAL 3 holds f is_hpartial_differentiable`22_in u0
implies SVF1(2,pdiff1(f,2),u0) is_continuous_in proj(2,3).u0
proof
let u0 be Element of REAL 3;
assume f is_hpartial_differentiable`22_in u0;
then pdiff1(f,2) is_partial_differentiable_in u0,2 by Th23;
hence thesis by PDIFF_4:32;
end;
theorem
for u0 being Element of REAL 3 holds f is_hpartial_differentiable`23_in u0
implies SVF1(3,pdiff1(f,2),u0) is_continuous_in proj(3,3).u0
proof
let u0 be Element of REAL 3;
assume f is_hpartial_differentiable`23_in u0;
then pdiff1(f,2) is_partial_differentiable_in u0,3 by Th24;
hence thesis by PDIFF_4:33;
end;
theorem
for u0 being Element of REAL 3 holds f is_hpartial_differentiable`31_in u0
implies SVF1(1,pdiff1(f,3),u0) is_continuous_in proj(1,3).u0
proof
let u0 be Element of REAL 3;
assume f is_hpartial_differentiable`31_in u0;
then pdiff1(f,3) is_partial_differentiable_in u0,1 by Th25;
hence thesis by PDIFF_4:31;
end;
theorem
for u0 being Element of REAL 3 holds f is_hpartial_differentiable`32_in u0
implies SVF1(2,pdiff1(f,3),u0) is_continuous_in proj(2,3).u0
proof
let u0 be Element of REAL 3;
assume f is_hpartial_differentiable`32_in u0;
then pdiff1(f,3) is_partial_differentiable_in u0,2 by Th26;
hence thesis by PDIFF_4:32;
end;
theorem
for u0 being Element of REAL 3 holds f is_hpartial_differentiable`33_in u0
implies SVF1(3,pdiff1(f,3),u0) is_continuous_in proj(3,3).u0
proof
let u0 be Element of REAL 3;
assume f is_hpartial_differentiable`33_in u0;
then pdiff1(f,3) is_partial_differentiable_in u0,3 by Th27;
hence thesis by PDIFF_4:33;
end;