:: Partial Differentiation of Vector-Valued Functions on $n$-Dimensional RealNormed Linear Spaces
:: by Takao Inou\'e , Adam Naumowicz , Noboru Endou and Yasunari Shidama
::
:: Received April 22, 2010
:: Copyright (c) 2010 Association of Mizar Users

begin

Lm1: for S being RealNormSpace
for x being Point of S
for N1, N2 being Neighbourhood of x holds N1 /\ N2 is Neighbourhood of x

proof end;

Lm2: for i, j being Element of NAT st i <= j holds
i + (j -' i) = (i + j) -' i

proof end;

theorem Th1: :: PDIFF_7:1

for i, j being Element of NAT st i <= j holds
(0* j) | i = 0* i

proof end;

theorem Th2: :: PDIFF_7:2

for i, j being Element of NAT st i <= j holds
(0* j) | (i -' 1) = 0* (i -' 1)

proof end;

Lm3: for i, j being Element of NAT st i <= j holds
(0* j) /^ i = 0* (j -' i)

proof end;

Lm4: for i, j being Element of NAT st i > j holds
(0* j) /^ i = 0* (j -' i)

proof end;

theorem Th3: :: PDIFF_7:3

for j, i being Element of NAT holds (0* j) /^ i = 0* (j -' i)

proof end;

theorem :: PDIFF_7:4

for i, j being Element of NAT holds
( ( i <= j implies (0* j) | (i -' 1) = 0* (i -' 1) ) & (0* j) /^ i = 0* (j -' i) ) by Th2, Th3;

theorem Th5: :: PDIFF_7:5

for i, j being Element of NAT
for xi being Element of (REAL-NS 1) st 1 <= i & i <= j holds
||.((reproj i,(0. (REAL-NS j))) . xi).|| = ||.xi.||

proof end;

theorem Th6: :: PDIFF_7:6

for m, i being Element of NAT
for x being Element of REAL m
for r being Real holds
( ((reproj i,x) . r) - x = (reproj i,(0* m)) . (r - ((proj i,m) . x)) & x - ((reproj i,x) . r) = (reproj i,(0* m)) . (((proj i,m) . x) - r) )

proof end;

theorem Th7: :: PDIFF_7:7

for m, i being Element of NAT
for x being Point of (REAL-NS m)
for p being Point of (REAL-NS 1) holds
( ((reproj i,x) . p) - x = (reproj i,(0. (REAL-NS m))) . (p - ((Proj i,m) . x)) & x - ((reproj i,x) . p) = (reproj i,(0. (REAL-NS m))) . (((Proj i,m) . x) - p) )

proof end;

Lm5: for m being Element of NAT
for nx being Point of (REAL-NS m)
for Z being Subset of (REAL-NS m)
for i being Element of NAT st Z is open & nx in Z & 1 <= i & i <= m holds
ex N being Neighbourhood of (Proj i,m) . nx st
for z being Point of (REAL-NS 1) st z in N holds
(reproj i,nx) . z in Z

proof end;

theorem Th8: :: PDIFF_7:8

for m, n being non empty Element of NAT
for i being Element of NAT
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for Z being Subset of (REAL-NS m) st Z is open & 1 <= i & i <= m holds
( f is_partial_differentiable_on Z,i iff ( Z c= dom f & ( for x being Point of (REAL-NS m) st x in Z holds
f is_partial_differentiable_in x,i ) ) )

proof end;

Lm6: for m being non empty Element of NAT
for v being Element of REAL m
for x being Element of REAL
for i being Element of NAT holds len (Replace v,i,x) = m

proof end;

Lm7: for m being non empty Element of NAT
for x being Element of REAL
for i, j being Element of NAT st 1 <= j & j <= m holds
( ( i = j implies (Replace (0* m),i,x) . j = x ) & ( i <> j implies (Replace (0* m),i,x) . j = 0 ) )

proof end;

theorem Th9: :: PDIFF_7:9

for m being non empty Element of NAT
for x, y being Element of REAL
for i being Element of NAT st 1 <= i & i <= m holds
Replace (0* m),i,(x + y) = (Replace (0* m),i,x) + (Replace (0* m),i,y)

proof end;

theorem Th10: :: PDIFF_7:10

for m being non empty Element of NAT
for x, a being Element of REAL
for i being Element of NAT st 1 <= i & i <= m holds
Replace (0* m),i,(a * x) = a * (Replace (0* m),i,x)

proof end;

theorem Th11: :: PDIFF_7:11

for m being non empty Element of NAT
for x being Element of REAL
for i being Element of NAT st 1 <= i & i <= m & x <> 0 holds
Replace (0* m),i,x <> 0* m

proof end;

theorem Th12: :: PDIFF_7:12

for m being non empty Element of NAT
for x, y being Element of REAL
for z being Element of REAL m
for i being Element of NAT st 1 <= i & i <= m & y = (proj i,m) . z holds
( (Replace z,i,x) - z = Replace (0* m),i,(x - y) & z - (Replace z,i,x) = Replace (0* m),i,(y - x) )

proof end;

theorem Th13: :: PDIFF_7:13

for m being non empty Element of NAT
for x, y being Element of REAL
for i being Element of NAT st 1 <= i & i <= m holds
(reproj i,(0* m)) . (x + y) = ((reproj i,(0* m)) . x) + ((reproj i,(0* m)) . y)

proof end;

theorem Th14: :: PDIFF_7:14

for m being non empty Element of NAT
for x, y being Point of (REAL-NS 1)
for i being Element of NAT st 1 <= i & i <= m holds
(reproj i,(0. (REAL-NS m))) . (x + y) = ((reproj i,(0. (REAL-NS m))) . x) + ((reproj i,(0. (REAL-NS m))) . y)

proof end;

theorem Th15: :: PDIFF_7:15

for m being non empty Element of NAT
for x, a being Element of REAL
for i being Element of NAT st 1 <= i & i <= m holds
(reproj i,(0* m)) . (a * x) = a * ((reproj i,(0* m)) . x)

proof end;

theorem Th16: :: PDIFF_7:16

for m being non empty Element of NAT
for x being Point of (REAL-NS 1)
for a being Element of REAL
for i being Element of NAT st 1 <= i & i <= m holds
(reproj i,(0. (REAL-NS m))) . (a * x) = a * ((reproj i,(0. (REAL-NS m))) . x)

proof end;

theorem Th17: :: PDIFF_7:17

for m being non empty Element of NAT
for x being Element of REAL
for i being Element of NAT st 1 <= i & i <= m & x <> 0 holds
(reproj i,(0* m)) . x <> 0* m

proof end;

theorem Th18: :: PDIFF_7:18

for m being non empty Element of NAT
for x being Point of (REAL-NS 1)
for i being Element of NAT st 1 <= i & i <= m & x <> 0. (REAL-NS 1) holds
(reproj i,(0. (REAL-NS m))) . x <> 0. (REAL-NS m)

proof end;

theorem Th19: :: PDIFF_7:19

for m being non empty Element of NAT
for x, y being Element of REAL
for z being Element of REAL m
for i being Element of NAT st 1 <= i & i <= m & y = (proj i,m) . z holds
( ((reproj i,z) . x) - z = (reproj i,(0* m)) . (x - y) & z - ((reproj i,z) . x) = (reproj i,(0* m)) . (y - x) )

proof end;

theorem Th20: :: PDIFF_7:20

for m being non empty Element of NAT
for x, y being Point of (REAL-NS 1)
for i being Element of NAT
for z being Point of (REAL-NS m) st 1 <= i & i <= m & y = (Proj i,m) . z holds
( ((reproj i,z) . x) - z = (reproj i,(0. (REAL-NS m))) . (x - y) & z - ((reproj i,z) . x) = (reproj i,(0. (REAL-NS m))) . (y - x) )

proof end;

theorem Th21: :: PDIFF_7:21

for n, m being non empty Element of NAT
for i being Element of NAT
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) st f is_differentiable_in x & 1 <= i & i <= m holds
( f is_partial_differentiable_in x,i & partdiff f,x,i = (diff f,x) * (reproj i,(0. (REAL-NS m))) )

proof end;

theorem Th22: :: PDIFF_7:22

for n, m being non empty Element of NAT
for i being Element of NAT
for g being PartFunc of (REAL m),(REAL n)
for y being Element of REAL m st g is_differentiable_in y & 1 <= i & i <= m holds
( g is_partial_differentiable_in y,i & partdiff g,y,i = ((diff g,y) * (reproj i,(0. (REAL-NS m)))) . <*1*> )

proof end;

definition

let n be non empty Element of NAT ;
let f be PartFunc of (REAL n),REAL ;
let x be Element of REAL n;
pred f is_differentiable_in x means :Def1: :: PDIFF_7:def 1
<>* f is_differentiable_in x;

end;

:: deftheorem Def1 defines is_differentiable_in PDIFF_7:def 1 :
for n being non empty Element of NAT
for f being PartFunc of (REAL n),REAL
for x being Element of REAL n holds
( f is_differentiable_in x iff <>* f is_differentiable_in x );

definition

let n be non empty Element of NAT ;
let f be PartFunc of (REAL n),REAL ;
let x be Element of REAL n;
func diff f,x -> Function of (REAL n),REAL equals :: PDIFF_7:def 2
(proj 1,1) * (diff (<>* f),x);
coherence
(proj 1,1) * (diff (<>* f),x) is Function of (REAL n),REAL ;

end;

:: deftheorem defines diff PDIFF_7:def 2 :
for n being non empty Element of NAT
for f being PartFunc of (REAL n),REAL
for x being Element of REAL n holds diff f,x = (proj 1,1) * (diff (<>* f),x);

theorem :: PDIFF_7:23

for m being non empty Element of NAT
for i being Element of NAT
for h being PartFunc of (REAL m),REAL
for y being Element of REAL m st h is_differentiable_in y & 1 <= i & i <= m holds
( h is_partial_differentiable_in y,i & partdiff h,y,i = diff (h * (reproj i,y)),((proj i,m) . y) & partdiff h,y,i = (diff h,y) . ((reproj i,(0* m)) . 1) )

proof end;

theorem Th24: :: PDIFF_7:24

for m being non empty Element of NAT
for v, w, u being FinSequence of REAL m st dom v = dom w & u = v + w holds
Sum u = (Sum v) + (Sum w)

proof end;

theorem Th25: :: PDIFF_7:25

for m being non empty Element of NAT
for r being Real
for w, u being FinSequence of REAL m st u = r (#) w holds
Sum u = r * (Sum w)

proof end;

Lm8: for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m ex L being bounded LinearOperator of m,n st
for h being Element of REAL m ex w being FinSequence of REAL n st
( dom w = Seg m & ( for i being Element of NAT st i in Seg m holds
w . i = ((proj i,m) . h) * (partdiff f,x,i) ) & L . h = Sum w )

proof end;

theorem Th26: :: PDIFF_7:26

for n being non empty Element of NAT
for h, g being FinSequence of REAL n st len h = (len g) + 1 & ( for i being Nat st i in dom g holds
g /. i = (h /. i) - (h /. (i + 1)) ) holds
(h /. 1) - (h /. (len h)) = Sum g

proof end;

theorem Th27: :: PDIFF_7:27

for n being non empty Element of NAT
for h, g, j being FinSequence of REAL n st len h = len j & len g = len j & ( for i being Nat st i in dom j holds
j /. i = (h /. i) - (g /. i) ) holds
Sum j = (Sum h) - (Sum g)

proof end;

theorem Th28: :: PDIFF_7:28

for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for x, y being Element of REAL m ex h being FinSequence of REAL m ex g being FinSequence of REAL n st
( len h = m + 1 & len g = m & ( for i being Nat st i in dom h holds
h /. i = (y | ((m + 1) -' i)) ^ (0* (i -' 1)) ) & ( for i being Nat st i in dom g holds
g /. i = (f /. (x + (h /. i))) - (f /. (x + (h /. (i + 1)))) ) & ( for i being Nat
for hi being Element of REAL m st i in dom h & h /. i = hi holds
|.hi.| <= |.y.| ) & (f /. (x + y)) - (f /. x) = Sum g )

proof end;

theorem Th29: :: PDIFF_7:29

for m being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL 1) ex f0 being PartFunc of (REAL m),REAL st f = <>* f0

proof end;

theorem Th30: :: PDIFF_7:30

for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for f0 being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Element of REAL m
for x0 being Element of (REAL-NS m) st x in dom f & x = x0 & f = f0 holds
f /. x = f0 /. x0

proof end;

definition

let m be non empty Element of NAT ;
let X be Subset of (REAL m);
attr X is open means :Def3: :: PDIFF_7:def 3
ex X0 being Subset of (REAL-NS m) st
( X0 = X & X0 is open );

end;

:: deftheorem Def3 defines open PDIFF_7:def 3 :
for m being non empty Element of NAT
for X being Subset of (REAL m) holds
( X is open iff ex X0 being Subset of (REAL-NS m) st
( X0 = X & X0 is open ) );

theorem Th31: :: PDIFF_7:31

for m being non empty Element of NAT
for X being Subset of (REAL m) holds
( X is open iff for x being Element of REAL m st x in X holds
ex r being Real st
( r > 0 & { y where y is Element of REAL m : |.(y - x).| < r } c= X ) )

proof end;

definition

let m, n be non empty Element of NAT ;
let i be Element of NAT ;
let f be PartFunc of (REAL m),(REAL n);
let X be set ;
pred f is_partial_differentiable_on X,i means :Def4: :: PDIFF_7:def 4
( X c= dom f & ( for x being Element of REAL m st x in X holds
f | X is_partial_differentiable_in x,i ) );

end;

:: deftheorem Def4 defines is_partial_differentiable_on PDIFF_7:def 4 :
for m, n being non empty Element of NAT
for i being Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for X being set holds
( f is_partial_differentiable_on X,i iff ( X c= dom f & ( for x being Element of REAL m st x in X holds
f | X is_partial_differentiable_in x,i ) ) );

theorem Th32: :: PDIFF_7:32

for i being Element of NAT
for X being set
for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n) st f is_partial_differentiable_on X,i holds
X is Subset of (REAL m)

proof end;

theorem Th33: :: PDIFF_7:33

for m, n being non empty Element of NAT
for i being Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n)
for Z being set st f = g holds
( f is_partial_differentiable_on Z,i iff g is_partial_differentiable_on Z,i )

proof end;

theorem Th34: :: PDIFF_7:34

for m, n being non empty Element of NAT
for i being Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for Z being Subset of (REAL m) st Z is open & 1 <= i & i <= m holds
( f is_partial_differentiable_on Z,i iff ( Z c= dom f & ( for x being Element of REAL m st x in Z holds
f is_partial_differentiable_in x,i ) ) )

proof end;

definition

let m, n be non empty Element of NAT ;
let i be Element of NAT ;
let f be PartFunc of (REAL m),(REAL n);
let X be set ;
assume A1: f is_partial_differentiable_on X,i ;
func f `partial| X,i -> PartFunc of (REAL m),(REAL n) means :Def5: :: PDIFF_7:def 5
( dom it = X & ( for x being Element of REAL m st x in X holds
it /. x = partdiff f,x,i ) );
existence
ex b₁ being PartFunc of (REAL m),(REAL n) st
( dom b₁ = X & ( for x being Element of REAL m st x in X holds
b₁ /. x = partdiff f,x,i ) )

proof end;

uniqueness
for b₁, b₂ being PartFunc of (REAL m),(REAL n) st dom b₁ = X & ( for x being Element of REAL m st x in X holds
b₁ /. x = partdiff f,x,i ) & dom b₂ = X & ( for x being Element of REAL m st x in X holds
b₂ /. x = partdiff f,x,i ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines `partial| PDIFF_7:def 5 :
for m, n being non empty Element of NAT
for i being Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for X being set st f is_partial_differentiable_on X,i holds
for b<sub>6</sub> being PartFunc of (REAL m),(REAL n) holds
( b<sub>6</sub> = f `partial| X,i iff ( dom b₆ = X & ( for x being Element of REAL m st x in X holds
b₆ /. x = partdiff f,x,i ) ) );

definition

let m, n be non empty Element of NAT ;
let f be PartFunc of (REAL m),(REAL n);
let x0 be Element of REAL m;
pred f is_continuous_in x0 means :Def6: :: PDIFF_7:def 6
ex y0 being Point of (REAL-NS m) ex g being PartFunc of (REAL-NS m),(REAL-NS n) st
( x0 = y0 & f = g & g is_continuous_in y0 );

end;

:: deftheorem Def6 defines is_continuous_in PDIFF_7:def 6 :
for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for x0 being Element of REAL m holds
( f is_continuous_in x0 iff ex y0 being Point of (REAL-NS m) ex g being PartFunc of (REAL-NS m),(REAL-NS n) st
( x0 = y0 & f = g & g is_continuous_in y0 ) );

theorem Th35: :: PDIFF_7:35

for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Element of REAL m
for y being Point of (REAL-NS m) st f = g & x = y holds
( f is_continuous_in x iff g is_continuous_in y )

proof end;

theorem :: PDIFF_7:36

for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for x0 being Element of REAL m holds
( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in dom f & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) ) )

proof end;

definition

let m, n be non empty Element of NAT ;
let f be PartFunc of (REAL m),(REAL n);
let X be set ;
pred f is_continuous_on X means :Def7: :: PDIFF_7:def 7
( X c= dom f & ( for x0 being Element of REAL m st x0 in X holds
f | X is_continuous_in x0 ) );

end;

:: deftheorem Def7 defines is_continuous_on PDIFF_7:def 7 :
for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for X being set holds
( f is_continuous_on X iff ( X c= dom f & ( for x0 being Element of REAL m st x0 in X holds
f | X is_continuous_in x0 ) ) );

theorem Th37: :: PDIFF_7:37

for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n)
for X being set st f = g holds
( f is_continuous_on X iff g is_continuous_on X )

proof end;

theorem Th38: :: PDIFF_7:38

for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for X being set holds
( f is_continuous_on X iff ( X c= dom f & ( for x0 being Element of REAL m
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) ) )

proof end;

theorem Th39: :: PDIFF_7:39

for m being non empty Element of NAT
for x, y being Element of REAL m
for i being Element of NAT
for xi being Real st 1 <= i & i <= m & y = (reproj i,x) . xi holds
(proj i,m) . y = xi

proof end;

theorem Th40: :: PDIFF_7:40

for m being non empty Element of NAT
for f being PartFunc of (REAL m),REAL
for x, y being Element of REAL m
for i being Element of NAT
for xi being Real st 1 <= i & i <= m & y = (reproj i,x) . xi holds
reproj i,x = reproj i,y

proof end;

theorem Th41: :: PDIFF_7:41

for m being non empty Element of NAT
for f being PartFunc of (REAL m),REAL
for g being PartFunc of REAL ,REAL
for x, y being Element of REAL m
for i being Element of NAT
for xi being Real st 1 <= i & i <= m & y = (reproj i,x) . xi & g = f * (reproj i,x) holds
diff g,xi = partdiff f,y,i

proof end;

theorem Th42: :: PDIFF_7:42

for m being non empty Element of NAT
for f being PartFunc of (REAL m),REAL
for p, q being Real
for x being Element of REAL m
for i being Element of NAT st 1 <= i & i <= m & p < q & ( for h being Real st h in [.p,q.] holds
(reproj i,x) . h in dom f ) & ( for h being Real st h in [.p,q.] holds
f is_partial_differentiable_in (reproj i,x) . h,i ) holds
ex r being Real ex y being Element of REAL m st
( r in ].p,q.[ & y = (reproj i,x) . r & (f /. ((reproj i,x) . q)) - (f /. ((reproj i,x) . p)) = (q - p) * (partdiff f,y,i) )

proof end;

theorem Th43: :: PDIFF_7:43

for m being non empty Element of NAT
for f being PartFunc of (REAL m),REAL
for p, q being Real
for x being Element of REAL m
for i being Element of NAT st 1 <= i & i <= m & p <= q & ( for h being Real st h in [.p,q.] holds
(reproj i,x) . h in dom f ) & ( for h being Real st h in [.p,q.] holds
f is_partial_differentiable_in (reproj i,x) . h,i ) holds
ex r being Real ex y being Element of REAL m st
( r in [.p,q.] & y = (reproj i,x) . r & (f /. ((reproj i,x) . q)) - (f /. ((reproj i,x) . p)) = (q - p) * (partdiff f,y,i) )

proof end;

theorem Th44: :: PDIFF_7:44

for m being non empty Element of NAT
for x, y, z, w being Element of REAL m
for i being Element of NAT
for d, p, q, r being Real st 1 <= i & i <= m & |.(y - x).| < d & |.(z - x).| < d & p = (proj i,m) . y & z = (reproj i,y) . q & r in [.p,q.] & w = (reproj i,y) . r holds
|.(w - x).| < d

proof end;

theorem Th45: :: PDIFF_7:45

for m being non empty Element of NAT
for f being PartFunc of (REAL m),REAL
for X being Subset of (REAL m)
for x, y, z being Element of REAL m
for i being Element of NAT
for d, p, q being Real st 1 <= i & i <= m & X is open & x in X & |.(y - x).| < d & |.(z - x).| < d & X c= dom f & ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i ) & 0 < d & ( for z being Element of REAL m st |.(z - x).| < d holds
z in X ) & z = (reproj i,y) . p & q = (proj i,m) . y holds
ex w being Element of REAL m st
( |.(w - x).| < d & f is_partial_differentiable_in w,i & (f /. z) - (f /. y) = (p - q) * (partdiff f,w,i) )

proof end;

theorem Th46: :: PDIFF_7:46

for m being non empty Element of NAT
for h being FinSequence of REAL m
for y, x being Element of REAL m
for j being Element of NAT st len h = m + 1 & 1 <= j & j <= m & ( for i being Nat st i in dom h holds
h /. i = (y | ((m + 1) -' i)) ^ (0* (i -' 1)) ) holds
x + (h /. j) = (reproj ((m + 1) -' j),(x + (h /. (j + 1)))) . ((proj ((m + 1) -' j),m) . (x + y))

proof end;

theorem Th47: :: PDIFF_7:47

for m being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL 1)
for X being Subset of (REAL m)
for x being Element of REAL m st X is open & x in X & ( for i being Element of NAT st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| X,i is_continuous_on X ) ) holds
( f is_differentiable_in x & ( for h being Element of REAL m ex w being FinSequence of REAL 1 st
( dom w = Seg m & ( for i being Element of NAT st i in Seg m holds
w . i = ((proj i,m) . h) * (partdiff f,x,i) ) & (diff f,x) . h = Sum w ) ) )

proof end;

theorem Th48: :: PDIFF_7:48

for m being non empty Element of NAT
for f being PartFunc of (REAL-NS m),(REAL-NS 1)
for X being Subset of (REAL-NS m)
for x being Point of (REAL-NS m) st X is open & x in X & ( for i being Element of NAT st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| X,i is_continuous_on X ) ) holds
( f is_differentiable_in x & ( for h being Point of (REAL-NS m) ex w being FinSequence of REAL 1 st
( dom w = Seg m & ( for i being Element of NAT st i in Seg m holds
w . i = (partdiff f,x,i) . <*((proj i,m) . h)*> ) & (diff f,x) . h = Sum w ) ) )

proof end;

theorem :: PDIFF_7:49

for m being non empty Element of NAT
for f being PartFunc of (REAL-NS m),(REAL-NS 1)
for X being Subset of (REAL-NS m) st X is open holds
( ( for i being Element of NAT st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| X,i is_continuous_on X ) ) iff ( f is_differentiable_on X & f `| X is_continuous_on X ) )

proof end;