:: by Keiko Narita , Artur Korni\l owicz and Yasunari Shidama

::

:: Received September 28, 2011

:: Copyright (c) 2011-2016 Association of Mizar Users

set ZR = [#] REAL;

Lm1: the carrier of (REAL-NS 1) = REAL 1

by REAL_NS1:def 4;

definition

let n be non zero Element of NAT ;

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

let x be Real;

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

let x be Real;

pred f is_differentiable_in x means :: NDIFF_4:def 1

ex g being PartFunc of REAL,(REAL-NS n) st

( f = g & g is_differentiable_in x );

ex g being PartFunc of REAL,(REAL-NS n) st

( f = g & g is_differentiable_in x );

:: deftheorem defines is_differentiable_in NDIFF_4:def 1 :

for n being non zero Element of NAT

for f being PartFunc of REAL,(REAL n)

for x being Real holds

( f is_differentiable_in x iff ex g being PartFunc of REAL,(REAL-NS n) st

( f = g & g is_differentiable_in x ) );

for n being non zero Element of NAT

for f being PartFunc of REAL,(REAL n)

for x being Real holds

( f is_differentiable_in x iff ex g being PartFunc of REAL,(REAL-NS n) st

( f = g & g is_differentiable_in x ) );

theorem :: NDIFF_4:2

definition

let n be non zero Element of NAT ;

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

let x be Real;

ex b_{1} being Element of REAL n ex g being PartFunc of REAL,(REAL-NS n) st

( f = g & b_{1} = diff (g,x) )

for b_{1}, b_{2} being Element of REAL n st ex g being PartFunc of REAL,(REAL-NS n) st

( f = g & b_{1} = diff (g,x) ) & ex g being PartFunc of REAL,(REAL-NS n) st

( f = g & b_{2} = diff (g,x) ) holds

b_{1} = b_{2}
;

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

let x be Real;

func diff (f,x) -> Element of REAL n means :Def2: :: NDIFF_4:def 2

ex g being PartFunc of REAL,(REAL-NS n) st

( f = g & it = diff (g,x) );

existence ex g being PartFunc of REAL,(REAL-NS n) st

( f = g & it = diff (g,x) );

ex b

( f = g & b

proof end;

uniqueness for b

( f = g & b

( f = g & b

b

:: deftheorem Def2 defines diff NDIFF_4:def 2 :

for n being non zero Element of NAT

for f being PartFunc of REAL,(REAL n)

for x being Real

for b_{4} being Element of REAL n holds

( b_{4} = diff (f,x) iff ex g being PartFunc of REAL,(REAL-NS n) st

( f = g & b_{4} = diff (g,x) ) );

for n being non zero Element of NAT

for f being PartFunc of REAL,(REAL n)

for x being Real

for b

( b

( f = g & b

theorem Th3: :: NDIFF_4:3

for n being non zero Element of NAT

for f being PartFunc of REAL,(REAL n)

for h being PartFunc of REAL,(REAL-NS n)

for x being Real st h = f holds

diff (f,x) = diff (h,x)

for f being PartFunc of REAL,(REAL n)

for h being PartFunc of REAL,(REAL-NS n)

for x being Real st h = f holds

diff (f,x) = diff (h,x)

proof end;

definition

let n be non zero Element of NAT ;

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

let X be set ;

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

let X be set ;

pred f is_differentiable_on X means :: NDIFF_4:def 3

( X c= dom f & ( for x being Real st x in X holds

f | X is_differentiable_in x ) );

( X c= dom f & ( for x being Real st x in X holds

f | X is_differentiable_in x ) );

:: deftheorem defines is_differentiable_on NDIFF_4:def 3 :

for n being non zero Element of NAT

for f being PartFunc of REAL,(REAL n)

for X being set holds

( f is_differentiable_on X iff ( X c= dom f & ( for x being Real st x in X holds

f | X is_differentiable_in x ) ) );

for n being non zero Element of NAT

for f being PartFunc of REAL,(REAL n)

for X being set holds

( f is_differentiable_on X iff ( X c= dom f & ( for x being Real st x in X holds

f | X is_differentiable_in x ) ) );

theorem Th5: :: NDIFF_4:5

for n being non zero Element of NAT

for Z being open Subset of REAL

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

( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Real st x in Z holds

f is_differentiable_in x ) ) )

for Z being open Subset of REAL

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

( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Real st x in Z holds

f is_differentiable_in x ) ) )

proof end;

theorem Th6: :: NDIFF_4:6

for n being non zero Element of NAT

for Y being Subset of REAL

for f being PartFunc of REAL,(REAL n) st f is_differentiable_on Y holds

Y is open

for Y being Subset of REAL

for f being PartFunc of REAL,(REAL n) st f is_differentiable_on Y holds

Y is open

proof end;

definition

let n be non zero Element of NAT ;

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

let X be set ;

assume A1: f is_differentiable_on X ;

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

( dom b_{1} = X & ( for x being Real st x in X holds

b_{1} . x = diff (f,x) ) )

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

b_{1} . x = diff (f,x) ) & dom b_{2} = X & ( for x being Real st x in X holds

b_{2} . x = diff (f,x) ) holds

b_{1} = b_{2}

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

let X be set ;

assume A1: f is_differentiable_on X ;

func f `| X -> PartFunc of REAL,(REAL n) means :Def4: :: NDIFF_4:def 4

( dom it = X & ( for x being Real st x in X holds

it . x = diff (f,x) ) );

existence ( dom it = X & ( for x being Real st x in X holds

it . x = diff (f,x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def4 defines `| NDIFF_4:def 4 :

for n being non zero Element of NAT

for f being PartFunc of REAL,(REAL n)

for X being set st f is_differentiable_on X holds

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

( b_{4} = f `| X iff ( dom b_{4} = X & ( for x being Real st x in X holds

b_{4} . x = diff (f,x) ) ) );

for n being non zero Element of NAT

for f being PartFunc of REAL,(REAL n)

for X being set st f is_differentiable_on X holds

for b

( b

b

theorem :: NDIFF_4:7

for n being non zero Element of NAT

for Z being open Subset of REAL

for f being PartFunc of REAL,(REAL n) st Z c= dom f & ex r being Element of REAL n st rng f = {r} holds

( f is_differentiable_on Z & ( for x being Real st x in Z holds

(f `| Z) /. x = 0* n ) )

