:: by Takao Inou\'e , Bing Xie and Xiquan Liang

::

:: Received November 7, 2009

:: Copyright (c) 2009-2018 Association of Mizar Users

theorem Th1: :: PDIFF_4:1

( dom (proj (1,3)) = REAL 3 & rng (proj (1,3)) = REAL & ( for x, y, z being Real holds (proj (1,3)) . <*x,y,z*> = x ) )

proof end;

theorem Th2: :: PDIFF_4:2

( dom (proj (2,3)) = REAL 3 & rng (proj (2,3)) = REAL & ( for x, y, z being Real holds (proj (2,3)) . <*x,y,z*> = y ) )

proof end;

theorem Th3: :: PDIFF_4:3

( dom (proj (3,3)) = REAL 3 & rng (proj (3,3)) = REAL & ( for x, y, z being Real holds (proj (3,3)) . <*x,y,z*> = z ) )

proof end;

theorem Th7: :: PDIFF_4:7

for f being PartFunc of (REAL 3),REAL

for u being Element of REAL 3 holds

( ex x0, y0, z0 being Real st

( u = <*x0,y0,z0*> & SVF1 (1,f,u) is_differentiable_in x0 ) iff f is_partial_differentiable_in u,1 )

for u being Element of REAL 3 holds

( ex x0, y0, z0 being Real st

( u = <*x0,y0,z0*> & SVF1 (1,f,u) is_differentiable_in x0 ) iff f is_partial_differentiable_in u,1 )

proof end;

theorem Th8: :: PDIFF_4:8

for f being PartFunc of (REAL 3),REAL

for u being Element of REAL 3 holds

( ex x0, y0, z0 being Real st

( u = <*x0,y0,z0*> & SVF1 (2,f,u) is_differentiable_in y0 ) iff f is_partial_differentiable_in u,2 )

for u being Element of REAL 3 holds

( ex x0, y0, z0 being Real st

( u = <*x0,y0,z0*> & SVF1 (2,f,u) is_differentiable_in y0 ) iff f is_partial_differentiable_in u,2 )

proof end;

theorem Th9: :: PDIFF_4:9

for f being PartFunc of (REAL 3),REAL

for u being Element of REAL 3 holds

( ex x0, y0, z0 being Real st

( u = <*x0,y0,z0*> & SVF1 (3,f,u) is_differentiable_in z0 ) iff f is_partial_differentiable_in u,3 )

for u being Element of REAL 3 holds

( ex x0, y0, z0 being Real st

( u = <*x0,y0,z0*> & SVF1 (3,f,u) is_differentiable_in z0 ) iff f is_partial_differentiable_in u,3 )

proof end;

theorem :: PDIFF_4:10

for x0, y0, z0 being Real

for u being Element of REAL 3

for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,1 holds

ex N being Neighbourhood of x0 st

( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st

for x being Real st x in N holds

((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) )

for u being Element of REAL 3

for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,1 holds

ex N being Neighbourhood of x0 st

( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st

for x being Real st x in N holds

((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) )

proof end;

theorem :: PDIFF_4:11

for x0, y0, z0 being Real

for u being Element of REAL 3

for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,2 holds

ex N being Neighbourhood of y0 st

( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st

for y being Real st y in N holds

((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) )

for u being Element of REAL 3

for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,2 holds

ex N being Neighbourhood of y0 st

( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st

for y being Real st y in N holds

((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) )

proof end;

theorem :: PDIFF_4:12

for x0, y0, z0 being Real

for u being Element of REAL 3

for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,3 holds

ex N being Neighbourhood of z0 st

( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st

for z being Real st z in N holds

((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) )

for u being Element of REAL 3

for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,3 holds

ex N being Neighbourhood of z0 st

( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st

for z being Real st z in N holds

((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) )

proof end;

theorem Th13: :: PDIFF_4:13

for f being PartFunc of (REAL 3),REAL

for u being Element of REAL 3 holds

( f is_partial_differentiable_in u,1 iff ex x0, y0, z0 being Real st

( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st

( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st

for x being Real st x in N holds

((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) )

for u being Element of REAL 3 holds

( f is_partial_differentiable_in u,1 iff ex x0, y0, z0 being Real st

( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st

( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st

for x being Real st x in N holds

((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) )

proof end;

theorem Th14: :: PDIFF_4:14

for f being PartFunc of (REAL 3),REAL

for u being Element of REAL 3 holds

( f is_partial_differentiable_in u,2 iff ex x0, y0, z0 being Real st

( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st

( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st

for y being Real st y in N holds

((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) )

for u being Element of REAL 3 holds

( f is_partial_differentiable_in u,2 iff ex x0, y0, z0 being Real st

( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st

( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st

for y being Real st y in N holds

((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) )

proof end;

theorem Th15: :: PDIFF_4:15

for f being PartFunc of (REAL 3),REAL

for u being Element of REAL 3 holds

( f is_partial_differentiable_in u,3 iff ex x0, y0, z0 being Real st

( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st

( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st

for z being Real st z in N holds

((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) )

for u being Element of REAL 3 holds

( f is_partial_differentiable_in u,3 iff ex x0, y0, z0 being Real st

( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st

( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st

for z being Real st z in N holds

((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) )

proof end;

Lm1: for x0, y0, z0, r being Real

for u being Element of REAL 3

for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,1 holds

( r = diff ((SVF1 (1,f,u)),x0) iff ex x0, y0, z0 being Real st

( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st

( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st

( r = L . 1 & ( for x being Real st x in N holds

((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) )

proof end;

Lm2: for x0, y0, z0, r being Real

for u being Element of REAL 3

for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,2 holds

( r = diff ((SVF1 (2,f,u)),y0) iff ex x0, y0, z0 being Real st

( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st

( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st

( r = L . 1 & ( for y being Real st y in N holds

((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) )

proof end;

Lm3: for x0, y0, z0, r being Real

for u being Element of REAL 3

for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,3 holds

( r = diff ((SVF1 (3,f,u)),z0) iff ex x0, y0, z0 being Real st

( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st

( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st

( r = L . 1 & ( for z being Real st z in N holds

((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) )

proof end;

theorem Th16: :: PDIFF_4:16

for x0, y0, z0, r being Real

for u being Element of REAL 3

for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,1 holds

( r = partdiff (f,u,1) iff ex x0, y0, z0 being Real st

( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st

( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st

( r = L . 1 & ( for x being Real st x in N holds

((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) )

for u being Element of REAL 3

for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,1 holds

( r = partdiff (f,u,1) iff ex x0, y0, z0 being Real st

( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st

( N c= dom (SVF1 (1,f,u)) & ex L being LinearFunc ex R being RestFunc st

( r = L . 1 & ( for x being Real st x in N holds

((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) )

proof end;

theorem Th17: :: PDIFF_4:17

for x0, y0, z0, r being Real

for u being Element of REAL 3

for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,2 holds

( r = partdiff (f,u,2) iff ex x0, y0, z0 being Real st

( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st

( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st

( r = L . 1 & ( for y being Real st y in N holds

((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) )

for u being Element of REAL 3

for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,2 holds

( r = partdiff (f,u,2) iff ex x0, y0, z0 being Real st

( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st

( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st

( r = L . 1 & ( for y being Real st y in N holds

((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) )

proof end;

theorem Th18: :: PDIFF_4:18

for x0, y0, z0, r being Real

for u being Element of REAL 3

for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,3 holds

( r = partdiff (f,u,3) iff ex x0, y0, z0 being Real st

( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st

( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st

( r = L . 1 & ( for z being Real st z in N holds

((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) )

for u being Element of REAL 3

for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,3 holds

( r = partdiff (f,u,3) iff ex x0, y0, z0 being Real st

( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st

( N c= dom (SVF1 (3,f,u)) & ex L being LinearFunc ex R being RestFunc st

( r = L . 1 & ( for z being Real st z in N holds

((SVF1 (3,f,u)) . z) - ((SVF1 (3,f,u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) )

proof end;

theorem :: PDIFF_4:19

theorem :: PDIFF_4:20

theorem :: PDIFF_4:21

definition

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

let D be set ;

end;
let D be set ;

pred f is_partial_differentiable`1_on D means :: PDIFF_4:def 1

( D c= dom f & ( for u being Element of REAL 3 st u in D holds

f | D is_partial_differentiable_in u,1 ) );

( D c= dom f & ( for u being Element of REAL 3 st u in D holds

f | D is_partial_differentiable_in u,1 ) );

pred f is_partial_differentiable`2_on D means :: PDIFF_4:def 2

( D c= dom f & ( for u being Element of REAL 3 st u in D holds

f | D is_partial_differentiable_in u,2 ) );

( D c= dom f & ( for u being Element of REAL 3 st u in D holds

f | D is_partial_differentiable_in u,2 ) );

pred f is_partial_differentiable`3_on D means :: PDIFF_4:def 3

( D c= dom f & ( for u being Element of REAL 3 st u in D holds

f | D is_partial_differentiable_in u,3 ) );

( D c= dom f & ( for u being Element of REAL 3 st u in D holds

f | D is_partial_differentiable_in u,3 ) );

:: deftheorem defines is_partial_differentiable`1_on PDIFF_4:def 1 :

for f being PartFunc of (REAL 3),REAL

for D being set holds

( f is_partial_differentiable`1_on D iff ( D c= dom f & ( for u being Element of REAL 3 st u in D holds

f | D is_partial_differentiable_in u,1 ) ) );

for f being PartFunc of (REAL 3),REAL

for D being set holds

( f is_partial_differentiable`1_on D iff ( D c= dom f & ( for u being Element of REAL 3 st u in D holds

f | D is_partial_differentiable_in u,1 ) ) );

:: deftheorem defines is_partial_differentiable`2_on PDIFF_4:def 2 :

for f being PartFunc of (REAL 3),REAL

for D being set holds

( f is_partial_differentiable`2_on D iff ( D c= dom f & ( for u being Element of REAL 3 st u in D holds

f | D is_partial_differentiable_in u,2 ) ) );

for f being PartFunc of (REAL 3),REAL

for D being set holds

( f is_partial_differentiable`2_on D iff ( D c= dom f & ( for u being Element of REAL 3 st u in D holds

f | D is_partial_differentiable_in u,2 ) ) );

:: deftheorem defines is_partial_differentiable`3_on PDIFF_4:def 3 :

for f being PartFunc of (REAL 3),REAL

for D being set holds

( f is_partial_differentiable`3_on D iff ( D c= dom f & ( for u being Element of REAL 3 st u in D holds

f | D is_partial_differentiable_in u,3 ) ) );

for f being PartFunc of (REAL 3),REAL

for D being set holds

( f is_partial_differentiable`3_on D iff ( D c= dom f & ( for u being Element of REAL 3 st u in D holds

f | D is_partial_differentiable_in u,3 ) ) );

theorem :: PDIFF_4:22

for D being set

for f being PartFunc of (REAL 3),REAL st f is_partial_differentiable`1_on D holds

( D c= dom f & ( for u being Element of REAL 3 st u in D holds

f is_partial_differentiable_in u,1 ) )

for f being PartFunc of (REAL 3),REAL st f is_partial_differentiable`1_on D holds

( D c= dom f & ( for u being Element of REAL 3 st u in D holds

f is_partial_differentiable_in u,1 ) )

proof end;

theorem :: PDIFF_4:23

for D being set

for f being PartFunc of (REAL 3),REAL st f is_partial_differentiable`2_on D holds

( D c= dom f & ( for u being Element of REAL 3 st u in D holds

f is_partial_differentiable_in u,2 ) )

for f being PartFunc of (REAL 3),REAL st f is_partial_differentiable`2_on D holds

( D c= dom f & ( for u being Element of REAL 3 st u in D holds

f is_partial_differentiable_in u,2 ) )

proof end;

theorem :: PDIFF_4:24

for D being set

for f being PartFunc of (REAL 3),REAL st f is_partial_differentiable`3_on D holds

( D c= dom f & ( for u being Element of REAL 3 st u in D holds

f is_partial_differentiable_in u,3 ) )

for f being PartFunc of (REAL 3),REAL st f is_partial_differentiable`3_on D holds

( D c= dom f & ( for u being Element of REAL 3 st u in D holds

f is_partial_differentiable_in u,3 ) )

proof end;

definition

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

let D be set ;

assume A1: f is_partial_differentiable`1_on D ;

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

( dom b_{1} = D & ( for u being Element of REAL 3 st u in D holds

b_{1} . u = partdiff (f,u,1) ) )

for b_{1}, b_{2} being PartFunc of (REAL 3),REAL st dom b_{1} = D & ( for u being Element of REAL 3 st u in D holds

b_{1} . u = partdiff (f,u,1) ) & dom b_{2} = D & ( for u being Element of REAL 3 st u in D holds

b_{2} . u = partdiff (f,u,1) ) holds

b_{1} = b_{2}

end;
let D be set ;

assume A1: f is_partial_differentiable`1_on D ;

func f `partial1| D -> PartFunc of (REAL 3),REAL means :: PDIFF_4:def 4

( dom it = D & ( for u being Element of REAL 3 st u in D holds

it . u = partdiff (f,u,1) ) );

existence ( dom it = D & ( for u being Element of REAL 3 st u in D holds

it . u = partdiff (f,u,1) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defines `partial1| PDIFF_4:def 4 :

for f being PartFunc of (REAL 3),REAL

for D being set st f is_partial_differentiable`1_on D holds

for b_{3} being PartFunc of (REAL 3),REAL holds

( b_{3} = f `partial1| D iff ( dom b_{3} = D & ( for u being Element of REAL 3 st u in D holds

b_{3} . u = partdiff (f,u,1) ) ) );

for f being PartFunc of (REAL 3),REAL

for D being set st f is_partial_differentiable`1_on D holds

for b

( b

b

definition

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

let D be set ;

assume A1: f is_partial_differentiable`2_on D ;

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

( dom b_{1} = D & ( for u being Element of REAL 3 st u in D holds

b_{1} . u = partdiff (f,u,2) ) )

for b_{1}, b_{2} being PartFunc of (REAL 3),REAL st dom b_{1} = D & ( for u being Element of REAL 3 st u in D holds

b_{1} . u = partdiff (f,u,2) ) & dom b_{2} = D & ( for u being Element of REAL 3 st u in D holds

b_{2} . u = partdiff (f,u,2) ) holds

b_{1} = b_{2}

end;
let D be set ;

assume A1: f is_partial_differentiable`2_on D ;

func f `partial2| D -> PartFunc of (REAL 3),REAL means :: PDIFF_4:def 5

( dom it = D & ( for u being Element of REAL 3 st u in D holds

it . u = partdiff (f,u,2) ) );

existence ( dom it = D & ( for u being Element of REAL 3 st u in D holds

it . u = partdiff (f,u,2) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defines `partial2| PDIFF_4:def 5 :

for f being PartFunc of (REAL 3),REAL

for D being set st f is_partial_differentiable`2_on D holds

for b_{3} being PartFunc of (REAL 3),REAL holds

( b_{3} = f `partial2| D iff ( dom b_{3} = D & ( for u being Element of REAL 3 st u in D holds

b_{3} . u = partdiff (f,u,2) ) ) );

for f being PartFunc of (REAL 3),REAL

for D being set st f is_partial_differentiable`2_on D holds

for b

( b

b

definition

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

let D be set ;

assume A1: f is_partial_differentiable`3_on D ;

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

( dom b_{1} = D & ( for u being Element of REAL 3 st u in D holds

b_{1} . u = partdiff (f,u,3) ) )

for b_{1}, b_{2} being PartFunc of (REAL 3),REAL st dom b_{1} = D & ( for u being Element of REAL 3 st u in D holds

b_{1} . u = partdiff (f,u,3) ) & dom b_{2} = D & ( for u being Element of REAL 3 st u in D holds

b_{2} . u = partdiff (f,u,3) ) holds

b_{1} = b_{2}

end;
let D be set ;

assume A1: f is_partial_differentiable`3_on D ;

func f `partial3| D -> PartFunc of (REAL 3),REAL means :: PDIFF_4:def 6

( dom it = D & ( for u being Element of REAL 3 st u in D holds

it . u = partdiff (f,u,3) ) );

existence ( dom it = D & ( for u being Element of REAL 3 st u in D holds

it . u = partdiff (f,u,3) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defines `partial3| PDIFF_4:def 6 :

for f being PartFunc of (REAL 3),REAL

for D being set st f is_partial_differentiable`3_on D holds

for b_{3} being PartFunc of (REAL 3),REAL holds

( b_{3} = f `partial3| D iff ( dom b_{3} = D & ( for u being Element of REAL 3 st u in D holds

b_{3} . u = partdiff (f,u,3) ) ) );

for f being PartFunc of (REAL 3),REAL

for D being set st f is_partial_differentiable`3_on D holds

for b

( b

b

theorem :: PDIFF_4:25

for f being PartFunc of (REAL 3),REAL

for u0 being Element of REAL 3

for N being Neighbourhood of (proj (1,3)) . u0 st f is_partial_differentiable_in u0,1 & N c= dom (SVF1 (1,f,u0)) holds

for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {((proj (1,3)) . u0)} & rng (h + c) c= N holds

( (h ") (#) (((SVF1 (1,f,u0)) /* (h + c)) - ((SVF1 (1,f,u0)) /* c)) is convergent & partdiff (f,u0,1) = lim ((h ") (#) (((SVF1 (1,f,u0)) /* (h + c)) - ((SVF1 (1,f,u0)) /* c))) )

for u0 being Element of REAL 3

for N being Neighbourhood of (proj (1,3)) . u0 st f is_partial_differentiable_in u0,1 & N c= dom (SVF1 (1,f,u0)) holds

for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {((proj (1,3)) . u0)} & rng (h + c) c= N holds

( (h ") (#) (((SVF1 (1,f,u0)) /* (h + c)) - ((SVF1 (1,f,u0)) /* c)) is convergent & partdiff (f,u0,1) = lim ((h ") (#) (((SVF1 (1,f,u0)) /* (h + c)) - ((SVF1 (1,f,u0)) /* c))) )

proof end;

theorem :: PDIFF_4:26

for f being PartFunc of (REAL 3),REAL

for u0 being Element of REAL 3

for N being Neighbourhood of (proj (2,3)) . u0 st f is_partial_differentiable_in u0,2 & N c= dom (SVF1 (2,f,u0)) holds

for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {((proj (2,3)) . u0)} & rng (h + c) c= N holds

( (h ") (#) (((SVF1 (2,f,u0)) /* (h + c)) - ((SVF1 (2,f,u0)) /* c)) is convergent & partdiff (f,u0,2) = lim ((h ") (#) (((SVF1 (2,f,u0)) /* (h + c)) - ((SVF1 (2,f,u0)) /* c))) )

for u0 being Element of REAL 3

for N being Neighbourhood of (proj (2,3)) . u0 st f is_partial_differentiable_in u0,2 & N c= dom (SVF1 (2,f,u0)) holds

for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {((proj (2,3)) . u0)} & rng (h + c) c= N holds

( (h ") (#) (((SVF1 (2,f,u0)) /* (h + c)) - ((SVF1 (2,f,u0)) /* c)) is convergent & partdiff (f,u0,2) = lim ((h ") (#) (((SVF1 (2,f,u0)) /* (h + c)) - ((SVF1 (2,f,u0)) /* c))) )

proof end;

theorem :: PDIFF_4:27

for f being PartFunc of (REAL 3),REAL

for u0 being Element of REAL 3

for N being Neighbourhood of (proj (3,3)) . u0 st f is_partial_differentiable_in u0,3 & N c= dom (SVF1 (3,f,u0)) holds

for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {((proj (3,3)) . u0)} & rng (h + c) c= N holds

( (h ") (#) (((SVF1 (3,f,u0)) /* (h + c)) - ((SVF1 (3,f,u0)) /* c)) is convergent & partdiff (f,u0,3) = lim ((h ") (#) (((SVF1 (3,f,u0)) /* (h + c)) - ((SVF1 (3,f,u0)) /* c))) )

for u0 being Element of REAL 3

for N being Neighbourhood of (proj (3,3)) . u0 st f is_partial_differentiable_in u0,3 & N c= dom (SVF1 (3,f,u0)) holds

for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {((proj (3,3)) . u0)} & rng (h + c) c= N holds

( (h ") (#) (((SVF1 (3,f,u0)) /* (h + c)) - ((SVF1 (3,f,u0)) /* c)) is convergent & partdiff (f,u0,3) = lim ((h ") (#) (((SVF1 (3,f,u0)) /* (h + c)) - ((SVF1 (3,f,u0)) /* c))) )

proof end;

theorem :: PDIFF_4:28

for u0 being Element of REAL 3

for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_partial_differentiable_in u0,1 & f2 is_partial_differentiable_in u0,1 holds

f1 (#) f2 is_partial_differentiable_in u0,1

for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_partial_differentiable_in u0,1 & f2 is_partial_differentiable_in u0,1 holds

f1 (#) f2 is_partial_differentiable_in u0,1

proof end;

theorem :: PDIFF_4:29

for u0 being Element of REAL 3

for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_partial_differentiable_in u0,2 & f2 is_partial_differentiable_in u0,2 holds

f1 (#) f2 is_partial_differentiable_in u0,2

for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_partial_differentiable_in u0,2 & f2 is_partial_differentiable_in u0,2 holds

f1 (#) f2 is_partial_differentiable_in u0,2

proof end;

theorem :: PDIFF_4:30

for u0 being Element of REAL 3

for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_partial_differentiable_in u0,3 & f2 is_partial_differentiable_in u0,3 holds

f1 (#) f2 is_partial_differentiable_in u0,3

for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_partial_differentiable_in u0,3 & f2 is_partial_differentiable_in u0,3 holds

f1 (#) f2 is_partial_differentiable_in u0,3

proof end;

theorem :: PDIFF_4:31

for f being PartFunc of (REAL 3),REAL

for u0 being Element of REAL 3 st f is_partial_differentiable_in u0,1 holds

SVF1 (1,f,u0) is_continuous_in (proj (1,3)) . u0 by FDIFF_1:24;

for u0 being Element of REAL 3 st f is_partial_differentiable_in u0,1 holds

SVF1 (1,f,u0) is_continuous_in (proj (1,3)) . u0 by FDIFF_1:24;

theorem :: PDIFF_4:32

for f being PartFunc of (REAL 3),REAL

for u0 being Element of REAL 3 st f is_partial_differentiable_in u0,2 holds

SVF1 (2,f,u0) is_continuous_in (proj (2,3)) . u0 by FDIFF_1:24;

for u0 being Element of REAL 3 st f is_partial_differentiable_in u0,2 holds

SVF1 (2,f,u0) is_continuous_in (proj (2,3)) . u0 by FDIFF_1:24;

theorem :: PDIFF_4:33

for f being PartFunc of (REAL 3),REAL

for u0 being Element of REAL 3 st f is_partial_differentiable_in u0,3 holds

SVF1 (3,f,u0) is_continuous_in (proj (3,3)) . u0 by FDIFF_1:24;

for u0 being Element of REAL 3 st f is_partial_differentiable_in u0,3 holds

SVF1 (3,f,u0) is_continuous_in (proj (3,3)) . u0 by FDIFF_1:24;

Lm4: for x1, x2, y1, y2, z1, z2 being Real holds |[x1,y1,z1]| + |[x2,y2,z2]| = |[(x1 + x2),(y1 + y2),(z1 + z2)]|

proof end;

definition

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

let p be Element of REAL 3;

(((partdiff (f,p,1)) * <e1>) + ((partdiff (f,p,2)) * <e2>)) + ((partdiff (f,p,3)) * <e3>) is Element of REAL 3 ;

end;
let p be Element of REAL 3;

func grad (f,p) -> Element of REAL 3 equals :: PDIFF_4:def 7

(((partdiff (f,p,1)) * <e1>) + ((partdiff (f,p,2)) * <e2>)) + ((partdiff (f,p,3)) * <e3>);

coherence (((partdiff (f,p,1)) * <e1>) + ((partdiff (f,p,2)) * <e2>)) + ((partdiff (f,p,3)) * <e3>);

(((partdiff (f,p,1)) * <e1>) + ((partdiff (f,p,2)) * <e2>)) + ((partdiff (f,p,3)) * <e3>) is Element of REAL 3 ;

:: deftheorem defines grad PDIFF_4:def 7 :

for f being PartFunc of (REAL 3),REAL

for p being Element of REAL 3 holds grad (f,p) = (((partdiff (f,p,1)) * <e1>) + ((partdiff (f,p,2)) * <e2>)) + ((partdiff (f,p,3)) * <e3>);

for f being PartFunc of (REAL 3),REAL

for p being Element of REAL 3 holds grad (f,p) = (((partdiff (f,p,1)) * <e1>) + ((partdiff (f,p,2)) * <e2>)) + ((partdiff (f,p,3)) * <e3>);

reconsider jj = 1 as Real ;

theorem Th34: :: PDIFF_4:34

for p being Element of REAL 3

for f being PartFunc of (REAL 3),REAL holds grad (f,p) = |[(partdiff (f,p,1)),(partdiff (f,p,2)),(partdiff (f,p,3))]|

for f being PartFunc of (REAL 3),REAL holds grad (f,p) = |[(partdiff (f,p,1)),(partdiff (f,p,2)),(partdiff (f,p,3))]|

proof end;

theorem Th35: :: PDIFF_4:35

for p being Element of REAL 3

for f, g being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 & g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3 holds

grad ((f + g),p) = (grad (f,p)) + (grad (g,p))

for f, g being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 & g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3 holds

grad ((f + g),p) = (grad (f,p)) + (grad (g,p))

proof end;

theorem Th36: :: PDIFF_4:36

for p being Element of REAL 3

for f, g being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 & g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3 holds

grad ((f - g),p) = (grad (f,p)) - (grad (g,p))

for f, g being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 & g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3 holds

grad ((f - g),p) = (grad (f,p)) - (grad (g,p))

proof end;

theorem Th37: :: PDIFF_4:37

for r being Real

for p being Element of REAL 3

for f being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 holds

grad ((r (#) f),p) = r * (grad (f,p))

for p being Element of REAL 3

for f being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 holds

grad ((r (#) f),p) = r * (grad (f,p))

proof end;

theorem :: PDIFF_4:38

for s, t being Real

for p being Element of REAL 3

for f, g being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 & g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3 holds

grad (((s (#) f) + (t (#) g)),p) = (s * (grad (f,p))) + (t * (grad (g,p)))

for p being Element of REAL 3

for f, g being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 & g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3 holds

grad (((s (#) f) + (t (#) g)),p) = (s * (grad (f,p))) + (t * (grad (g,p)))

proof end;

theorem :: PDIFF_4:39

for s, t being Real

for p being Element of REAL 3

for f, g being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 & g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3 holds

grad (((s (#) f) - (t (#) g)),p) = (s * (grad (f,p))) - (t * (grad (g,p)))

for p being Element of REAL 3

for f, g being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 & g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3 holds

grad (((s (#) f) - (t (#) g)),p) = (s * (grad (f,p))) - (t * (grad (g,p)))

proof end;

theorem :: PDIFF_4:40

for p being Element of REAL 3

for f being PartFunc of (REAL 3),REAL st f is total & f is constant holds

grad (f,p) = 0.REAL 3

for f being PartFunc of (REAL 3),REAL st f is total & f is constant holds

grad (f,p) = 0.REAL 3

proof end;

definition

let a be Element of REAL 3;

|[((a . 1) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)))),((a . 2) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)))),((a . 3) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2))))]| is Element of REAL 3 ;

end;
func unitvector a -> Element of REAL 3 equals :: PDIFF_4:def 8

|[((a . 1) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)))),((a . 2) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)))),((a . 3) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2))))]|;

coherence |[((a . 1) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)))),((a . 2) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)))),((a . 3) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2))))]|;

|[((a . 1) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)))),((a . 2) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)))),((a . 3) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2))))]| is Element of REAL 3 ;

:: deftheorem defines unitvector PDIFF_4:def 8 :

for a being Element of REAL 3 holds unitvector a = |[((a . 1) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)))),((a . 2) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)))),((a . 3) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2))))]|;

for a being Element of REAL 3 holds unitvector a = |[((a . 1) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)))),((a . 2) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)))),((a . 3) / (sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2))))]|;

definition

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

let p, a be Element of REAL 3;

(((partdiff (f,p,1)) * ((unitvector a) . 1)) + ((partdiff (f,p,2)) * ((unitvector a) . 2))) + ((partdiff (f,p,3)) * ((unitvector a) . 3)) is Real ;

end;
let p, a be Element of REAL 3;

func Directiondiff (f,p,a) -> Real equals :: PDIFF_4:def 9

(((partdiff (f,p,1)) * ((unitvector a) . 1)) + ((partdiff (f,p,2)) * ((unitvector a) . 2))) + ((partdiff (f,p,3)) * ((unitvector a) . 3));

coherence (((partdiff (f,p,1)) * ((unitvector a) . 1)) + ((partdiff (f,p,2)) * ((unitvector a) . 2))) + ((partdiff (f,p,3)) * ((unitvector a) . 3));

(((partdiff (f,p,1)) * ((unitvector a) . 1)) + ((partdiff (f,p,2)) * ((unitvector a) . 2))) + ((partdiff (f,p,3)) * ((unitvector a) . 3)) is Real ;

:: deftheorem defines Directiondiff PDIFF_4:def 9 :

for f being PartFunc of (REAL 3),REAL

for p, a being Element of REAL 3 holds Directiondiff (f,p,a) = (((partdiff (f,p,1)) * ((unitvector a) . 1)) + ((partdiff (f,p,2)) * ((unitvector a) . 2))) + ((partdiff (f,p,3)) * ((unitvector a) . 3));

for f being PartFunc of (REAL 3),REAL

for p, a being Element of REAL 3 holds Directiondiff (f,p,a) = (((partdiff (f,p,1)) * ((unitvector a) . 1)) + ((partdiff (f,p,2)) * ((unitvector a) . 2))) + ((partdiff (f,p,3)) * ((unitvector a) . 3));

theorem :: PDIFF_4:41

for x0, y0, z0 being Real

for p, a being Element of REAL 3

for f being PartFunc of (REAL 3),REAL st a = <*x0,y0,z0*> holds

Directiondiff (f,p,a) = ((((partdiff (f,p,1)) * x0) / (sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2)))) + (((partdiff (f,p,2)) * y0) / (sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2))))) + (((partdiff (f,p,3)) * z0) / (sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2))))

for p, a being Element of REAL 3

for f being PartFunc of (REAL 3),REAL st a = <*x0,y0,z0*> holds

Directiondiff (f,p,a) = ((((partdiff (f,p,1)) * x0) / (sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2)))) + (((partdiff (f,p,2)) * y0) / (sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2))))) + (((partdiff (f,p,3)) * z0) / (sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2))))

proof end;

theorem :: PDIFF_4:42

for p, a being Element of REAL 3

for f being PartFunc of (REAL 3),REAL holds Directiondiff (f,p,a) = |((grad (f,p)),(unitvector a))|

for f being PartFunc of (REAL 3),REAL holds Directiondiff (f,p,a) = |((grad (f,p)),(unitvector a))|

proof end;

definition

let f1, f2, f3 be PartFunc of (REAL 3),REAL;

let p be Element of REAL 3;

((((partdiff (f3,p,2)) - (partdiff (f2,p,3))) * <e1>) + (((partdiff (f1,p,3)) - (partdiff (f3,p,1))) * <e2>)) + (((partdiff (f2,p,1)) - (partdiff (f1,p,2))) * <e3>) is Element of REAL 3 ;

end;
let p be Element of REAL 3;

func curl (f1,f2,f3,p) -> Element of REAL 3 equals :: PDIFF_4:def 10

((((partdiff (f3,p,2)) - (partdiff (f2,p,3))) * <e1>) + (((partdiff (f1,p,3)) - (partdiff (f3,p,1))) * <e2>)) + (((partdiff (f2,p,1)) - (partdiff (f1,p,2))) * <e3>);

coherence ((((partdiff (f3,p,2)) - (partdiff (f2,p,3))) * <e1>) + (((partdiff (f1,p,3)) - (partdiff (f3,p,1))) * <e2>)) + (((partdiff (f2,p,1)) - (partdiff (f1,p,2))) * <e3>);

((((partdiff (f3,p,2)) - (partdiff (f2,p,3))) * <e1>) + (((partdiff (f1,p,3)) - (partdiff (f3,p,1))) * <e2>)) + (((partdiff (f2,p,1)) - (partdiff (f1,p,2))) * <e3>) is Element of REAL 3 ;

:: deftheorem defines curl PDIFF_4:def 10 :

for f1, f2, f3 being PartFunc of (REAL 3),REAL

for p being Element of REAL 3 holds curl (f1,f2,f3,p) = ((((partdiff (f3,p,2)) - (partdiff (f2,p,3))) * <e1>) + (((partdiff (f1,p,3)) - (partdiff (f3,p,1))) * <e2>)) + (((partdiff (f2,p,1)) - (partdiff (f1,p,2))) * <e3>);

for f1, f2, f3 being PartFunc of (REAL 3),REAL

for p being Element of REAL 3 holds curl (f1,f2,f3,p) = ((((partdiff (f3,p,2)) - (partdiff (f2,p,3))) * <e1>) + (((partdiff (f1,p,3)) - (partdiff (f3,p,1))) * <e2>)) + (((partdiff (f2,p,1)) - (partdiff (f1,p,2))) * <e3>);

theorem :: PDIFF_4:43

for p being Element of REAL 3

for f1, f2, f3 being PartFunc of (REAL 3),REAL holds curl (f1,f2,f3,p) = |[((partdiff (f3,p,2)) - (partdiff (f2,p,3))),((partdiff (f1,p,3)) - (partdiff (f3,p,1))),((partdiff (f2,p,1)) - (partdiff (f1,p,2)))]|

for f1, f2, f3 being PartFunc of (REAL 3),REAL holds curl (f1,f2,f3,p) = |[((partdiff (f3,p,2)) - (partdiff (f2,p,3))),((partdiff (f1,p,3)) - (partdiff (f3,p,1))),((partdiff (f2,p,1)) - (partdiff (f1,p,2)))]|

proof end;