:: by Takao Inou\'e , Adam Naumowicz , Noboru Endou and Yasunari Shidama

::

:: Received April 22, 2010

:: Copyright (c) 2010-2021 Association of Mizar Users

registration

let n be Nat;

let p, q be Element of (TOP-REAL n);

let f, g be real-valued FinSequence;

compatibility

( p = f & q = g implies p + q = f + g ) ;

end;
let p, q be Element of (TOP-REAL n);

let f, g be real-valued FinSequence;

compatibility

( p = f & q = g implies p + q = f + g ) ;

registration

let r, s be Real;

let n be Nat;

let p be Element of (TOP-REAL n);

let f be real-valued FinSequence;

compatibility

( r = s & p = f implies r * p = s * f ) ;

end;
let n be Nat;

let p be Element of (TOP-REAL n);

let f be real-valued FinSequence;

compatibility

( r = s & p = f implies r * p = s * f ) ;

registration

let n be Nat;

let p be Element of (TOP-REAL n);

let f be real-valued FinSequence;

compatibility

( p = f implies - p = - f ) ;

end;
let p be Element of (TOP-REAL n);

let f be real-valued FinSequence;

compatibility

( p = f implies - p = - f ) ;

registration

let n be Nat;

let p, q be Element of (TOP-REAL n);

let f, g be real-valued FinSequence;

compatibility

( p = f & q = g implies p - q = f - g ) ;

end;
let p, q be Element of (TOP-REAL n);

let f, g be real-valued FinSequence;

compatibility

( p = f & q = g implies p - q = f - g ) ;

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 Nat st i <= j holds

i + (j -' i) = (i + j) -' i

proof end;

Lm3: for i, j being Nat st i <= j holds

(0* j) /^ i = 0* (j -' i)

proof end;

Lm4: for i, j being Nat st i > j holds

(0* j) /^ i = 0* (j -' i)

proof end;

theorem :: PDIFF_7:4

theorem Th5: :: PDIFF_7:5

for i, j being Nat

for xi being Element of (REAL-NS 1) st 1 <= i & i <= j holds

||.((reproj (i,(0. (REAL-NS j)))) . xi).|| = ||.xi.||

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 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) )

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 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) )

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 Nat

for nx being Point of (REAL-NS m)

for Z being Subset of (REAL-NS m)

for i being 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 zero Nat

for i being 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 ) ) )

for i being 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 zero Nat

for v being Element of REAL m

for x being Real

for i being Nat holds len (Replace (v,i,x)) = m

proof end;

Lm7: for m being non zero Nat

for x being Real

for i, j being 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 zero Nat

for x, y being Element of REAL

for i being Nat st 1 <= i & i <= m holds

Replace ((0* m),i,(x + y)) = (Replace ((0* m),i,x)) + (Replace ((0* m),i,y))

for x, y being Element of REAL

for i being 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;

registration

let f be real-valued FinSequence;

let i be Nat;

let p be Real;

coherence

Replace (f,i,p) is real-valued

end;
let i be Nat;

let p be Real;

coherence

Replace (f,i,p) is real-valued

proof end;

theorem Th10: :: PDIFF_7:10

for m being non zero Nat

for x, a being Real

for i being Nat st 1 <= i & i <= m holds

(0* m) +* (i,(a * x)) = a * (Replace ((0* m),i,x))

for x, a being Real

for i being Nat st 1 <= i & i <= m holds

(0* m) +* (i,(a * x)) = a * (Replace ((0* m),i,x))

proof end;

theorem Th11: :: PDIFF_7:11

for m being non zero Nat

for x being Element of REAL

for i being Nat st 1 <= i & i <= m & x <> 0 holds

Replace ((0* m),i,x) <> 0* m

for x being Element of REAL

for i being 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 zero Nat

for x, y being Element of REAL

for z being Element of REAL m

for i being Nat st 1 <= i & i <= m & y = (proj (i,m)) . z holds

( (Replace (z,i,x)) - z = (0* m) +* (i,(x - y)) & z - (Replace (z,i,x)) = (0* m) +* (i,(y - x)) )

for x, y being Element of REAL

for z being Element of REAL m

for i being Nat st 1 <= i & i <= m & y = (proj (i,m)) . z holds

