:: Second-order Partial Differentiation of Real Ternary Functions :: by Takao Inou\'e :: :: Received January 26, 2010 :: Copyright (c) 2010-2021 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, NUMERALS, ARITHM; 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 :: PDIFF_5:def 1 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 :: PDIFF_5:def 2 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 :: PDIFF_5:def 3 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 :: PDIFF_5:def 4 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 :: PDIFF_5:def 5 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 :: PDIFF_5:def 6 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 :: PDIFF_5:def 7 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 :: PDIFF_5:def 8 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 :: PDIFF_5:def 9 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 f is_hpartial_differentiable`11_in u; func hpartdiff11(f,u) -> Real means :: PDIFF_5:def 10 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); end; definition let f be PartFunc of REAL 3,REAL; let u be Element of REAL 3; assume f is_hpartial_differentiable`12_in u; func hpartdiff12(f,u) -> Real means :: PDIFF_5:def 11 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); end; definition let f be PartFunc of REAL 3,REAL; let u be Element of REAL 3; assume f is_hpartial_differentiable`13_in u; func hpartdiff13(f,u) -> Real means :: PDIFF_5:def 12 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); end; definition let f be PartFunc of REAL 3,REAL; let u be Element of REAL 3; assume f is_hpartial_differentiable`21_in u; func hpartdiff21(f,u) -> Real means :: PDIFF_5:def 13 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); end; definition let f be PartFunc of REAL 3,REAL; let u be Element of REAL 3; assume f is_hpartial_differentiable`22_in u; func hpartdiff22(f,u) -> Real means :: PDIFF_5:def 14 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); end; definition let f be PartFunc of REAL 3,REAL; let u be Element of REAL 3; assume f is_hpartial_differentiable`23_in u; func hpartdiff23(f,u) -> Real means :: PDIFF_5:def 15 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); end; definition let f be PartFunc of REAL 3,REAL; let u be Element of REAL 3; assume f is_hpartial_differentiable`31_in u; func hpartdiff31(f,u) -> Real means :: PDIFF_5:def 16 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); end; definition let f be PartFunc of REAL 3,REAL; let u be Element of REAL 3; assume f is_hpartial_differentiable`32_in u; func hpartdiff32(f,u) -> Real means :: PDIFF_5:def 17 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); end; definition let f be PartFunc of REAL 3,REAL; let u be Element of REAL 3; assume f is_hpartial_differentiable`33_in u; func hpartdiff33(f,u) -> Real means :: PDIFF_5:def 18 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); end; theorem :: PDIFF_5:1 u = <*x0,y0,z0*> & f is_hpartial_differentiable`11_in u implies SVF1(1,pdiff1(f,1),u) is_differentiable_in x0; theorem :: PDIFF_5:2 u = <*x0,y0,z0*> & f is_hpartial_differentiable`12_in u implies SVF1(2,pdiff1(f,1),u) is_differentiable_in y0; theorem :: PDIFF_5:3 u = <*x0,y0,z0*> & f is_hpartial_differentiable`13_in u implies SVF1(3,pdiff1(f,1),u) is_differentiable_in z0; theorem :: PDIFF_5:4 u = <*x0,y0,z0*> & f is_hpartial_differentiable`21_in u implies SVF1(1,pdiff1(f,2),u) is_differentiable_in x0; theorem :: PDIFF_5:5 u = <*x0,y0,z0*> & f is_hpartial_differentiable`22_in u implies SVF1(2,pdiff1(f,2),u) is_differentiable_in y0; theorem :: PDIFF_5:6 u = <*x0,y0,z0*> & f is_hpartial_differentiable`23_in u implies SVF1(3,pdiff1(f,2),u) is_differentiable_in z0; theorem :: PDIFF_5:7 u = <*x0,y0,z0*> & f is_hpartial_differentiable`31_in u implies SVF1(1,pdiff1(f,3),u) is_differentiable_in x0; theorem :: PDIFF_5:8 u = <*x0,y0,z0*> & f is_hpartial_differentiable`32_in u implies SVF1(2,pdiff1(f,3),u) is_differentiable_in y0; theorem :: PDIFF_5:9 u = <*x0,y0,z0*> & f is_hpartial_differentiable`33_in u implies SVF1(3,pdiff1(f,3),u) is_differentiable_in z0; theorem :: PDIFF_5:10 u = <*x0,y0,z0*> & f is_hpartial_differentiable`11_in u implies hpartdiff11(f,u) = diff(SVF1(1,pdiff1(f,1),u),x0); theorem :: PDIFF_5:11 u = <*x0,y0,z0*> & f is_hpartial_differentiable`12_in u implies hpartdiff12(f,u) = diff(SVF1(2,pdiff1(f,1),u),y0); theorem :: PDIFF_5:12 u = <*x0,y0,z0*> & f is_hpartial_differentiable`13_in u implies hpartdiff13(f,u) = diff(SVF1(3,pdiff1(f,1),u),z0); theorem :: PDIFF_5:13 u = <*x0,y0,z0*> & f is_hpartial_differentiable`21_in u implies hpartdiff21(f,u) = diff(SVF1(1,pdiff1(f,2),u),x0); theorem :: PDIFF_5:14 u = <*x0,y0,z0*> & f is_hpartial_differentiable`22_in u implies hpartdiff22(f,u) = diff(SVF1(2,pdiff1(f,2),u),y0); theorem :: PDIFF_5:15 u = <*x0,y0,z0*> & f is_hpartial_differentiable`23_in u implies hpartdiff23(f,u) = diff(SVF1(3,pdiff1(f,2),u),z0); theorem :: PDIFF_5:16 u = <*x0,y0,z0*> & f is_hpartial_differentiable`31_in u implies hpartdiff31(f,u) = diff(SVF1(1,pdiff1(f,3),u),x0); theorem :: PDIFF_5:17 u = <*x0,y0,z0*> & f is_hpartial_differentiable`32_in u implies hpartdiff32(f,u) = diff(SVF1(2,pdiff1(f,3),u),y0); theorem :: PDIFF_5:18 u = <*x0,y0,z0*> & f is_hpartial_differentiable`33_in u implies hpartdiff33(f,u) = diff(SVF1(3,pdiff1(f,3),u),z0); definition let f be PartFunc of REAL 3,REAL; let D be set; pred f is_hpartial_differentiable`11_on D means :: PDIFF_5:def 19 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 :: PDIFF_5:def 20 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 :: PDIFF_5:def 21 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 :: PDIFF_5:def 22 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 :: PDIFF_5:def 23 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 :: PDIFF_5:def 24 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 :: PDIFF_5:def 25 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 :: PDIFF_5:def 26 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 :: PDIFF_5:def 27 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 f is_hpartial_differentiable`11_on D; func f`hpartial11|D -> PartFunc of REAL 3,REAL means :: PDIFF_5:def 28 dom it = D & for u be Element of REAL 3 st u in D holds it.u = hpartdiff11(f,u); end; definition let f be PartFunc of REAL 3,REAL; let D be set; assume f is_hpartial_differentiable`12_on D; func f`hpartial12|D -> PartFunc of REAL 3,REAL means :: PDIFF_5:def 29 dom it = D & for u be Element of REAL 3 st u in D holds it.u = hpartdiff12(f,u); end; definition let f be PartFunc of REAL 3,REAL; let D be set; assume f is_hpartial_differentiable`13_on D; func f`hpartial13|D -> PartFunc of REAL 3,REAL means :: PDIFF_5:def 30 dom it = D & for u be Element of REAL 3 st u in D holds it.u = hpartdiff13(f,u); end; definition let f be PartFunc of REAL 3,REAL; let D be set; assume f is_hpartial_differentiable`21_on D; func f`hpartial21|D -> PartFunc of REAL 3,REAL means :: PDIFF_5:def 31 dom it = D & for u be Element of REAL 3 st u in D holds it.u = hpartdiff21(f,u); end; definition let f be PartFunc of REAL 3,REAL; let D be set; assume f is_hpartial_differentiable`22_on D; func f`hpartial22|D -> PartFunc of REAL 3,REAL means :: PDIFF_5:def 32 dom it = D & for u be Element of REAL 3 st u in D holds it.u = hpartdiff22(f,u); end; definition let f be PartFunc of REAL 3,REAL; let D be set; assume f is_hpartial_differentiable`23_on D; func f`hpartial23|D -> PartFunc of REAL 3,REAL means :: PDIFF_5:def 33 dom it = D & for u be Element of REAL 3 st u in D holds it.u = hpartdiff23(f,u); end; definition let f be PartFunc of REAL 3,REAL; let D be set; assume f is_hpartial_differentiable`31_on D; func f`hpartial31|D -> PartFunc of REAL 3,REAL means :: PDIFF_5:def 34 dom it = D & for u be Element of REAL 3 st u in D holds it.u = hpartdiff31(f,u); end; definition let f be PartFunc of REAL 3,REAL; let D be set; assume f is_hpartial_differentiable`32_on D; func f`hpartial32|D -> PartFunc of REAL 3,REAL means :: PDIFF_5:def 35 dom it = D & for u be Element of REAL 3 st u in D holds it.u = hpartdiff32(f,u); end; definition let f be PartFunc of REAL 3,REAL; let D be set; assume f is_hpartial_differentiable`33_on D; func f`hpartial33|D -> PartFunc of REAL 3,REAL means :: PDIFF_5:def 36 dom it = D & for u be Element of REAL 3 st u in D holds it.u = hpartdiff33(f,u); end; begin :: Main Properties of Second-order Partial Derivatives theorem :: PDIFF_5:19 f is_hpartial_differentiable`11_in u iff pdiff1(f,1) is_partial_differentiable_in u,1; theorem :: PDIFF_5:20 f is_hpartial_differentiable`12_in u iff pdiff1(f,1) is_partial_differentiable_in u,2; theorem :: PDIFF_5:21 f is_hpartial_differentiable`13_in u iff pdiff1(f,1) is_partial_differentiable_in u,3; theorem :: PDIFF_5:22 f is_hpartial_differentiable`21_in u iff pdiff1(f,2) is_partial_differentiable_in u,1; theorem :: PDIFF_5:23 f is_hpartial_differentiable`22_in u iff pdiff1(f,2) is_partial_differentiable_in u,2; theorem :: PDIFF_5:24 f is_hpartial_differentiable`23_in u iff pdiff1(f,2) is_partial_differentiable_in u,3; theorem :: PDIFF_5:25 f is_hpartial_differentiable`31_in u iff pdiff1(f,3) is_partial_differentiable_in u,1; theorem :: PDIFF_5:26 f is_hpartial_differentiable`32_in u iff pdiff1(f,3) is_partial_differentiable_in u,2; theorem :: PDIFF_5:27 f is_hpartial_differentiable`33_in u iff pdiff1(f,3) is_partial_differentiable_in u,3; theorem :: PDIFF_5:28 f is_hpartial_differentiable`11_in u implies hpartdiff11(f,u) = partdiff(pdiff1(f,1),u,1); theorem :: PDIFF_5:29 f is_hpartial_differentiable`12_in u implies hpartdiff12(f,u) = partdiff(pdiff1(f,1),u,2); theorem :: PDIFF_5:30 f is_hpartial_differentiable`13_in u implies hpartdiff13(f,u) = partdiff(pdiff1(f,1),u,3); theorem :: PDIFF_5:31 f is_hpartial_differentiable`21_in u implies hpartdiff21(f,u) = partdiff(pdiff1(f,2),u,1); theorem :: PDIFF_5:32 f is_hpartial_differentiable`22_in u implies hpartdiff22(f,u) = partdiff(pdiff1(f,2),u,2); theorem :: PDIFF_5:33 f is_hpartial_differentiable`23_in u implies hpartdiff23(f,u) = partdiff(pdiff1(f,2),u,3); theorem :: PDIFF_5:34 f is_hpartial_differentiable`31_in u implies hpartdiff31(f,u) = partdiff(pdiff1(f,3),u,1); theorem :: PDIFF_5:35 f is_hpartial_differentiable`32_in u implies hpartdiff32(f,u) = partdiff(pdiff1(f,3),u,2); theorem :: PDIFF_5:36 f is_hpartial_differentiable`33_in u implies hpartdiff33(f,u) = partdiff(pdiff1(f,3),u,3); theorem :: PDIFF_5:37 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)); theorem :: PDIFF_5:38 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)); theorem :: PDIFF_5:39 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)); theorem :: PDIFF_5:40 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)); theorem :: PDIFF_5:41 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)); theorem :: PDIFF_5:42 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)); theorem :: PDIFF_5:43 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)); theorem :: PDIFF_5:44 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)); theorem :: PDIFF_5:45 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)); theorem :: PDIFF_5:46 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); theorem :: PDIFF_5:47 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); theorem :: PDIFF_5:48 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); theorem :: PDIFF_5:49 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); theorem :: PDIFF_5:50 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); theorem :: PDIFF_5:51 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); theorem :: PDIFF_5:52 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); theorem :: PDIFF_5:53 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); theorem :: PDIFF_5:54 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); theorem :: PDIFF_5:55 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); theorem :: PDIFF_5:56 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); theorem :: PDIFF_5:57 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); theorem :: PDIFF_5:58 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); theorem :: PDIFF_5:59 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); theorem :: PDIFF_5:60 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); theorem :: PDIFF_5:61 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); theorem :: PDIFF_5:62 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); theorem :: PDIFF_5:63 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); theorem :: PDIFF_5:64 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); theorem :: PDIFF_5:65 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); theorem :: PDIFF_5:66 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); theorem :: PDIFF_5:67 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; theorem :: PDIFF_5:68 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; theorem :: PDIFF_5:69 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; theorem :: PDIFF_5:70 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; theorem :: PDIFF_5:71 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; theorem :: PDIFF_5:72 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; theorem :: PDIFF_5:73 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; theorem :: PDIFF_5:74 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; theorem :: PDIFF_5:75 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; theorem :: PDIFF_5:76 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; theorem :: PDIFF_5:77 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; theorem :: PDIFF_5:78 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; theorem :: PDIFF_5:79 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; theorem :: PDIFF_5:80 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; theorem :: PDIFF_5:81 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; theorem :: PDIFF_5:82 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; theorem :: PDIFF_5:83 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; theorem :: PDIFF_5:84 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;