:: Second-order Partial Differentiation of Real Ternary Functions
:: by Takao Inou\'e
::
:: Received January 26, 2010
:: Copyright (c) 2010-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
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, XXREAL_1, VALUED_0, NAT_1, FUNCT_7;
notations TARSKI, SUBSET_1, XXREAL_0, XCMPLX_0, XREAL_0, ORDINAL1, NUMBERS,
REAL_1, VALUED_0, FUNCT_1, 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, FCONT_1, PDIFF_1, PDIFF_2,
RELSET_1, PDIFF_3, RVSUM_1, BINOP_2, COMSEQ_2, COMPLEX1;
registrations RELSET_1, XREAL_0, MEMBERED, FDIFF_1, FUNCT_2, NAT_1, NUMBERS,
VALUED_0, VALUED_1, PDIFF_3, EUCLID, ORDINAL1;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities RCOMP_1, XBOOLE_0;
expansions XBOOLE_0;
theorems TARSKI, 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, XREAL_0;
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 RestFunc;
reserve L,L1 for LinearFunc;
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
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
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
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
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
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
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
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
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
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;
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 3;
take r;
L.1 = r*1 by A5
.= r;
hence thesis by A2,A3,A4;
end;
uniqueness
proof
let r,s be Real;
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 3;
consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 3;
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:78;
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:17;
consider g be Real such that
A22: 0 < g & N0 = ].x0-g,x0+g.[ by RCOMP_1:def 6;
deffunc F(Nat) = g/($1+2);
consider s1 such that
A23: for n being Nat holds s1.n = F(n) from SEQ_1:sch 1;
now let n be Nat;
g/(n+2) <> 0 by A22,XREAL_1:139;
hence s1.n <> 0 by A23;
end;
then
A24: s1 is non-zero by SEQ_1:5;
s1 is convergent & lim s1 = 0 by A23,SEQ_4:31;
then reconsider h = s1 as 0-convergent non-zero 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:139;
0+1 < n+1+1 by XREAL_1:6;
then g/(n+2) < g/1 by A22,XREAL_1:76;then
A27: x0+g/(n+2) < x0+g by XREAL_1:6;
x0+-g < x0+g/(n+2) by A22,A26,XREAL_1:6;
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: r - s in REAL by XREAL_0:def 1;
A30: for n being Nat holds r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n
proof let n be Nat;
A31: n in NAT by ORDINAL1:def 12; then
ex x st x in N & x in N1 & h.n = x-x0 by A25;then
A32: r*(h.n) + R.(h.n) = s*(h.n) + R1.(h.n) by A19;
A33: h.n <> 0 by SEQ_1:5;
A34: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (s*(h.n) + R1.(h.n))/(h.n)
by A32,XCMPLX_1:62;
A35: (r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:74
.= r*1 by A33,XCMPLX_1:60
.= r;
(s*(h.n))/(h.n) = s*((h.n)/(h.n)) by XCMPLX_1:74
.= s*1 by A33,XCMPLX_1:60
.= s;then
A36: r + (R.(h.n))/(h.n) = s + (R1.(h.n))/(h.n) by A34,A35,XCMPLX_1:62;
dom R = REAL by PARTFUN1:def 2;then
A37: rng h c= dom R;
dom R1 = REAL by PARTFUN1:def 2;then
A38: rng h c= dom R1;
A39: (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 A37,A31,FUNCT_2:108
.= ((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 A38,A31,FUNCT_2:108
.= ((h")(#)(R1/*h)).n by VALUED_1:5;
then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by A36,A39;
hence thesis by RFUNCT_2:1;
end; then
A40: ((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant by VALUED_0:def 18,A29;
(((h")(#)(R1/*h))-((h")(#)(R/*h))).1 = r-s by A30;then
A41: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-s by A40,SEQ_4:25;
A42: (h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0 by FDIFF_1:def 2;
(h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by FDIFF_1:def 2;
then r-s = 0-0 by A41,A42,SEQ_2:12;
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;
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 3;
take r;
L.1 = r*1 by A5 .= r;
hence thesis by A2,A3,A4;
end;
uniqueness
proof
let r,s be Real;
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 3;
consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 3;
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:78;
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:17;
consider g be Real such that
A22: 0 < g & N0 = ].y0-g,y0+g.[ by RCOMP_1:def 6;
deffunc F(Nat) = g/($1+2);
consider s1 such that
A23: for n being Nat holds s1.n = F(n) from SEQ_1:sch 1;
now let n be Nat;
g/(n+2) <> 0 by A22,XREAL_1:139;
hence s1.n <> 0 by A23;
end; then
A24: s1 is non-zero by SEQ_1:5;
s1 is convergent & lim s1 = 0 by A23,SEQ_4:31;
then reconsider h = s1 as 0-convergent non-zero 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:139;
0+1 < n+1+1 by XREAL_1:6;
then g/(n+2) < g/1 by A22,XREAL_1:76;then
A27: y0+g/(n+2) < y0+g by XREAL_1:6;
y0+-g < y0+g/(n+2) by A22,A26,XREAL_1:6;
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: r - s in REAL by XREAL_0:def 1;
A30: now let n be Nat;
A31: n in NAT by ORDINAL1:def 12; then
ex y st y in N & y in N1 & h.n = y-y0 by A25;then
A32: r*(h.n) + R.(h.n) = s*(h.n) + R1.(h.n) by A19;
A33: h.n <> 0 by SEQ_1:5;
A34: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (s*(h.n) + R1.(h.n))/(h.n)
by A32,XCMPLX_1:62;
A35: (r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:74
.= r*1 by A33,XCMPLX_1:60
.= r;
(s*(h.n))/(h.n) = s*((h.n)/(h.n)) by XCMPLX_1:74
.= s*1 by A33,XCMPLX_1:60
.= s;then
A36: r + (R.(h.n))/(h.n) = s + (R1.(h.n))/(h.n) by A34,A35,XCMPLX_1:62;
dom R = REAL by PARTFUN1:def 2;then
A37: rng h c= dom R;
dom R1 = REAL by PARTFUN1:def 2;then
A38: rng h c= dom R1;
A39: (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 A37,A31,FUNCT_2:108
.= ((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 A38,A31,FUNCT_2:108
.= ((h")(#)(R1/*h)).n by VALUED_1:5;
then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by A36,A39;
hence r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n by RFUNCT_2:1;
end; then
A40: ((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant by VALUED_0:def 18,A29;
(((h")(#)(R1/*h))-((h")(#)(R/*h))).1 = r-s by A30;then
A41: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-s by A40,SEQ_4:25;
A42: (h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0 by FDIFF_1:def 2;
(h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by FDIFF_1:def 2;
then r-s = 0-0 by A41,A42,SEQ_2:12;
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;
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 3;
take r;
L.1 = r*1 by A5 .= r;
hence thesis by A2,A3,A4;
end;
uniqueness
proof
let r,s be Real;
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 3;
consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 3;
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:78;
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:17;
consider g be Real such that
A22: 0 < g & N0 = ].z0-g,z0+g.[ by RCOMP_1:def 6;
deffunc F(Nat) = g/($1+2);
consider s1 such that
A23: for n being Nat holds s1.n = F(n) from SEQ_1:sch 1;
now let n be Nat;
g/(n+2) <> 0 by A22,XREAL_1:139;
hence s1.n <> 0 by A23;
end; then
A24: s1 is non-zero by SEQ_1:5;
s1 is convergent & lim s1 = 0 by A23,SEQ_4:31;
then reconsider h = s1 as 0-convergent non-zero 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:139;
0+1 < n+1+1 by XREAL_1:6;
then g/(n+2) < g/1 by A22,XREAL_1:76;then
A27: z0+g/(n+2) < z0+g by XREAL_1:6;
z0+-g < z0+g/(n+2) by A22,A26,XREAL_1:6;
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: r - s in REAL by XREAL_0:def 1;
A30: now let n be Nat;
A31: n in NAT by ORDINAL1:def 12; then
ex z st z in N & z in N1 & h.n = z-z0 by A25;then
A32: r*(h.n) + R.(h.n) = s*(h.n) + R1.(h.n) by A19;
A33: h.n <> 0 by SEQ_1:5;
A34: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (s*(h.n) + R1.(h.n))/(h.n)
by A32,XCMPLX_1:62;
A35: (r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:74
.= r*1 by A33,XCMPLX_1:60
.= r;
(s*(h.n))/(h.n) = s*((h.n)/(h.n)) by XCMPLX_1:74
.= s*1 by A33,XCMPLX_1:60
.= s;then
A36: r + (R.(h.n))/(h.n) = s + (R1.(h.n))/(h.n) by A34,A35,XCMPLX_1:62;
dom R = REAL by PARTFUN1:def 2;then
A37: rng h c= dom R;
dom R1 = REAL by PARTFUN1:def 2;then
A38: rng h c= dom R1;
A39: (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 A37,A31,FUNCT_2:108
.= ((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 A38,A31,FUNCT_2:108
.= ((h")(#)(R1/*h)).n by VALUED_1:5;
then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by A36,A39;
hence r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n by RFUNCT_2:1;
end; then
A40: ((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant by VALUED_0:def 18,A29;
(((h")(#)(R1/*h))-((h")(#)(R/*h))).1 = r-s by A30;then
A41: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-s by A40,SEQ_4:25;
A42: (h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0 by FDIFF_1:def 2;
(h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by FDIFF_1:def 2;
then r-s = 0-0 by A41,A42,SEQ_2:12;
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;
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 3;
take r;
L.1 = r*1 by A5
.= r;
hence thesis by A2,A3,A4;
end;
uniqueness
proof
let r,s be Real;
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 3;
consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 3;
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:78;
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:17;
consider g be Real such that
A22: 0 < g & N0 = ].x0-g,x0+g.[ by RCOMP_1:def 6;
deffunc F(Nat) = g/($1+2);
consider s1 such that
A23: for n being Nat holds s1.n = F(n) from SEQ_1:sch 1;
now let n be Nat;
g/(n+2) <> 0 by A22,XREAL_1:139;
hence s1.n <> 0 by A23;
end; then
A24: s1 is non-zero by SEQ_1:5;
s1 is convergent & lim s1 = 0 by A23,SEQ_4:31;
then reconsider h = s1 as 0-convergent non-zero 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:139;
0+1 < n+1+1 by XREAL_1:6;
then g/(n+2) < g/1 by A22,XREAL_1:76;then
A27: x0+g/(n+2) < x0+g by XREAL_1:6;
x0+-g < x0+g/(n+2) by A22,A26,XREAL_1:6;
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: r - s in REAL by XREAL_0:def 1;
A30: now let n be Nat;
A31: n in NAT by ORDINAL1:def 12; then
ex x st x in N & x in N1 & h.n = x-x0 by A25;then
A32: r*(h.n) + R.(h.n) = s*(h.n) + R1.(h.n) by A19;
A33: h.n <> 0 by SEQ_1:5;
A34: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (s*(h.n) + R1.(h.n))/(h.n)
by A32,XCMPLX_1:62;
A35: (r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:74
.= r*1 by A33,XCMPLX_1:60
.= r;
(s*(h.n))/(h.n) = s*((h.n)/(h.n)) by XCMPLX_1:74
.= s*1 by A33,XCMPLX_1:60
.= s;then
A36: r + (R.(h.n))/(h.n) = s + (R1.(h.n))/(h.n) by A34,A35,XCMPLX_1:62;
dom R = REAL by PARTFUN1:def 2;then
A37: rng h c= dom R;
dom R1 = REAL by PARTFUN1:def 2;then
A38: rng h c= dom R1;
A39: (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 A37,A31,FUNCT_2:108
.= ((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 A38,A31,FUNCT_2:108
.= ((h")(#)(R1/*h)).n by VALUED_1:5;
then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by A36,A39;
hence r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n by A31,VALUED_1:15;
end; then
A40: ((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant by VALUED_0:def 18,A29;
(((h")(#)(R1/*h))-((h")(#)(R/*h))).1 = r-s by A30;then
A41: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-s by A40,SEQ_4:25;
A42: (h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0 by FDIFF_1:def 2;
(h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by FDIFF_1:def 2;
then r-s = 0-0 by A41,A42,SEQ_2:12;
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;
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 3;
take r;
L.1 = r*1 by A5 .= r;
hence thesis by A2,A3,A4;
end;
uniqueness
proof
let r,s be Real;
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 3;
consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 3;
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:78;
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:17;
consider g be Real such that
A22: 0 < g & N0 = ].y0-g,y0+g.[ by RCOMP_1:def 6;
deffunc F(Nat) = g/($1+2);
consider s1 such that
A23: for n being Nat holds s1.n = F(n) from SEQ_1:sch 1;
now let n be Nat;
g/(n+2) <> 0 by A22,XREAL_1:139;
hence s1.n <> 0 by A23;
end; then
A24: s1 is non-zero by SEQ_1:5;
s1 is convergent & lim s1 = 0 by A23,SEQ_4:31;
then reconsider h = s1 as 0-convergent non-zero 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:139;
0+1 < n+1+1 by XREAL_1:6;
then g/(n+2) < g/1 by A22,XREAL_1:76;then
A27: y0+g/(n+2) < y0+g by XREAL_1:6;
y0+-g < y0+g/(n+2) by A22,A26,XREAL_1:6;
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: r - s in REAL by XREAL_0:def 1;
A30: now let n be Nat;
A31: n in NAT by ORDINAL1:def 12; then
ex y st y in N & y in N1 & h.n = y-y0 by A25;then
A32: r*(h.n) + R.(h.n) = s*(h.n) + R1.(h.n) by A19;
A33: h.n <> 0 by SEQ_1:5;
A34: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (s*(h.n) + R1.(h.n))/(h.n)
by A32,XCMPLX_1:62;
A35: (r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:74
.= r*1 by A33,XCMPLX_1:60
.= r;
(s*(h.n))/(h.n) = s*((h.n)/(h.n)) by XCMPLX_1:74
.= s*1 by A33,XCMPLX_1:60
.= s;then
A36: r + (R.(h.n))/(h.n) = s + (R1.(h.n))/(h.n) by A34,A35,XCMPLX_1:62;
dom R = REAL by PARTFUN1:def 2;then
A37: rng h c= dom R;
dom R1 = REAL by PARTFUN1:def 2;then
A38: rng h c= dom R1;
A39: (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 A37,A31,FUNCT_2:108
.= ((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 A38,A31,FUNCT_2:108
.= ((h")(#)(R1/*h)).n by VALUED_1:5;
then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by A36,A39;
hence r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n by RFUNCT_2:1;
end; then
A40: ((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant by VALUED_0:def 18,A29;
(((h")(#)(R1/*h))-((h")(#)(R/*h))).1 = r-s by A30;then
A41: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-s by A40,SEQ_4:25;
A42: (h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0 by FDIFF_1:def 2;
(h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by FDIFF_1:def 2;
then r-s = 0-0 by A41,A42,SEQ_2:12;
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;
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 3;
take r;
L.1 = r*1 by A5 .= r;
hence thesis by A2,A3,A4;
end;
uniqueness
proof
let r,s be Real;
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 3;
consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 3;
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:78;
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:17;
consider g be Real such that
A22: 0 < g & N0 = ].z0-g,z0+g.[ by RCOMP_1:def 6;
deffunc F(Nat) = g/($1+2);
consider s1 such that
A23: for n being Nat holds s1.n = F(n) from SEQ_1:sch 1;
now let n be Nat ;
g/(n+2) <> 0 by A22,XREAL_1:139;
hence s1.n <> 0 by A23;
end; then
A24: s1 is non-zero by SEQ_1:5;
s1 is convergent & lim s1 = 0 by A23,SEQ_4:31;
then reconsider h = s1 as 0-convergent non-zero 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:139;
0+1 < n+1+1 by XREAL_1:6;
then g/(n+2) < g/1 by A22,XREAL_1:76;then
A27: z0+g/(n+2) < z0+g by XREAL_1:6;
z0+-g < z0+g/(n+2) by A22,A26,XREAL_1:6;
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: r - s in REAL by XREAL_0:def 1;
A30: now let n be Nat;
A31: n in NAT by ORDINAL1:def 12; then
ex z st z in N & z in N1 & h.n = z-z0 by A25;then
A32: r*(h.n) + R.(h.n) = s*(h.n) + R1.(h.n) by A19;
A33: h.n <> 0 by SEQ_1:5;
A34: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (s*(h.n) + R1.(h.n))/(h.n)
by A32,XCMPLX_1:62;
A35: (r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:74
.= r*1 by A33,XCMPLX_1:60
.= r;
(s*(h.n))/(h.n) = s*((h.n)/(h.n)) by XCMPLX_1:74
.= s*1 by A33,XCMPLX_1:60
.= s;then
A36: r + (R.(h.n))/(h.n) = s + (R1.(h.n))/(h.n) by A34,A35,XCMPLX_1:62;
dom R = REAL by PARTFUN1:def 2;then
A37: rng h c= dom R;
dom R1 = REAL by PARTFUN1:def 2;then
A38: rng h c= dom R1;
A39: (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 A37,A31,FUNCT_2:108
.= ((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 A38,A31,FUNCT_2:108
.= ((h")(#)(R1/*h)).n by VALUED_1:5;
then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by A36,A39;
hence r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n by RFUNCT_2:1;
end; then
A40: ((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant by VALUED_0:def 18,A29;
(((h")(#)(R1/*h))-((h")(#)(R/*h))).1 = r-s by A30;then
A41: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-s by A40,SEQ_4:25;
A42: (h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0 by FDIFF_1:def 2;
(h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by FDIFF_1:def 2;
then r-s = 0-0 by A41,A42,SEQ_2:12;
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;
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 3;
take r;
L.1 = r*1 by A5
.= r;
hence thesis by A2,A3,A4;
end;
uniqueness
proof
let r,s be Real;
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 3;
consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 3;
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:78;
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:17;
consider g be Real such that
A22: 0 < g & N0 = ].x0-g,x0+g.[ by RCOMP_1:def 6;
deffunc F(Nat) = g/($1+2);
consider s1 such that
A23: for n being Nat holds s1.n = F(n) from SEQ_1:sch 1;
now let n be Nat;
g/(n+2) <> 0 by A22,XREAL_1:139;
hence s1.n <> 0 by A23;
end; then
A24: s1 is non-zero by SEQ_1:5;
s1 is convergent & lim s1 = 0 by A23,SEQ_4:31;
then reconsider h = s1 as 0-convergent non-zero 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:139;
0+1 < n+1+1 by XREAL_1:6;
then g/(n+2) < g/1 by A22,XREAL_1:76;then
A27: x0+g/(n+2) < x0+g by XREAL_1:6;
x0+-g < x0+g/(n+2) by A22,A26,XREAL_1:6;
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: r - s in REAL by XREAL_0:def 1;
A30: now let n be Nat;
A31: n in NAT by ORDINAL1:def 12; then
ex x st x in N & x in N1 & h.n = x-x0 by A25;then
A32: r*(h.n) + R.(h.n) = s*(h.n) + R1.(h.n) by A19;
A33: h.n <> 0 by SEQ_1:5;
A34: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (s*(h.n) + R1.(h.n))/(h.n)
by A32,XCMPLX_1:62;
A35: (r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:74
.= r*1 by A33,XCMPLX_1:60
.= r;
(s*(h.n))/(h.n) = s*((h.n)/(h.n)) by XCMPLX_1:74
.= s*1 by A33,XCMPLX_1:60
.= s;then
A36: r + (R.(h.n))/(h.n) = s + (R1.(h.n))/(h.n) by A34,A35,XCMPLX_1:62;
dom R = REAL by PARTFUN1:def 2;then
A37: rng h c= dom R;
dom R1 = REAL by PARTFUN1:def 2;then
A38: rng h c= dom R1;
A39: (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 A37,A31,FUNCT_2:108
.= ((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 A38,A31,FUNCT_2:108
.= ((h")(#)(R1/*h)).n by VALUED_1:5;
then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by A36,A39;
hence r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n by A31,VALUED_1:15;
end; then
A40: ((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant by VALUED_0:def 18,A29;
(((h")(#)(R1/*h))-((h")(#)(R/*h))).1 = r-s by A30;then
A41: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-s by A40,SEQ_4:25;
A42: (h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0 by FDIFF_1:def 2;
(h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by FDIFF_1:def 2;
then r-s = 0-0 by A41,A42,SEQ_2:12;
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;
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 3;
take r;
L.1 = r*1 by A5 .= r;
hence thesis by A2,A3,A4;
end;
uniqueness
proof
let r,s be Real;
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 3;
consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 3;
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:78;
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:17;
consider g be Real such that
A22: 0 < g & N0 = ].y0-g,y0+g.[ by RCOMP_1:def 6;
deffunc F(Nat) = g/($1+2);
consider s1 such that
A23: for n being Nat holds s1.n = F(n) from SEQ_1:sch 1;
now let n be Nat;
g/(n+2) <> 0 by A22,XREAL_1:139;
hence s1.n <> 0 by A23;
end; then
A24: s1 is non-zero by SEQ_1:5;
s1 is convergent & lim s1 = 0 by A23,SEQ_4:31;
then reconsider h = s1 as 0-convergent non-zero 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:139;
0+1 < n+1+1 by XREAL_1:6;
then g/(n+2) < g/1 by A22,XREAL_1:76;then
A27: y0+g/(n+2) < y0+g by XREAL_1:6;
y0+-g < y0+g/(n+2) by A22,A26,XREAL_1:6;
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: r - s in REAL by XREAL_0:def 1;
A30: now let n be Nat;
A31: n in NAT by ORDINAL1:def 12; then
ex y st y in N & y in N1 & h.n = y-y0 by A25;then
A32: r*(h.n) + R.(h.n) = s*(h.n) + R1.(h.n) by A19;
A33: h.n <> 0 by SEQ_1:5;
A34: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (s*(h.n) + R1.(h.n))/(h.n)
by A32,XCMPLX_1:62;
A35: (r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:74
.= r*1 by A33,XCMPLX_1:60
.= r;
(s*(h.n))/(h.n) = s*((h.n)/(h.n)) by XCMPLX_1:74
.= s*1 by A33,XCMPLX_1:60
.= s;then
A36: r + (R.(h.n))/(h.n) = s + (R1.(h.n))/(h.n) by A34,A35,XCMPLX_1:62;
dom R = REAL by PARTFUN1:def 2;then
A37: rng h c= dom R;
dom R1 = REAL by PARTFUN1:def 2;then
A38: rng h c= dom R1;
A39: (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 A37,A31,FUNCT_2:108
.= ((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 A38,A31,FUNCT_2:108
.= ((h")(#)(R1/*h)).n by VALUED_1:5;
then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by A36,A39;
hence r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n by RFUNCT_2:1;
end; then
A40: ((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant by VALUED_0:def 18,A29;
(((h")(#)(R1/*h))-((h")(#)(R/*h))).1 = r-s by A30;then
A41: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-s by A40,SEQ_4:25;
A42: (h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0 by FDIFF_1:def 2;
(h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by FDIFF_1:def 2;
then r-s = 0-0 by A41,A42,SEQ_2:12;
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;
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 3;
take r;
L.1 = r*1 by A5 .= r;
hence thesis by A2,A3,A4;
end;
uniqueness
proof
let r,s be Real;
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 3;
consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 3;
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:78;
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:17;
consider g be Real such that
A22: 0 < g & N0 = ].z0-g,z0+g.[ by RCOMP_1:def 6;
deffunc F(Nat) = g/($1+2);
consider s1 such that
A23: for n being Nat holds s1.n = F(n) from SEQ_1:sch 1;
now let n be Nat;
g/(n+2) <> 0 by A22,XREAL_1:139;
hence s1.n <> 0 by A23;
end; then
A24: s1 is non-zero by SEQ_1:5;
s1 is convergent & lim s1 = 0 by A23,SEQ_4:31;
then reconsider h = s1 as 0-convergent non-zero 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:139;
0+1 < n+1+1 by XREAL_1:6;
then g/(n+2) < g/1 by A22,XREAL_1:76;then
A27: z0+g/(n+2) < z0+g by XREAL_1:6;
z0+-g < z0+g/(n+2) by A22,A26,XREAL_1:6;
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: r - s in REAL by XREAL_0:def 1;
A30: now let n be Nat;
A31: n in NAT by ORDINAL1:def 12; then
ex z st z in N & z in N1 & h.n = z-z0 by A25;then
A32: r*(h.n) + R.(h.n) = s*(h.n) + R1.(h.n) by A19;
A33: h.n <> 0 by SEQ_1:5;
A34: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (s*(h.n) + R1.(h.n))/(h.n)
by A32,XCMPLX_1:62;
A35: (r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:74
.= r*1 by A33,XCMPLX_1:60
.= r;
(s*(h.n))/(h.n) = s*((h.n)/(h.n)) by XCMPLX_1:74
.= s*1 by A33,XCMPLX_1:60
.= s;then
A36: r + (R.(h.n))/(h.n) = s + (R1.(h.n))/(h.n) by A34,A35,XCMPLX_1:62;
dom R = REAL by PARTFUN1:def 2;then
A37: rng h c= dom R;
dom R1 = REAL by PARTFUN1:def 2;then
A38: rng h c= dom R1;
A39: (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 A37,A31,FUNCT_2:108
.= ((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 A38,A31,FUNCT_2:108
.= ((h")(#)(R1/*h)).n by VALUED_1:5;
then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by A36,A39;
hence r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n by RFUNCT_2:1;
end; then
A40: ((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant by VALUED_0:def 18,A29;
(((h")(#)(R1/*h))-((h")(#)(R/*h))).1 = r-s by A30;then
A41: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-s by A40,SEQ_4:25;
A42: (h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0 by FDIFF_1:def 2;
(h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by FDIFF_1:def 2;
then r-s = 0-0 by A41,A42,SEQ_2:12;
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;
x0 = x1 by A1,A3,FINSEQ_1:78;
hence thesis by A3,FDIFF_1:def 4;
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;
y0 = y1 by A1,A3,FINSEQ_1:78;
hence thesis by A3,FDIFF_1:def 4;
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;
z0 = z1 by A1,A3,FINSEQ_1:78;
hence thesis by A3,FDIFF_1:def 4;
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;
x0 = x1 by A1,A3,FINSEQ_1:78;
hence thesis by A3,FDIFF_1:def 4;
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;
y0 = y1 by A1,A3,FINSEQ_1:78;
hence thesis by A3,FDIFF_1:def 4;
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;
z0 = z1 by A1,A3,FINSEQ_1:78;
hence thesis by A3,FDIFF_1:def 4;
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;
x0 = x1 by A1,A3,FINSEQ_1:78;
hence thesis by A3,FDIFF_1:def 4;
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;
y0 = y1 by A1,A3,FINSEQ_1:78;
hence thesis by A3,FDIFF_1:def 4;
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;
z0 = z1 by A1,A3,FINSEQ_1:78;
hence thesis by A3,FDIFF_1:def 4;
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;
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:78;
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 4;
hence thesis by A4,A5,A6,A7,FDIFF_1:def 5;
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;
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:78;
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 4;
hence thesis by A4,A5,A6,A7,FDIFF_1:def 5;
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;
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:78;
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 4;
hence thesis by A4,A5,A6,A7,FDIFF_1:def 5;
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;
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:78;
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 4;
hence thesis by A4,A5,A6,A7,FDIFF_1:def 5;
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;
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:78;
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 4;
hence thesis by A4,A5,A6,A7,FDIFF_1:def 5;
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;
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:78;
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 4;
hence thesis by A4,A5,A6,A7,FDIFF_1:def 5;
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;
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:78;
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 4;
hence thesis by A4,A5,A6,A7,FDIFF_1:def 5;
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;
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:78;
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 4;
hence thesis by A4,A5,A6,A7,FDIFF_1:def 5;
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;
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:78;
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 4;
hence thesis by A4,A5,A6,A7,FDIFF_1:def 5;
end;
definition
let f be PartFunc of REAL 3,REAL;
let D be set;
pred f is_hpartial_differentiable`11_on D means
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
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
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
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
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
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
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
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
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) = In(hpartdiff11(f,$1),REAL);
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 object 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 object such that
A4: y in D;
D c= dom f by A1;
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;
hereby
let u be Element of REAL 3;
assume u in D;then
u in dom F by A2;
hence F.u = F(u) by A2
.= hpartdiff11(f,u);
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:5;
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) = In(hpartdiff12(f,$1),REAL);
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 object 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 object such that
A4: y in D;
D c= dom f by A1;
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;
hereby
let u be Element of REAL 3;
assume u in D;then
u in dom F by A2;
hence F.u = F(u) by A2
.= hpartdiff12(f,u);
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:5;
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) = In(hpartdiff13(f,$1),REAL);
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 object 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 object such that
A4: y in D;
D c= dom f by A1;
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;
hereby
let u be Element of REAL 3;
assume u in D;then
u in dom F by A2;
hence F.u = F(u) by A2
.= hpartdiff13(f,u);
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:5;
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) = In(hpartdiff21(f,$1),REAL);
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 object 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 object such that
A4: y in D;
D c= dom f by A1;
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;
hereby
let u be Element of REAL 3;
assume u in D;then
u in dom F by A2;
hence F.u = F(u) by A2
.= hpartdiff21(f,u);
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:5;
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) = In(hpartdiff22(f,$1),REAL);
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 object 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 object such that
A4: y in D;
D c= dom f by A1;
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;
hereby
let u be Element of REAL 3;
assume u in D;then
u in dom F by A2;
hence F.u = F(u) by A2
.= hpartdiff22(f,u);
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:5;
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) = In(hpartdiff23(f,$1),REAL);
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 object 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 object such that
A4: y in D;
D c= dom f by A1;
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;
hereby
let u be Element of REAL 3;
assume u in D;then
u in dom F by A2;
hence F.u = F(u) by A2
.= hpartdiff23(f,u);
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:5;
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) = In(hpartdiff31(f,$1),REAL);
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 object 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 object such that
A4: y in D;
D c= dom f by A1;
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;
hereby
let u be Element of REAL 3;
assume u in D;then
u in dom F by A2;
hence F.u = F(u) by A2
.= hpartdiff31(f,u);
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:5;
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) = In(hpartdiff32(f,$1),REAL);
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 object 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 object such that
A4: y in D;
D c= dom f by A1;
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;
hereby
let u be Element of REAL 3;
assume u in D;then
u in dom F by A2;
hence F.u = F(u) by A2
.= hpartdiff32(f,u);
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:5;
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) = In(hpartdiff33(f,$1),REAL);
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 object 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 object such that
A4: y in D;
D c= dom f by A1;
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;
hereby
let u be Element of REAL 3;
assume u in D;then
u in dom F by A2;
hence F.u = F(u) by A2
.= hpartdiff33(f,u);
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:5;
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
by PDIFF_4:13;
theorem Th20:
f is_hpartial_differentiable`12_in u iff
pdiff1(f,1) is_partial_differentiable_in u,2
by PDIFF_4:14;
theorem Th21:
f is_hpartial_differentiable`13_in u iff
pdiff1(f,1) is_partial_differentiable_in u,3
by PDIFF_4:15;
theorem Th22:
f is_hpartial_differentiable`21_in u iff
pdiff1(f,2) is_partial_differentiable_in u,1
by PDIFF_4:13;
theorem Th23:
f is_hpartial_differentiable`22_in u iff
pdiff1(f,2) is_partial_differentiable_in u,2
by PDIFF_4:14;
theorem Th24:
f is_hpartial_differentiable`23_in u iff
pdiff1(f,2) is_partial_differentiable_in u,3
by PDIFF_4:15;
theorem Th25:
f is_hpartial_differentiable`31_in u iff
pdiff1(f,3) is_partial_differentiable_in u,1
by PDIFF_4:13;
theorem Th26:
f is_hpartial_differentiable`32_in u iff
pdiff1(f,3) is_partial_differentiable_in u,2
by PDIFF_4:14;
theorem Th27:
f is_hpartial_differentiable`33_in u iff
pdiff1(f,3) is_partial_differentiable_in u,3
by PDIFF_4:15;
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 Element of REAL such that
A2: u = <*x0,y0,z0*> by FINSEQ_2:103;
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 Element of REAL such that
A2: u = <*x0,y0,z0*> by FINSEQ_2:103;
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 Element of REAL such that
A2: u = <*x0,y0,z0*> by FINSEQ_2:103;
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 Element of REAL such that
A2: u = <*x0,y0,z0*> by FINSEQ_2:103;
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 Element of REAL such that
A2: u = <*x0,y0,z0*> by FINSEQ_2:103;
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 Element of REAL such that
A2: u = <*x0,y0,z0*> by FINSEQ_2:103;
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 Element of REAL such that
A2: u = <*x0,y0,z0*> by FINSEQ_2:103;
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 Element of REAL such that
A2: u = <*x0,y0,z0*> by FINSEQ_2:103;
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 Element of REAL such that
A2: u = <*x0,y0,z0*> by FINSEQ_2:103;
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 0-convergent non-zero 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 0-convergent non-zero 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 Element of REAL such that
A4: u0 = <*x0,y0,z0*> by FINSEQ_2:103;
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 0-convergent non-zero 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 0-convergent non-zero 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 Element of REAL such that
A4: u0 = <*x0,y0,z0*> by FINSEQ_2:103;
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 0-convergent non-zero 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 0-convergent non-zero 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 Element of REAL such that
A4: u0 = <*x0,y0,z0*> by FINSEQ_2:103;
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 0-convergent non-zero 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 0-convergent non-zero 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 Element of REAL such that
A4: u0 = <*x0,y0,z0*> by FINSEQ_2:103;
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 0-convergent non-zero 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 0-convergent non-zero 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 Element of REAL such that
A4: u0 = <*x0,y0,z0*> by FINSEQ_2:103;
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 0-convergent non-zero 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 0-convergent non-zero 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 Element of REAL such that
A4: u0 = <*x0,y0,z0*> by FINSEQ_2:103;
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 0-convergent non-zero 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 0-convergent non-zero 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 Element of REAL such that
A4: u0 = <*x0,y0,z0*> by FINSEQ_2:103;
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 0-convergent non-zero 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 0-convergent non-zero 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 Element of REAL such that
A4: u0 = <*x0,y0,z0*> by FINSEQ_2:103;
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 0-convergent non-zero 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 0-convergent non-zero 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 Element of REAL such that
A4: u0 = <*x0,y0,z0*> by FINSEQ_2:103;
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
by Th19,PDIFF_4:31;
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
by Th20,PDIFF_4:32;
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
by Th21,PDIFF_4:33;
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
by Th22,PDIFF_4:31;
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
by Th23,PDIFF_4:32;
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
by Th24,PDIFF_4:33;
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
by Th25,PDIFF_4:31;
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
by Th26,PDIFF_4:32;
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
by Th27,PDIFF_4:33;