( (Replace (z,i,x)) - z = (0* m) +* (i,(x - y)) & z - (Replace (z,i,x)) = (0* m) +* (i,(y - x)) )

proof end;

theorem Th13: :: PDIFF_7:13

for m being non zero Nat

for x, y being Element of REAL

for i being Nat st 1 <= i & i <= m holds

(reproj (i,(0* m))) . (x + y) = ((reproj (i,(0* m))) . x) + ((reproj (i,(0* m))) . y)

for x, y being Element of REAL

for i being 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 zero Nat

for x, y being Point of (REAL-NS 1)

for i being 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)

for x, y being Point of (REAL-NS 1)

for i being 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 zero Nat

for x, a being Real

for i being Nat st 1 <= i & i <= m holds

(reproj (i,(0* m))) . (a * x) = a (#) ((reproj (i,(0* m))) . x)

for x, a being Real

for i being 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 zero Nat

for x being Point of (REAL-NS 1)

for a being Real

for i being Nat st 1 <= i & i <= m holds

(reproj (i,(0. (REAL-NS m)))) . (a * x) = a * ((reproj (i,(0. (REAL-NS m)))) . x)

for x being Point of (REAL-NS 1)

for a being Real

for i being 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 zero Nat

for x being Element of REAL

for i being Nat st 1 <= i & i <= m & x <> 0 holds

(reproj (i,(0* m))) . x <> 0* m

for x being Element of REAL

for i being 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 zero Nat

for x being Point of (REAL-NS 1)

for i being Nat st 1 <= i & i <= m & x <> 0. (REAL-NS 1) holds

(reproj (i,(0. (REAL-NS m)))) . x <> 0. (REAL-NS m)

for x being Point of (REAL-NS 1)

for i being 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 zero Nat

for x, y being Element of REAL

for z being Element of REAL m

for i being 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) )

for x, y being Element of REAL

for z being Element of REAL m

for i being 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 zero Nat

for x, y being Point of (REAL-NS 1)

for i being 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) )

for x, y being Point of (REAL-NS 1)

for i being 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 zero Nat

for i being 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)))) )

for i being 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 zero Nat

for i being 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*> )

for i being 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
end;

:: deftheorem defines is_differentiable_in PDIFF_7:def 1 :

for n being non zero 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 );

for n being non zero 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 zero Nat;

let f be PartFunc of (REAL n),REAL;

let x be Element of REAL n;

(proj (1,1)) * (diff ((<>* f),x)) is Function of (REAL n),REAL ;

end;
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));

(proj (1,1)) * (diff ((<>* f),x)) is Function of (REAL n),REAL ;

:: deftheorem defines diff PDIFF_7:def 2 :

for n being non zero 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));

for n being non zero 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));

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

theorem :: PDIFF_7:23

for m being non zero Nat

for i being 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) )

for i being 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 zero 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)

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 zero Nat

for r being Real

for w, u being FinSequence of REAL m st u = r (#) w holds

Sum u = r * (Sum w)

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 zero Nat

for f being PartFunc of (REAL m),(REAL n)

for x being Element of REAL m ex L being Lipschitzian 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 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 zero 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

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 zero 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)

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 zero 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 )

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 zero Nat

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

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 zero 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

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;

:: deftheorem defines open PDIFF_7:def 3 :

for m being non zero 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 ) );

for m being non zero 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 zero 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 ) )

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 zero Nat;

let i be Nat;

let f be PartFunc of (REAL m),(REAL n);

let X be set ;

end;
let i be Nat;

let f be PartFunc of (REAL m),(REAL n);

let X be set ;

pred f is_partial_differentiable_on X,i means :: 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 ) );

( X c= dom f & ( for x being Element of REAL m st x in X holds

f | X is_partial_differentiable_in x,i ) );

:: deftheorem defines is_partial_differentiable_on PDIFF_7:def 4 :

for m, n being non zero Nat

for i being 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 ) ) );

for m, n being non zero Nat

for i being 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 Th33: :: PDIFF_7:33

for m, n being non zero Nat

for i being 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 )

for i being 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 zero Nat

for i being 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 ) ) )

for i being 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 zero Nat;

let i be Nat;

let f be PartFunc of (REAL m),(REAL n);

let X be set ;

assume A1: f is_partial_differentiable_on X,i ;