for Z being open Subset of REAL

for f being PartFunc of REAL,(REAL n) st Z c= dom f & ex r being Element of REAL n st rng f = {r} holds

( f is_differentiable_on Z & ( for x being Real st x in Z holds

(f `| Z) /. x = 0* n ) )

proof end;

theorem :: NDIFF_4:8

for n being non zero Element of NAT

for x0 being Real

for f being PartFunc of REAL,(REAL n)

for g being PartFunc of REAL,(REAL-NS n)

for N being Neighbourhood of x0 st f = g & f is_differentiable_in x0 & N c= dom f holds

for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= N holds

( (h ") (#) ((g /* (h + c)) - (g /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((g /* (h + c)) - (g /* c))) )

for x0 being Real

for f being PartFunc of REAL,(REAL n)

for g being PartFunc of REAL,(REAL-NS n)

for N being Neighbourhood of x0 st f = g & f is_differentiable_in x0 & N c= dom f holds

for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= N holds

( (h ") (#) ((g /* (h + c)) - (g /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((g /* (h + c)) - (g /* c))) )

proof end;

theorem Th9: :: NDIFF_4:9

for x0, r being Real

for n being non zero Element of NAT

for f being PartFunc of REAL,(REAL n) st f is_differentiable_in x0 holds

( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) )

for n being non zero Element of NAT

for f being PartFunc of REAL,(REAL n) st f is_differentiable_in x0 holds

( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) )

proof end;

theorem Th10: :: NDIFF_4:10

for x0 being Real

for n being non zero Element of NAT

for f being PartFunc of REAL,(REAL n) st f is_differentiable_in x0 holds

( - f is_differentiable_in x0 & diff ((- f),x0) = - (diff (f,x0)) )

for n being non zero Element of NAT

for f being PartFunc of REAL,(REAL n) st f is_differentiable_in x0 holds

( - f is_differentiable_in x0 & diff ((- f),x0) = - (diff (f,x0)) )

proof end;

theorem Th11: :: NDIFF_4:11

for x0 being Real

for n being non zero Element of NAT

for f1, f2 being PartFunc of REAL,(REAL n) st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds

( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) )

for n being non zero Element of NAT

for f1, f2 being PartFunc of REAL,(REAL n) st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds

( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) )

proof end;

theorem :: NDIFF_4:12

for x0 being Real

for n being non zero Element of NAT

for f1, f2 being PartFunc of REAL,(REAL n) st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds

( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) )

for n being non zero Element of NAT

for f1, f2 being PartFunc of REAL,(REAL n) st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds

( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) )

proof end;

theorem Th13: :: NDIFF_4:13

for r being Real

for n being non zero Element of NAT

for Z being open Subset of REAL

for f being PartFunc of REAL,(REAL n) st Z c= dom f & f is_differentiable_on Z holds

( r (#) f is_differentiable_on Z & ( for x being Real st x in Z holds

((r (#) f) `| Z) . x = r * (diff (f,x)) ) )

