PDIFF_3: Second-order Partial Differentiation of Real Binary Functions

:: Second-order Partial Differentiation of Real Binary Functions
:: by Bing Xie , Xiquan Liang and Xiuzhuan Shen
::
:: Received December 16, 2008
:: Copyright (c) 2008 Association of Mizar Users

registration

cluster -> total Relation of REAL , REAL ;
coherence by FDIFF_1:def 3;

end;

definition

let f be PartFunc of REAL 2, REAL ;
let z be Element of REAL 2;
func pdiff1 f,z -> Function of REAL 2, REAL means :: PDIFF_3:def 1
for z being Element of REAL 2 st z in REAL 2 holds
it . z = partdiff1 f,z;
existence

proof end;

uniqueness

proof end;

func pdiff2 f,z -> Function of REAL 2, REAL means :: PDIFF_3:def 2
for z being Element of REAL 2 st z in REAL 2 holds
it . z = partdiff2 f,z;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines pdiff1 PDIFF_3:def 1 :

:: deftheorem defines pdiff2 PDIFF_3:def 2 :

definition

let f be PartFunc of REAL 2, REAL ;
let z be Element of REAL 2;
pred f is_hpartial_differentiable`11_in z means :Def3: :: PDIFF_3:def 3
ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (pdiff1 f,z),z) & ex L being LINEAR ex R being REST st
for x being Real st x in N holds
((SVF1 (pdiff1 f,z),z) . x) - ((SVF1 (pdiff1 f,z),z) . x0) = (L . (x - x0)) + (R . (x - x0)) ) );
pred f is_hpartial_differentiable`12_in z means :Def4: :: PDIFF_3:def 4
ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF2 (pdiff1 f,z),z) & ex L being LINEAR ex R being REST st
for y being Real st y in N holds
((SVF2 (pdiff1 f,z),z) . y) - ((SVF2 (pdiff1 f,z),z) . y0) = (L . (y - y0)) + (R . (y - y0)) ) );
pred f is_hpartial_differentiable`21_in z means :Def5: :: PDIFF_3:def 5
ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (pdiff2 f,z),z) & ex L being LINEAR ex R being REST st
for x being Real st x in N holds
((SVF1 (pdiff2 f,z),z) . x) - ((SVF1 (pdiff2 f,z),z) . x0) = (L . (x - x0)) + (R . (x - x0)) ) );
pred f is_hpartial_differentiable`22_in z means :Def6: :: PDIFF_3:def 6
ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF2 (pdiff2 f,z),z) & ex L being LINEAR ex R being REST st
for y being Real st y in N holds
((SVF2 (pdiff2 f,z),z) . y) - ((SVF2 (pdiff2 f,z),z) . y0) = (L . (y - y0)) + (R . (y - y0)) ) );

end;

:: deftheorem Def3 defines is_hpartial_differentiable`11_in PDIFF_3:def 3 :

:: deftheorem Def4 defines is_hpartial_differentiable`12_in PDIFF_3:def 4 :

:: deftheorem Def5 defines is_hpartial_differentiable`21_in PDIFF_3:def 5 :

:: deftheorem Def6 defines is_hpartial_differentiable`22_in PDIFF_3:def 6 :

definition