ex b_{1} being PartFunc of (REAL m),(REAL n) st

( dom b_{1} = X & ( for x being Element of REAL m st x in X holds

b_{1} /. x = partdiff (f,x,i) ) )

for b_{1}, b_{2} being PartFunc of (REAL m),(REAL n) st dom b_{1} = X & ( for x being Element of REAL m st x in X holds

b_{1} /. x = partdiff (f,x,i) ) & dom b_{2} = X & ( for x being Element of REAL m st x in X holds

b_{2} /. x = partdiff (f,x,i) ) holds

b_{1} = b_{2}

end;
let i be 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 ( dom it = X & ( for x being Element of REAL m st x in X holds

it /. x = partdiff (f,x,i) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def5 defines `partial| PDIFF_7:def 5 :

for m, n being non zero Nat

for i being 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_{6} being PartFunc of (REAL m),(REAL n) holds

( b_{6} = f `partial| (X,i) iff ( dom b_{6} = X & ( for x being Element of REAL m st x in X holds

b_{6} /. x = partdiff (f,x,i) ) ) );

for m, n being non zero Nat

for i being 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

( b

b

definition

let m, n be non zero Nat;

let f be PartFunc of (REAL m),(REAL n);

let x0 be Element of REAL m;

end;
let f be PartFunc of (REAL m),(REAL n);

let x0 be Element of REAL m;

pred f is_continuous_in x0 means :: 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 );

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 );

:: deftheorem defines is_continuous_in PDIFF_7:def 6 :

for m, n being non zero 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 ) );

for m, n being non zero 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 :: PDIFF_7:35

theorem :: PDIFF_7:36

for m, n being non zero 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 ) ) ) ) )

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 zero Nat;

let f be PartFunc of (REAL m),(REAL n);

let X be set ;

end;
let f be PartFunc of (REAL m),(REAL n);

let X be set ;

pred f is_continuous_on X means :: 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 ) );

( X c= dom f & ( for x0 being Element of REAL m st x0 in X holds

f | X is_continuous_in x0 ) );

:: deftheorem defines is_continuous_on PDIFF_7:def 7 :

for m, n being non zero 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 ) ) );

for m, n being non zero 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 zero 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 )

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 zero 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 ) ) ) ) )

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 zero Nat

for x, y being Element of REAL m

for i being Nat

for xi being Real st 1 <= i & i <= m & y = (reproj (i,x)) . xi holds

(proj (i,m)) . y = xi

for x, y being Element of REAL m

for i being 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 zero Nat

for f being PartFunc of (REAL m),REAL

for x, y being Element of REAL m

for i being Nat

for xi being Real st 1 <= i & i <= m & y = (reproj (i,x)) . xi holds

reproj (i,x) = reproj (i,y)

for f being PartFunc of (REAL m),REAL

for x, y being Element of REAL m

for i being 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 zero 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 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)

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 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 zero Nat

for f being PartFunc of (REAL m),REAL

for p, q being Real

for x being Element of REAL m

for i being 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 Element of 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)) )

for f being PartFunc of (REAL m),REAL

for p, q being Real

for x being Element of REAL m

for i being 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 Element of 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 zero Nat

for f being PartFunc of (REAL m),REAL

for p, q being Real

for x being Element of REAL m

for i being 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 Element of 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)) )

for f being PartFunc of (REAL m),REAL

for p, q being Real

for x being Element of REAL m

for i being 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 Element of 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 zero Nat

for x, y, z, w being Element of REAL m

for i being 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

for x, y, z, w being Element of REAL m

for i being 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 zero 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 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)) )

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 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 zero Nat

for h being FinSequence of REAL m

for y, x being Element of REAL m

for j being 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))

for h being FinSequence of REAL m

for y, x being Element of REAL m

for j being 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 zero 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 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 Nat st i in Seg m holds

w . i = ((proj (i,m)) . h) * (partdiff (f,x,i)) ) & (diff (f,x)) . h = Sum w ) ) )

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 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 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 zero 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 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 Nat st i in Seg m holds

w . i = (partdiff (f,x,i)) . <*((proj (i,m)) . h)*> ) & (diff (f,x)) . h = Sum w ) ) )

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 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 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 zero 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 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 ) )

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 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;