for n being non zero Element of NAT

for Z being open Subset of REAL

for f being PartFunc of REAL,(REAL n) st Z c= dom f & f is_differentiable_on Z holds

( r (#) f is_differentiable_on Z & ( for x being Real st x in Z holds

((r (#) f) `| Z) . x = r * (diff (f,x)) ) )

proof end;

theorem Th14: :: NDIFF_4:14

for n being non zero Element of NAT

for Z being open Subset of REAL

for f being PartFunc of REAL,(REAL n) st Z c= dom f & f is_differentiable_on Z holds

( - f is_differentiable_on Z & ( for x being Real st x in Z holds

((- f) `| Z) . x = - (diff (f,x)) ) )

for Z being open Subset of REAL

for f being PartFunc of REAL,(REAL n) st Z c= dom f & f is_differentiable_on Z holds

( - f is_differentiable_on Z & ( for x being Real st x in Z holds

((- f) `| Z) . x = - (diff (f,x)) ) )

proof end;

theorem Th15: :: NDIFF_4:15

for n being non zero Element of NAT

for Z being open Subset of REAL

for f1, f2 being PartFunc of REAL,(REAL n) st Z c= dom (f1 + f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds

( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds

((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x)) ) )

for Z being open Subset of REAL

for f1, f2 being PartFunc of REAL,(REAL n) st Z c= dom (f1 + f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds

( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds

((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x)) ) )

proof end;

theorem :: NDIFF_4:16

for n being non zero Element of NAT

for Z being open Subset of REAL

for f1, f2 being PartFunc of REAL,(REAL n) st Z c= dom (f1 - f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds

( f1 - f2 is_differentiable_on Z & ( for x being Real st x in Z holds

((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x)) ) )

for Z being open Subset of REAL

for f1, f2 being PartFunc of REAL,(REAL n) st Z c= dom (f1 - f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds

( f1 - f2 is_differentiable_on Z & ( for x being Real st x in Z holds

((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x)) ) )

proof end;

theorem :: NDIFF_4:17

for n being non zero Element of NAT

for Z being open Subset of REAL

for f being PartFunc of REAL,(REAL n) st Z c= dom f & f | Z is constant holds

( f is_differentiable_on Z & ( for x being Real st x in Z holds

(f `| Z) . x = 0* n ) )

for Z being open Subset of REAL

for f being PartFunc of REAL,(REAL n) st Z c= dom f & f | Z is constant holds

( f is_differentiable_on Z & ( for x being Real st x in Z holds

(f `| Z) . x = 0* n ) )

proof end;

theorem Th18: :: NDIFF_4:18

for n being non zero Element of NAT

for Z being open Subset of REAL

for f being PartFunc of REAL,(REAL n)

for r, p being Element of REAL n st Z c= dom f & ( for x being Real st x in Z holds

f /. x = (x * r) + p ) holds

( f is_differentiable_on Z & ( for x being Real st x in Z holds

(f `| Z) . x = r ) )

for Z being open Subset of REAL

for f being PartFunc of REAL,(REAL n)

for r, p being Element of REAL n st Z c= dom f & ( for x being Real st x in Z holds

f /. x = (x * r) + p ) holds

( f is_differentiable_on Z & ( for x being Real st x in Z holds

(f `| Z) . x = r ) )

proof end;

theorem :: NDIFF_4:19

for n being non zero Element of NAT

for f being PartFunc of REAL,(REAL n)

for x0 being Real st f is_differentiable_in x0 holds

f is_continuous_in x0 by NDIFF_3:22, NFCONT_4:def 1;

for f being PartFunc of REAL,(REAL n)

for x0 being Real st f is_differentiable_in x0 holds

f is_continuous_in x0 by NDIFF_3:22, NFCONT_4:def 1;

theorem :: NDIFF_4:20

for X being set

for n being non zero Element of NAT

for f being PartFunc of REAL,(REAL n) st f is_differentiable_on X holds

f | X is continuous

for n being non zero Element of NAT

for f being PartFunc of REAL,(REAL n) st f is_differentiable_on X holds

f | X is continuous

proof end;

theorem Th21: :: NDIFF_4:21

for X being set

for n being non zero Element of NAT

for Z being open Subset of REAL

for f being PartFunc of REAL,(REAL n) st f is_differentiable_on X & Z c= X holds

f is_differentiable_on Z

for n being non zero Element of NAT

for Z being open Subset of REAL

for f being PartFunc of REAL,(REAL n) st f is_differentiable_on X & Z c= X holds

f is_differentiable_on Z

proof end;

:: deftheorem Def5 defines differentiable NDIFF_4:def 5 :

for n being non zero Element of NAT

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

( f is differentiable iff f is_differentiable_on dom f );

for n being non zero Element of NAT

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

( f is differentiable iff f is_differentiable_on dom f );

registration

let n be non zero Element of NAT ;

coherence

for b_{1} being Function of REAL,(REAL n) st b_{1} = REAL --> (0* n) holds

b_{1} is differentiable

end;
coherence

for b

b

proof end;

registration

let n be non zero Element of NAT ;

ex b_{1} being Function of REAL,(REAL n) st b_{1} is differentiable

end;
cluster Relation-like REAL -defined REAL n -valued non empty Function-like total quasi_total Function-yielding V237() V238() V239() differentiable for Element of K16(K17(REAL,(REAL n)));

existence ex b

proof end;

theorem :: NDIFF_4:22

theorem Th23: :: NDIFF_4:23

for n being non zero Element of NAT

for R being PartFunc of REAL,(REAL-NS n) st R is total holds

( R is RestFunc-like iff for r being Real st r > 0 holds

ex d being Real st

( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds

(|.z.| ") * ||.(R /. z).|| < r ) ) )

for R being PartFunc of REAL,(REAL-NS n) st R is total holds

( R is RestFunc-like iff for r being Real st r > 0 holds

ex d being Real st

( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds

(|.z.| ") * ||.(R /. z).|| < r ) ) )

proof end;

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

theorem Th24: :: NDIFF_4:24

for i being Element of NAT

for n being non zero Element of NAT

for g being PartFunc of REAL,(REAL-NS n)

for x0 being Real st 1 <= i & i <= n & g is_differentiable_in x0 holds

( (Proj (i,n)) * g is_differentiable_in x0 & (Proj (i,n)) . (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) )

for n being non zero Element of NAT

for g being PartFunc of REAL,(REAL-NS n)

for x0 being Real st 1 <= i & i <= n & g is_differentiable_in x0 holds

( (Proj (i,n)) * g is_differentiable_in x0 & (Proj (i,n)) . (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) )

proof end;

theorem Th25: :: NDIFF_4:25

for n being non zero Element of NAT

for g being PartFunc of REAL,(REAL-NS n)

for x0 being Real holds

( g is_differentiable_in x0 iff for i being Element of NAT st 1 <= i & i <= n holds

(Proj (i,n)) * g is_differentiable_in x0 )

for g being PartFunc of REAL,(REAL-NS n)

for x0 being Real holds

( g is_differentiable_in x0 iff for i being Element of NAT st 1 <= i & i <= n holds

(Proj (i,n)) * g is_differentiable_in x0 )

proof end;

theorem :: NDIFF_4:26

for i being Element of NAT

for n being non zero Element of NAT

for f being PartFunc of REAL,(REAL n)

for x0 being Real st 1 <= i & i <= n & f is_differentiable_in x0 holds

( (Proj (i,n)) * f is_differentiable_in x0 & (Proj (i,n)) . (diff (f,x0)) = diff (((Proj (i,n)) * f),x0) )

for n being non zero Element of NAT

for f being PartFunc of REAL,(REAL n)

for x0 being Real st 1 <= i & i <= n & f is_differentiable_in x0 holds

( (Proj (i,n)) * f is_differentiable_in x0 & (Proj (i,n)) . (diff (f,x0)) = diff (((Proj (i,n)) * f),x0) )

proof end;

theorem :: NDIFF_4:27

for n being non zero Element of NAT

for f being PartFunc of REAL,(REAL n)

for x0 being Real holds

( f is_differentiable_in x0 iff for i being Element of NAT st 1 <= i & i <= n holds

(Proj (i,n)) * f is_differentiable_in x0 )

for f being PartFunc of REAL,(REAL n)

for x0 being Real holds

( f is_differentiable_in x0 iff for i being Element of NAT st 1 <= i & i <= n holds

(Proj (i,n)) * f is_differentiable_in x0 )

proof end;

theorem Th28: :: NDIFF_4:28

for X being set

for i being Element of NAT

for n being non zero Element of NAT

for g being PartFunc of REAL,(REAL-NS n) st 1 <= i & i <= n & g is_differentiable_on X holds

( (Proj (i,n)) * g is_differentiable_on X & (Proj (i,n)) * (g `| X) = ((Proj (i,n)) * g) `| X )

for i being Element of NAT

for n being non zero Element of NAT

for g being PartFunc of REAL,(REAL-NS n) st 1 <= i & i <= n & g is_differentiable_on X holds

( (Proj (i,n)) * g is_differentiable_on X & (Proj (i,n)) * (g `| X) = ((Proj (i,n)) * g) `| X )

proof end;

theorem Th29: :: NDIFF_4:29

for X being set

for i being Element of NAT

for n being non zero Element of NAT

for f being PartFunc of REAL,(REAL n) st 1 <= i & i <= n & f is_differentiable_on X holds

( (Proj (i,n)) * f is_differentiable_on X & (Proj (i,n)) * (f `| X) = ((Proj (i,n)) * f) `| X )

for i being Element of NAT

for n being non zero Element of NAT

for f being PartFunc of REAL,(REAL n) st 1 <= i & i <= n & f is_differentiable_on X holds

( (Proj (i,n)) * f is_differentiable_on X & (Proj (i,n)) * (f `| X) = ((Proj (i,n)) * f) `| X )

proof end;

theorem Th30: :: NDIFF_4:30

for X being set

for n being non zero Element of NAT

for g being PartFunc of REAL,(REAL-NS n) holds

( g is_differentiable_on X iff for i being Element of NAT st 1 <= i & i <= n holds

(Proj (i,n)) * g is_differentiable_on X )

for n being non zero Element of NAT

for g being PartFunc of REAL,(REAL-NS n) holds

( g is_differentiable_on X iff for i being Element of NAT st 1 <= i & i <= n holds

(Proj (i,n)) * g is_differentiable_on X )

proof end;

theorem :: NDIFF_4:31

for X being set

for n being non zero Element of NAT

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

( f is_differentiable_on X iff for i being Element of NAT st 1 <= i & i <= n holds

(Proj (i,n)) * f is_differentiable_on X )

for n being non zero Element of NAT

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

( f is_differentiable_on X iff for i being Element of NAT st 1 <= i & i <= n holds

(Proj (i,n)) * f is_differentiable_on X )

proof end;

theorem Th32: :: NDIFF_4:32

for J being Function of (REAL-NS 1),REAL

for x0 being Point of (REAL-NS 1) st J = proj (1,1) holds

J is_continuous_in x0

for x0 being Point of (REAL-NS 1) st J = proj (1,1) holds

J is_continuous_in x0

proof end;

theorem Th33: :: NDIFF_4:33

for x0 being Real

for I being Function of REAL,(REAL-NS 1) st I = (proj (1,1)) " holds

I is_continuous_in x0

for I being Function of REAL,(REAL-NS 1) st I = (proj (1,1)) " holds

I is_continuous_in x0

proof end;

theorem Th34: :: NDIFF_4:34

for S, T being RealNormSpace

for f1 being PartFunc of S,REAL

for f2 being PartFunc of REAL,T

for x0 being Point of S st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds

f2 * f1 is_continuous_in x0

for f1 being PartFunc of S,REAL

for f2 being PartFunc of REAL,T

for x0 being Point of S st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds

f2 * f1 is_continuous_in x0

proof end;

Lm2: ( dom (proj (1,1)) = REAL 1 & rng (proj (1,1)) = REAL & ( for x being Element of REAL holds

( (proj (1,1)) . <*x*> = x & ((proj (1,1)) ") . x = <*x*> ) ) )

proof end;

theorem :: NDIFF_4:35

for n being non zero Element of NAT

for J being Function of (REAL-NS 1),REAL

for x0 being Point of (REAL-NS 1)

for y0 being Element of REAL

for g being PartFunc of REAL,(REAL-NS n)

for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds

( f is_continuous_in x0 iff g is_continuous_in y0 )

for J being Function of (REAL-NS 1),REAL

for x0 being Point of (REAL-NS 1)

for y0 being Element of REAL

for g being PartFunc of REAL,(REAL-NS n)

for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds

( f is_continuous_in x0 iff g is_continuous_in y0 )

proof end;

theorem :: NDIFF_4:36

for n being non zero Element of NAT

for I being Function of REAL,(REAL-NS 1)

for x0 being Point of (REAL-NS 1)

for y0 being Element of REAL

for g being PartFunc of REAL,(REAL-NS n)

for f being PartFunc of (REAL-NS 1),(REAL-NS n) st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds

( f is_continuous_in x0 iff g is_continuous_in y0 )

for I being Function of REAL,(REAL-NS 1)

for x0 being Point of (REAL-NS 1)

for y0 being Element of REAL

for g being PartFunc of REAL,(REAL-NS n)

for f being PartFunc of (REAL-NS 1),(REAL-NS n) st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds

( f is_continuous_in x0 iff g is_continuous_in y0 )

proof end;

theorem :: NDIFF_4:37

for x0 being Real

for I being Function of REAL,(REAL-NS 1) st I = (proj (1,1)) " holds

( I is_differentiable_in x0 & diff (I,x0) = <*1*> )

for I being Function of REAL,(REAL-NS 1) st I = (proj (1,1)) " holds

( I is_differentiable_in x0 & diff (I,x0) = <*1*> )

proof end;

definition

let n be non zero Element of NAT ;

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

let x be Point of (REAL-NS n);

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

let x be Point of (REAL-NS n);

pred f is_differentiable_in x means :: NDIFF_4:def 6

ex g being PartFunc of (REAL n),REAL ex y being Element of REAL n st

( f = g & x = y & g is_differentiable_in y );

ex g being PartFunc of (REAL n),REAL ex y being Element of REAL n st

( f = g & x = y & g is_differentiable_in y );

:: deftheorem defines is_differentiable_in NDIFF_4:def 6 :

for n being non zero Element of NAT

for f being PartFunc of (REAL-NS n),REAL

for x being Point of (REAL-NS n) holds

( f is_differentiable_in x iff ex g being PartFunc of (REAL n),REAL ex y being Element of REAL n st

( f = g & x = y & g is_differentiable_in y ) );

for n being non zero Element of NAT

for f being PartFunc of (REAL-NS n),REAL

for x being Point of (REAL-NS n) holds

( f is_differentiable_in x iff ex g being PartFunc of (REAL n),REAL ex y being Element of REAL n st

( f = g & x = y & g is_differentiable_in y ) );

definition

let n be non zero Element of NAT ;

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

let x be Point of (REAL-NS n);

ex b_{1} being Function of (REAL-NS n),REAL ex g being PartFunc of (REAL n),REAL ex y being Element of REAL n st

( f = g & x = y & b_{1} = diff (g,y) )

for b_{1}, b_{2} being Function of (REAL-NS n),REAL st ex g being PartFunc of (REAL n),REAL ex y being Element of REAL n st

( f = g & x = y & b_{1} = diff (g,y) ) & ex g being PartFunc of (REAL n),REAL ex y being Element of REAL n st

( f = g & x = y & b_{2} = diff (g,y) ) holds

b_{1} = b_{2}
;

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

let x be Point of (REAL-NS n);

func diff (f,x) -> Function of (REAL-NS n),REAL means :Def7: :: NDIFF_4:def 7

ex g being PartFunc of (REAL n),REAL ex y being Element of REAL n st

( f = g & x = y & it = diff (g,y) );

existence ex g being PartFunc of (REAL n),REAL ex y being Element of REAL n st

( f = g & x = y & it = diff (g,y) );

ex b

( f = g & x = y & b

proof end;

uniqueness for b

( f = g & x = y & b

( f = g & x = y & b

b

:: deftheorem Def7 defines diff NDIFF_4:def 7 :

for n being non zero Element of NAT

for f being PartFunc of (REAL-NS n),REAL

for x being Point of (REAL-NS n)

for b_{4} being Function of (REAL-NS n),REAL holds

( b_{4} = diff (f,x) iff ex g being PartFunc of (REAL n),REAL ex y being Element of REAL n st

( f = g & x = y & b_{4} = diff (g,y) ) );

for n being non zero Element of NAT

for f being PartFunc of (REAL-NS n),REAL

for x being Point of (REAL-NS n)

for b

( b

( f = g & x = y & b

theorem Th38: :: NDIFF_4:38

for J being Function of (REAL 1),REAL

for x0 being Element of REAL 1 st J = proj (1,1) holds

( J is_differentiable_in x0 & diff (J,x0) = J )

for x0 being Element of REAL 1 st J = proj (1,1) holds

( J is_differentiable_in x0 & diff (J,x0) = J )

proof end;

theorem :: NDIFF_4:39

for J being Function of (REAL-NS 1),REAL

for x0 being Point of (REAL-NS 1) st J = proj (1,1) holds

( J is_differentiable_in x0 & diff (J,x0) = J )

for x0 being Point of (REAL-NS 1) st J = proj (1,1) holds

( J is_differentiable_in x0 & diff (J,x0) = J )

proof end;

theorem Th40: :: NDIFF_4:40

for n being non zero Element of NAT

for I being Function of REAL,(REAL-NS 1) st I = (proj (1,1)) " holds

( ( for R being RestFunc of (REAL-NS 1),(REAL-NS n) holds R * I is RestFunc of (REAL-NS n) ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS n) holds L * I is LinearFunc of (REAL-NS n) ) )

for I being Function of REAL,(REAL-NS 1) st I = (proj (1,1)) " holds

( ( for R being RestFunc of (REAL-NS 1),(REAL-NS n) holds R * I is RestFunc of (REAL-NS n) ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS n) holds L * I is LinearFunc of (REAL-NS n) ) )

proof end;

theorem Th41: :: NDIFF_4:41

for n being non zero Element of NAT

for J being Function of (REAL-NS 1),REAL st J = proj (1,1) holds

( ( for R being RestFunc of (REAL-NS n) holds R * J is RestFunc of (REAL-NS 1),(REAL-NS n) ) & ( for L being LinearFunc of (REAL-NS n) holds L * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS n) ) )

for J being Function of (REAL-NS 1),REAL st J = proj (1,1) holds

( ( for R being RestFunc of (REAL-NS n) holds R * J is RestFunc of (REAL-NS 1),(REAL-NS n) ) & ( for L being LinearFunc of (REAL-NS n) holds L * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS n) ) )

proof end;

theorem Th42: :: NDIFF_4:42

for n being non zero Element of NAT

for I being Function of REAL,(REAL-NS 1)

for x0 being Point of (REAL-NS 1)

for y0 being Element of REAL

for g being PartFunc of REAL,(REAL-NS n)

for f being PartFunc of (REAL-NS 1),(REAL-NS n) st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g & f is_differentiable_in x0 holds

( g is_differentiable_in y0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )

for I being Function of REAL,(REAL-NS 1)

for x0 being Point of (REAL-NS 1)

for y0 being Element of REAL

for g being PartFunc of REAL,(REAL-NS n)

for f being PartFunc of (REAL-NS 1),(REAL-NS n) st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g & f is_differentiable_in x0 holds

( g is_differentiable_in y0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )

proof end;

theorem Th43: :: NDIFF_4:43

for n being non zero Element of NAT

for I being Function of REAL,(REAL-NS 1)

for x0 being Point of (REAL-NS 1)

for y0 being Real

for g being PartFunc of REAL,(REAL-NS n)

for f being PartFunc of (REAL-NS 1),(REAL-NS n) st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds

( f is_differentiable_in x0 iff g is_differentiable_in y0 )

for I being Function of REAL,(REAL-NS 1)

for x0 being Point of (REAL-NS 1)

for y0 being Real

for g being PartFunc of REAL,(REAL-NS n)

for f being PartFunc of (REAL-NS 1),(REAL-NS n) st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds

( f is_differentiable_in x0 iff g is_differentiable_in y0 )

proof end;

theorem Th44: :: NDIFF_4:44

for n being non zero Element of NAT

for J being Function of (REAL-NS 1),REAL

for x0 being Point of (REAL-NS 1)

for y0 being Element of REAL

for g being PartFunc of REAL,(REAL-NS n)

for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds

( f is_differentiable_in x0 iff g is_differentiable_in y0 )

for J being Function of (REAL-NS 1),REAL

for x0 being Point of (REAL-NS 1)

for y0 being Element of REAL

for g being PartFunc of REAL,(REAL-NS n)

for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds

( f is_differentiable_in x0 iff g is_differentiable_in y0 )

proof end;

theorem :: NDIFF_4:45

for n being non zero Element of NAT

for J being Function of (REAL-NS 1),REAL

for x0 being Point of (REAL-NS 1)

for y0 being Element of REAL

for g being PartFunc of REAL,(REAL-NS n)

for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J & g is_differentiable_in y0 holds

( f is_differentiable_in x0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )

for J being Function of (REAL-NS 1),REAL

for x0 being Point of (REAL-NS 1)

for y0 being Element of REAL

for g being PartFunc of REAL,(REAL-NS n)

for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J & g is_differentiable_in y0 holds

( f is_differentiable_in x0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )

proof end;

theorem Th46: :: NDIFF_4:46

for n being non zero Element of NAT

for R being RestFunc of (REAL-NS n) st R /. 0 = 0. (REAL-NS n) holds

for e being Real st e > 0 holds

ex d being Real st

( d > 0 & ( for h being Real st |.h.| < d holds

||.(R /. h).|| <= e * |.h.| ) )

for R being RestFunc of (REAL-NS n) st R /. 0 = 0. (REAL-NS n) holds

for e being Real st e > 0 holds

ex d being Real st

( d > 0 & ( for h being Real st |.h.| < d holds

||.(R /. h).|| <= e * |.h.| ) )

proof end;

theorem Th47: :: NDIFF_4:47

for n, m being non zero Element of NAT

for R being RestFunc of (REAL-NS n)

for L being Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m) holds L * R is RestFunc of (REAL-NS m)

for R being RestFunc of (REAL-NS n)

for L being Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m) holds L * R is RestFunc of (REAL-NS m)

proof end;

theorem Th48: :: NDIFF_4:48

for n, m being non zero Element of NAT

for R1 being RestFunc of (REAL-NS n) st R1 /. 0 = 0. (REAL-NS n) holds

for R2 being RestFunc of (REAL-NS n),(REAL-NS m) st R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) holds

for L being LinearFunc of (REAL-NS n) holds R2 * (L + R1) is RestFunc of (REAL-NS m)

for R1 being RestFunc of (REAL-NS n) st R1 /. 0 = 0. (REAL-NS n) holds

for R2 being RestFunc of (REAL-NS n),(REAL-NS m) st R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) holds

for L being LinearFunc of (REAL-NS n) holds R2 * (L + R1) is RestFunc of (REAL-NS m)

proof end;

theorem Th49: :: NDIFF_4:49

for n, m being non zero Element of NAT

for R1 being RestFunc of (REAL-NS n) st R1 /. 0 = 0. (REAL-NS n) holds

for R2 being RestFunc of (REAL-NS n),(REAL-NS m) st R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) holds

for L1 being LinearFunc of (REAL-NS n)

for L2 being Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m) holds (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of (REAL-NS m)

for R1 being RestFunc of (REAL-NS n) st R1 /. 0 = 0. (REAL-NS n) holds

for R2 being RestFunc of (REAL-NS n),(REAL-NS m) st R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) holds

for L1 being LinearFunc of (REAL-NS n)

for L2 being Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m) holds (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of (REAL-NS m)

proof end;

theorem :: NDIFF_4:50

for n, m being non zero Element of NAT

for x0 being Element of REAL

for g being PartFunc of REAL,(REAL-NS n) st g is_differentiable_in x0 holds

for f being PartFunc of (REAL-NS n),(REAL-NS m) st f is_differentiable_in g /. x0 holds

( f * g is_differentiable_in x0 & diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) )

for x0 being Element of REAL

for g being PartFunc of REAL,(REAL-NS n) st g is_differentiable_in x0 holds

for f being PartFunc of (REAL-NS n),(REAL-NS m) st f is_differentiable_in g /. x0 holds

( f * g is_differentiable_in x0 & diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) )

proof end;