let f be PartFunc of REAL 2, REAL ;
let z be Element of REAL 2;
assume A1: f is_hpartial_differentiable`11_in z ;
func hpartdiff11 f,z -> Real means :Def7: :: PDIFF_3:def 7
ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (pdiff1 f,z),z) & ex L being LINEAR ex R being REST st
( it = L . 1 & ( for x being Real st x in N holds
((SVF1 (pdiff1 f,z),z) . x) - ((SVF1 (pdiff1 f,z),z) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines hpartdiff11 PDIFF_3:def 7 :

definition

let f be PartFunc of REAL 2, REAL ;
let z be Element of REAL 2;
assume A1: f is_hpartial_differentiable`12_in z ;
func hpartdiff12 f,z -> Real means :Def8: :: PDIFF_3:def 8
ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF2 (pdiff1 f,z),z) & ex L being LINEAR ex R being REST st
( it = L . 1 & ( for y being Real st y in N holds
((SVF2 (pdiff1 f,z),z) . y) - ((SVF2 (pdiff1 f,z),z) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines hpartdiff12 PDIFF_3:def 8 :

definition

let f be PartFunc of REAL 2, REAL ;
let z be Element of REAL 2;
assume A1: f is_hpartial_differentiable`21_in z ;
func hpartdiff21 f,z -> Real means :Def9: :: PDIFF_3:def 9
ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (pdiff2 f,z),z) & ex L being LINEAR ex R being REST st
( it = L . 1 & ( for x being Real st x in N holds
((SVF1 (pdiff2 f,z),z) . x) - ((SVF1 (pdiff2 f,z),z) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines hpartdiff21 PDIFF_3:def 9 :

definition

let f be PartFunc of REAL 2, REAL ;
let z be Element of REAL 2;
assume A1: f is_hpartial_differentiable`22_in z ;
func hpartdiff22 f,z -> Real means :Def10: :: PDIFF_3:def 10
ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF2 (pdiff2 f,z),z) & ex L being LINEAR ex R being REST st
( it = L . 1 & ( for y being Real st y in N holds
((SVF2 (pdiff2 f,z),z) . y) - ((SVF2 (pdiff2 f,z),z) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines hpartdiff22 PDIFF_3:def 10 :

theorem :: PDIFF_3:1

for x0, y0 being Real
for z being Element of REAL 2
for f being PartFunc of REAL 2, REAL st z = <*x0,y0*> & f is_hpartial_differentiable`11_in z holds
SVF1 (pdiff1 f,z),z is_differentiable_in x0

proof end;

theorem :: PDIFF_3:2

for x0, y0 being Real
for z being Element of REAL 2
for f being PartFunc of REAL 2, REAL st z = <*x0,y0*> & f is_hpartial_differentiable`12_in z holds
SVF2 (pdiff1 f,z),z is_differentiable_in y0

proof end;

theorem :: PDIFF_3:3

for x0, y0 being Real
for z being Element of REAL 2
for f being PartFunc of REAL 2, REAL st z = <*x0,y0*> & f is_hpartial_differentiable`21_in z holds
SVF1 (pdiff2 f,z),z is_differentiable_in x0

proof end;

theorem :: PDIFF_3:4

for x0, y0 being Real
for z being Element of REAL 2
for f being PartFunc of REAL 2, REAL st z = <*x0,y0*> & f is_hpartial_differentiable`22_in z holds
SVF2 (pdiff2 f,z),z is_differentiable_in y0

proof end;

theorem Th5: :: PDIFF_3:5

for x0, y0 being Real
for z being Element of REAL 2
for f being PartFunc of REAL 2, REAL st z = <*x0,y0*> & f is_hpartial_differentiable`11_in z holds
hpartdiff11 f,z = diff (SVF1 (pdiff1 f,z),z),x0

proof end;

theorem Th6: :: PDIFF_3:6

for x0, y0 being Real
for z being Element of REAL 2
for f being PartFunc of REAL 2, REAL st z = <*x0,y0*> & f is_hpartial_differentiable`12_in z holds
hpartdiff12 f,z = diff (SVF2 (pdiff1 f,z),z),y0

proof end;

theorem Th7: :: PDIFF_3:7

for x0, y0 being Real
for z being Element of REAL 2
for f being PartFunc of REAL 2, REAL st z = <*x0,y0*> & f is_hpartial_differentiable`21_in z holds
hpartdiff21 f,z = diff (SVF1 (pdiff2 f,z),z),x0

proof end;

theorem Th8: :: PDIFF_3:8

for x0, y0 being Real
for z being Element of REAL 2
for f being PartFunc of REAL 2, REAL st z = <*x0,y0*> & f is_hpartial_differentiable`22_in z holds
hpartdiff22 f,z = diff (SVF2 (pdiff2 f,z),z),y0

proof end;

definition

end;

:: deftheorem Def11 defines is_hpartial_differentiable`11_on PDIFF_3:def 11 :

:: deftheorem Def12 defines is_hpartial_differentiable`12_on PDIFF_3:def 12 :

:: deftheorem Def13 defines is_hpartial_differentiable`21_on PDIFF_3:def 13 :

:: deftheorem Def14 defines is_hpartial_differentiable`22_on PDIFF_3:def 14 :

definition

let f be PartFunc of REAL 2, REAL ;
let Z be set ;
assume A1: f is_hpartial_differentiable`11_on Z ;
func f `hpartial11| Z -> PartFunc of REAL 2, REAL means :: PDIFF_3:def 15
( dom it = Z & ( for z being Element of REAL 2 st z in Z holds
it . z = hpartdiff11 f,z ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines `hpartial11| PDIFF_3:def 15 :

definition

let f be PartFunc of REAL 2, REAL ;
let Z be set ;
assume A1: f is_hpartial_differentiable`12_on Z ;
func f `hpartial12| Z -> PartFunc of REAL 2, REAL means :: PDIFF_3:def 16
( dom it = Z & ( for z being Element of REAL 2 st z in Z holds
it . z = hpartdiff12 f,z ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines `hpartial12| PDIFF_3:def 16 :

definition

let f be PartFunc of REAL 2, REAL ;
let Z be set ;
assume A1: f is_hpartial_differentiable`21_on Z ;
func f `hpartial21| Z -> PartFunc of REAL 2, REAL means :: PDIFF_3:def 17
( dom it = Z & ( for z being Element of REAL 2 st z in Z holds
it . z = hpartdiff21 f,z ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines `hpartial21| PDIFF_3:def 17 :

definition

let f be PartFunc of REAL 2, REAL ;
let Z be set ;
assume A1: f is_hpartial_differentiable`22_on Z ;
func f `hpartial22| Z -> PartFunc of REAL 2, REAL means :: PDIFF_3:def 18
( dom it = Z & ( for z being Element of REAL 2 st z in Z holds
it . z = hpartdiff22 f,z ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines `hpartial22| PDIFF_3:def 18 :

theorem Th9: :: PDIFF_3:9

for z being Element of REAL 2
for f being PartFunc of REAL 2, REAL holds
( f is_hpartial_differentiable`11_in z iff pdiff1 f,z is_partial_differentiable`1_in z )

proof end;

theorem Th10: :: PDIFF_3:10

for z being Element of REAL 2
for f being PartFunc of REAL 2, REAL holds
( f is_hpartial_differentiable`12_in z iff pdiff1 f,z is_partial_differentiable`2_in z )

proof end;

theorem Th11: :: PDIFF_3:11

for z being Element of REAL 2
for f being PartFunc of REAL 2, REAL holds
( f is_hpartial_differentiable`21_in z iff pdiff2 f,z is_partial_differentiable`1_in z )

proof end;

theorem Th12: :: PDIFF_3:12

for z being Element of REAL 2
for f being PartFunc of REAL 2, REAL holds
( f is_hpartial_differentiable`22_in z iff pdiff2 f,z is_partial_differentiable`2_in z )

proof end;

theorem :: PDIFF_3:13

for z being Element of REAL 2
for f being PartFunc of REAL 2, REAL holds
( f is_hpartial_differentiable`11_in z iff pdiff1 f,z is_partial_differentiable_in z,1 )

proof end;

theorem :: PDIFF_3:14

for z being Element of REAL 2
for f being PartFunc of REAL 2, REAL holds
( f is_hpartial_differentiable`12_in z iff pdiff1 f,z is_partial_differentiable_in z,2 )

proof end;

theorem :: PDIFF_3:15

for z being Element of REAL 2
for f being PartFunc of REAL 2, REAL holds
( f is_hpartial_differentiable`21_in z iff pdiff2 f,z is_partial_differentiable_in z,1 )

proof end;

theorem :: PDIFF_3:16

for z being Element of REAL 2
for f being PartFunc of REAL 2, REAL holds
( f is_hpartial_differentiable`22_in z iff pdiff2 f,z is_partial_differentiable_in z,2 )

proof end;

theorem Th17: :: PDIFF_3:17

for z being Element of REAL 2
for f being PartFunc of REAL 2, REAL st f is_hpartial_differentiable`11_in z holds
hpartdiff11 f,z = partdiff1 (pdiff1 f,z),z

proof end;

theorem Th18: :: PDIFF_3:18

for z being Element of REAL 2
for f being PartFunc of REAL 2, REAL st f is_hpartial_differentiable`12_in z holds
hpartdiff12 f,z = partdiff2 (pdiff1 f,z),z

proof end;

theorem Th19: :: PDIFF_3:19

for z being Element of REAL 2
for f being PartFunc of REAL 2, REAL st f is_hpartial_differentiable`21_in z holds
hpartdiff21 f,z = partdiff1 (pdiff2 f,z),z

proof end;

theorem Th20: :: PDIFF_3:20

for z being Element of REAL 2
for f being PartFunc of REAL 2, REAL st f is_hpartial_differentiable`22_in z holds
hpartdiff22 f,z = partdiff2 (pdiff2 f,z),z

proof end;

theorem :: PDIFF_3:21

for f being PartFunc of REAL 2, REAL
for z0 being Element of REAL 2
for N being Neighbourhood of (proj 1,2) . z0 st f is_hpartial_differentiable`11_in z0 & N c= dom (SVF1 (pdiff1 f,z0),z0) holds
for h being convergent_to_0 Real_Sequence
for c being V6 Real_Sequence st rng c = {((proj 1,2) . z0)} & rng (h + c) c= N holds
( (h " ) (#) (((SVF1 (pdiff1 f,z0),z0) /* (h + c)) - ((SVF1 (pdiff1 f,z0),z0) /* c)) is convergent & hpartdiff11 f,z0 = lim ((h " ) (#) (((SVF1 (pdiff1 f,z0),z0) /* (h + c)) - ((SVF1 (pdiff1 f,z0),z0) /* c))) )

proof end;

theorem :: PDIFF_3:22

for f being PartFunc of REAL 2, REAL
for z0 being Element of REAL 2
for N being Neighbourhood of (proj 2,2) . z0 st f is_hpartial_differentiable`12_in z0 & N c= dom (SVF2 (pdiff1 f,z0),z0) holds
for h being convergent_to_0 Real_Sequence
for c being V6 Real_Sequence st rng c = {((proj 2,2) . z0)} & rng (h + c) c= N holds
( (h " ) (#) (((SVF2 (pdiff1 f,z0),z0) /* (h + c)) - ((SVF2 (pdiff1 f,z0),z0) /* c)) is convergent & hpartdiff12 f,z0 = lim ((h " ) (#) (((SVF2 (pdiff1 f,z0),z0) /* (h + c)) - ((SVF2 (pdiff1 f,z0),z0) /* c))) )

proof end;

theorem :: PDIFF_3:23

for f being PartFunc of REAL 2, REAL
for z0 being Element of REAL 2
for N being Neighbourhood of (proj 1,2) . z0 st f is_hpartial_differentiable`21_in z0 & N c= dom (SVF1 (pdiff2 f,z0),z0) holds
for h being convergent_to_0 Real_Sequence
for c being V6 Real_Sequence st rng c = {((proj 1,2) . z0)} & rng (h + c) c= N holds
( (h " ) (#) (((SVF1 (pdiff2 f,z0),z0) /* (h + c)) - ((SVF1 (pdiff2 f,z0),z0) /* c)) is convergent & hpartdiff21 f,z0 = lim ((h " ) (#) (((SVF1 (pdiff2 f,z0),z0) /* (h + c)) - ((SVF1 (pdiff2 f,z0),z0) /* c))) )

proof end;

theorem :: PDIFF_3:24

for f being PartFunc of REAL 2, REAL
for z0 being Element of REAL 2
for N being Neighbourhood of (proj 2,2) . z0 st f is_hpartial_differentiable`22_in z0 & N c= dom (SVF2 (pdiff2 f,z0),z0) holds
for h being convergent_to_0 Real_Sequence
for c being V6 Real_Sequence st rng c = {((proj 2,2) . z0)} & rng (h + c) c= N holds
( (h " ) (#) (((SVF2 (pdiff2 f,z0),z0) /* (h + c)) - ((SVF2 (pdiff2 f,z0),z0) /* c)) is convergent & hpartdiff22 f,z0 = lim ((h " ) (#) (((SVF2 (pdiff2 f,z0),z0) /* (h + c)) - ((SVF2 (pdiff2 f,z0),z0) /* c))) )

proof end;

theorem :: PDIFF_3:25

for z0 being Element of REAL 2
for f1, f2 being PartFunc of REAL 2, REAL st f1 is_hpartial_differentiable`11_in z0 & f2 is_hpartial_differentiable`11_in z0 holds
( (pdiff1 f1,z0) + (pdiff1 f2,z0) is_partial_differentiable`1_in z0 & partdiff1 ((pdiff1 f1,z0) + (pdiff1 f2,z0)),z0 = (hpartdiff11 f1,z0) + (hpartdiff11 f2,z0) )

proof end;

theorem :: PDIFF_3:26

for z0 being Element of REAL 2
for f1, f2 being PartFunc of REAL 2, REAL st f1 is_hpartial_differentiable`12_in z0 & f2 is_hpartial_differentiable`12_in z0 holds
( (pdiff1 f1,z0) + (pdiff1 f2,z0) is_partial_differentiable`2_in z0 & partdiff2 ((pdiff1 f1,z0) + (pdiff1 f2,z0)),z0 = (hpartdiff12 f1,z0) + (hpartdiff12 f2,z0) )

proof end;

theorem :: PDIFF_3:27

for z0 being Element of REAL 2
for f1, f2 being PartFunc of REAL 2, REAL st f1 is_hpartial_differentiable`21_in z0 & f2 is_hpartial_differentiable`21_in z0 holds
( (pdiff2 f1,z0) + (pdiff2 f2,z0) is_partial_differentiable`1_in z0 & partdiff1 ((pdiff2 f1,z0) + (pdiff2 f2,z0)),z0 = (hpartdiff21 f1,z0) + (hpartdiff21 f2,z0) )

proof end;

theorem :: PDIFF_3:28

for z0 being Element of REAL 2
for f1, f2 being PartFunc of REAL 2, REAL st f1 is_hpartial_differentiable`22_in z0 & f2 is_hpartial_differentiable`22_in z0 holds
( (pdiff2 f1,z0) + (pdiff2 f2,z0) is_partial_differentiable`2_in z0 & partdiff2 ((pdiff2 f1,z0) + (pdiff2 f2,z0)),z0 = (hpartdiff22 f1,z0) + (hpartdiff22 f2,z0) )

proof end;

theorem :: PDIFF_3:29

for z0 being Element of REAL 2
for f1, f2 being PartFunc of REAL 2, REAL st f1 is_hpartial_differentiable`11_in z0 & f2 is_hpartial_differentiable`11_in z0 holds
( (pdiff1 f1,z0) - (pdiff1 f2,z0) is_partial_differentiable`1_in z0 & partdiff1 ((pdiff1 f1,z0) - (pdiff1 f2,z0)),z0 = (hpartdiff11 f1,z0) - (hpartdiff11 f2,z0) )

proof end;

theorem :: PDIFF_3:30

for z0 being Element of REAL 2
for f1, f2 being PartFunc of REAL 2, REAL st f1 is_hpartial_differentiable`12_in z0 & f2 is_hpartial_differentiable`12_in z0 holds
( (pdiff1 f1,z0) - (pdiff1 f2,z0) is_partial_differentiable`2_in z0 & partdiff2 ((pdiff1 f1,z0) - (pdiff1 f2,z0)),z0 = (hpartdiff12 f1,z0) - (hpartdiff12 f2,z0) )

proof end;

theorem :: PDIFF_3:31

for z0 being Element of REAL 2
for f1, f2 being PartFunc of REAL 2, REAL st f1 is_hpartial_differentiable`21_in z0 & f2 is_hpartial_differentiable`21_in z0 holds
( (pdiff2 f1,z0) - (pdiff2 f2,z0) is_partial_differentiable`1_in z0 & partdiff1 ((pdiff2 f1,z0) - (pdiff2 f2,z0)),z0 = (hpartdiff21 f1,z0) - (hpartdiff21 f2,z0) )

proof end;

theorem :: PDIFF_3:32

for z0 being Element of REAL 2
for f1, f2 being PartFunc of REAL 2, REAL st f1 is_hpartial_differentiable`22_in z0 & f2 is_hpartial_differentiable`22_in z0 holds
( (pdiff2 f1,z0) - (pdiff2 f2,z0) is_partial_differentiable`2_in z0 & partdiff2 ((pdiff2 f1,z0) - (pdiff2 f2,z0)),z0 = (hpartdiff22 f1,z0) - (hpartdiff22 f2,z0) )

proof end;

theorem :: PDIFF_3:33

for r being Real
for z0 being Element of REAL 2
for f being PartFunc of REAL 2, REAL st f is_hpartial_differentiable`11_in z0 holds
( r (#) (pdiff1 f,z0) is_partial_differentiable`1_in z0 & partdiff1 (r (#) (pdiff1 f,z0)),z0 = r * (hpartdiff11 f,z0) )

proof end;

theorem :: PDIFF_3:34

for r being Real
for z0 being Element of REAL 2
for f being PartFunc of REAL 2, REAL st f is_hpartial_differentiable`12_in z0 holds
( r (#) (pdiff1 f,z0) is_partial_differentiable`2_in z0 & partdiff2 (r (#) (pdiff1 f,z0)),z0 = r * (hpartdiff12 f,z0) )

proof end;

theorem :: PDIFF_3:35

for r being Real
for z0 being Element of REAL 2
for f being PartFunc of REAL 2, REAL st f is_hpartial_differentiable`21_in z0 holds
( r (#) (pdiff2 f,z0) is_partial_differentiable`1_in z0 & partdiff1 (r (#) (pdiff2 f,z0)),z0 = r * (hpartdiff21 f,z0) )

proof end;

theorem :: PDIFF_3:36

for r being Real
for z0 being Element of REAL 2
for f being PartFunc of REAL 2, REAL st f is_hpartial_differentiable`22_in z0 holds
( r (#) (pdiff2 f,z0) is_partial_differentiable`2_in z0 & partdiff2 (r (#) (pdiff2 f,z0)),z0 = r * (hpartdiff22 f,z0) )

proof end;

theorem :: PDIFF_3:37

for z0 being Element of REAL 2
for f1, f2 being PartFunc of REAL 2, REAL st f1 is_hpartial_differentiable`11_in z0 & f2 is_hpartial_differentiable`11_in z0 holds
(pdiff1 f1,z0) (#) (pdiff1 f2,z0) is_partial_differentiable`1_in z0

proof end;

theorem :: PDIFF_3:38

for z0 being Element of REAL 2
for f1, f2 being PartFunc of REAL 2, REAL st f1 is_hpartial_differentiable`12_in z0 & f2 is_hpartial_differentiable`12_in z0 holds
(pdiff1 f1,z0) (#) (pdiff1 f2,z0) is_partial_differentiable`2_in z0

proof end;

theorem :: PDIFF_3:39

for z0 being Element of REAL 2
for f1, f2 being PartFunc of REAL 2, REAL st f1 is_hpartial_differentiable`21_in z0 & f2 is_hpartial_differentiable`21_in z0 holds
(pdiff2 f1,z0) (#) (pdiff2 f2,z0) is_partial_differentiable`1_in z0

proof end;

theorem :: PDIFF_3:40

for z0 being Element of REAL 2
for f1, f2 being PartFunc of REAL 2, REAL st f1 is_hpartial_differentiable`22_in z0 & f2 is_hpartial_differentiable`22_in z0 holds
(pdiff2 f1,z0) (#) (pdiff2 f2,z0) is_partial_differentiable`2_in z0

proof end;

theorem :: PDIFF_3:41

for f being PartFunc of REAL 2, REAL
for z0 being Element of REAL 2 st f is_hpartial_differentiable`11_in z0 holds
SVF1 (pdiff1 f,z0),z0 is_continuous_in (proj 1,2) . z0

proof end;

theorem :: PDIFF_3:42

for f being PartFunc of REAL 2, REAL
for z0 being Element of REAL 2 st f is_hpartial_differentiable`12_in z0 holds
SVF2 (pdiff1 f,z0),z0 is_continuous_in (proj 2,2) . z0

proof end;

theorem :: PDIFF_3:43

for f being PartFunc of REAL 2, REAL
for z0 being Element of REAL 2 st f is_hpartial_differentiable`21_in z0 holds
SVF1 (pdiff2 f,z0),z0 is_continuous_in (proj 1,2) . z0

proof end;

theorem :: PDIFF_3:44

for f being PartFunc of REAL 2, REAL
for z0 being Element of REAL 2 st f is_hpartial_differentiable`22_in z0 holds
SVF2 (pdiff2 f,z0),z0 is_continuous_in (proj 2,2) . z0

proof end;

theorem :: PDIFF_3:45

for z0 being Element of REAL 2
for f being PartFunc of REAL 2, REAL st f is_hpartial_differentiable`11_in z0 holds
ex R being REST st
( R . 0 = 0 & R is_continuous_in 0 )

proof end;

theorem :: PDIFF_3:46

for z0 being Element of REAL 2
for f being PartFunc of REAL 2, REAL st f is_hpartial_differentiable`12_in z0 holds
ex R being REST st
( R . 0 = 0 & R is_continuous_in 0 )

proof end;

theorem :: PDIFF_3:47

for z0 being Element of REAL 2
for f being PartFunc of REAL 2, REAL st f is_hpartial_differentiable`21_in z0 holds
ex R being REST st
( R . 0 = 0 & R is_continuous_in 0 )

proof end;

theorem :: PDIFF_3:48

for z0 being Element of REAL 2
for f being PartFunc of REAL 2, REAL st f is_hpartial_differentiable`22_in z0 holds
ex R being REST st
( R . 0 = 0 & R is_continuous_in 0 )

proof end;