:: by Hiroshi Imura , Morishige Kimura and Yasunari Shidama

::

:: Received May 24, 2004

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

theorem Th1: :: NDIFF_1:1

for S being RealNormSpace

for x0 being Point of S

for N1, N2 being Neighbourhood of x0 ex N being Neighbourhood of x0 st

( N c= N1 & N c= N2 )

for x0 being Point of S

for N1, N2 being Neighbourhood of x0 ex N being Neighbourhood of x0 st

( N c= N1 & N c= N2 )

proof end;

theorem Th2: :: NDIFF_1:2

for S being RealNormSpace

for X being Subset of S st X is open holds

for r being Point of S st r in X holds

ex N being Neighbourhood of r st N c= X

for X being Subset of S st X is open holds

for r being Point of S st r in X holds

ex N being Neighbourhood of r st N c= X

proof end;

theorem :: NDIFF_1:3

for S being RealNormSpace

for X being Subset of S st X is open holds

for r being Point of S st r in X holds

ex g being Real st

( 0 < g & { y where y is Point of S : ||.(y - r).|| < g } c= X )

for X being Subset of S st X is open holds

for r being Point of S st r in X holds

ex g being Real st

( 0 < g & { y where y is Point of S : ||.(y - r).|| < g } c= X )

proof end;

theorem Th4: :: NDIFF_1:4

for S being RealNormSpace

for X being Subset of S st ( for r being Point of S st r in X holds

ex N being Neighbourhood of r st N c= X ) holds

X is open

for X being Subset of S st ( for r being Point of S st r in X holds

ex N being Neighbourhood of r st N c= X ) holds

X is open

proof end;

theorem :: NDIFF_1:5

for S being RealNormSpace

for X being Subset of S holds

( ( for r being Point of S st r in X holds

ex N being Neighbourhood of r st N c= X ) iff X is open ) by Th2, Th4;

for X being Subset of S holds

( ( for r being Point of S st r in X holds

ex N being Neighbourhood of r st N c= X ) iff X is open ) by Th2, Th4;

:: Normed Linear Spaces versions of SEQ_1: -

definition

let X be set ;

let S be ZeroStr ;

let f be Function of X,S;

compatibility

( f is non-zero iff rng f c= NonZero S )

end;
let S be ZeroStr ;

let f be Function of X,S;

compatibility

( f is non-zero iff rng f c= NonZero S )

proof end;

:: deftheorem defines non-zero NDIFF_1:def 1 :

for X being set

for S being ZeroStr

for f being Function of X,S holds

( f is non-zero iff rng f c= NonZero S );

for X being set

for S being ZeroStr

for f being Function of X,S holds

( f is non-zero iff rng f c= NonZero S );

theorem Th6: :: NDIFF_1:6

for S being RealNormSpace

for seq being sequence of S holds

( seq is non-zero iff for x being set st x in NAT holds

seq . x <> 0. S )

for seq being sequence of S holds

( seq is non-zero iff for x being set st x in NAT holds

seq . x <> 0. S )

proof end;

theorem Th7: :: NDIFF_1:7

for S being RealNormSpace

for seq being sequence of S holds

( seq is non-zero iff for n being Nat holds seq . n <> 0. S )

for seq being sequence of S holds

( seq is non-zero iff for n being Nat holds seq . n <> 0. S )

proof end;

definition

let RNS be RealLinearSpace;

let S be sequence of RNS;

let a be Real_Sequence;

ex b_{1} being sequence of RNS st

for n being Nat holds b_{1} . n = (a . n) * (S . n)

for b_{1}, b_{2} being sequence of RNS st ( for n being Nat holds b_{1} . n = (a . n) * (S . n) ) & ( for n being Nat holds b_{2} . n = (a . n) * (S . n) ) holds

b_{1} = b_{2}

end;
let S be sequence of RNS;

let a be Real_Sequence;

func a (#) S -> sequence of RNS means :Def2: :: NDIFF_1:def 2

for n being Nat holds it . n = (a . n) * (S . n);

existence for n being Nat holds it . n = (a . n) * (S . n);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines (#) NDIFF_1:def 2 :

for RNS being RealLinearSpace

for S being sequence of RNS

for a being Real_Sequence

for b_{4} being sequence of RNS holds

( b_{4} = a (#) S iff for n being Nat holds b_{4} . n = (a . n) * (S . n) );

for RNS being RealLinearSpace

for S being sequence of RNS

for a being Real_Sequence

for b

( b

definition

let RNS be RealLinearSpace;

let z be Point of RNS;

let a be Real_Sequence;

ex b_{1} being sequence of RNS st

for n being Nat holds b_{1} . n = (a . n) * z

for b_{1}, b_{2} being sequence of RNS st ( for n being Nat holds b_{1} . n = (a . n) * z ) & ( for n being Nat holds b_{2} . n = (a . n) * z ) holds

b_{1} = b_{2}

end;
let z be Point of RNS;

let a be Real_Sequence;

func a * z -> sequence of RNS means :Def3: :: NDIFF_1:def 3

for n being Nat holds it . n = (a . n) * z;

existence for n being Nat holds it . n = (a . n) * z;

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines * NDIFF_1:def 3 :

for RNS being RealLinearSpace

for z being Point of RNS

for a being Real_Sequence

for b_{4} being sequence of RNS holds

( b_{4} = a * z iff for n being Nat holds b_{4} . n = (a . n) * z );

for RNS being RealLinearSpace

for z being Point of RNS

for a being Real_Sequence

for b

( b

theorem :: NDIFF_1:8

for S being RealNormSpace

for seq being sequence of S

for rseq1, rseq2 being Real_Sequence holds (rseq1 + rseq2) (#) seq = (rseq1 (#) seq) + (rseq2 (#) seq)

for seq being sequence of S

for rseq1, rseq2 being Real_Sequence holds (rseq1 + rseq2) (#) seq = (rseq1 (#) seq) + (rseq2 (#) seq)

proof end;

theorem Th9: :: NDIFF_1:9

for S being RealNormSpace

for rseq being Real_Sequence

for seq1, seq2 being sequence of S holds rseq (#) (seq1 + seq2) = (rseq (#) seq1) + (rseq (#) seq2)

for rseq being Real_Sequence

for seq1, seq2 being sequence of S holds rseq (#) (seq1 + seq2) = (rseq (#) seq1) + (rseq (#) seq2)

proof end;

theorem Th10: :: NDIFF_1:10

for r being Real

for S being RealNormSpace

for seq being sequence of S

for rseq being Real_Sequence holds r * (rseq (#) seq) = rseq (#) (r * seq)

for S being RealNormSpace

for seq being sequence of S

for rseq being Real_Sequence holds r * (rseq (#) seq) = rseq (#) (r * seq)

proof end;

theorem :: NDIFF_1:11

for S being RealNormSpace

for seq being sequence of S

for rseq1, rseq2 being Real_Sequence holds (rseq1 - rseq2) (#) seq = (rseq1 (#) seq) - (rseq2 (#) seq)

for seq being sequence of S

for rseq1, rseq2 being Real_Sequence holds (rseq1 - rseq2) (#) seq = (rseq1 (#) seq) - (rseq2 (#) seq)

proof end;

theorem Th12: :: NDIFF_1:12

for S being RealNormSpace

for rseq being Real_Sequence

for seq1, seq2 being sequence of S holds rseq (#) (seq1 - seq2) = (rseq (#) seq1) - (rseq (#) seq2)

for rseq being Real_Sequence

for seq1, seq2 being sequence of S holds rseq (#) (seq1 - seq2) = (rseq (#) seq1) - (rseq (#) seq2)

proof end;

theorem Th13: :: NDIFF_1:13

for S being RealNormSpace

for rseq being Real_Sequence

for seq being sequence of S st rseq is convergent & seq is convergent holds

rseq (#) seq is convergent

for rseq being Real_Sequence

for seq being sequence of S st rseq is convergent & seq is convergent holds

rseq (#) seq is convergent

proof end;

theorem Th14: :: NDIFF_1:14

for S being RealNormSpace

for rseq being Real_Sequence

for seq being sequence of S st rseq is convergent & seq is convergent holds

lim (rseq (#) seq) = (lim rseq) * (lim seq)

for rseq being Real_Sequence

for seq being sequence of S st rseq is convergent & seq is convergent holds

lim (rseq (#) seq) = (lim rseq) * (lim seq)

proof end;

theorem Th15: :: NDIFF_1:15

for S being RealNormSpace

for seq, seq1 being sequence of S

for k being Nat holds (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k)

for seq, seq1 being sequence of S

for k being Nat holds (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k)

proof end;

theorem Th16: :: NDIFF_1:16

for k being Element of NAT

for S being RealNormSpace

for seq, seq1 being sequence of S holds (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k)

for S being RealNormSpace

for seq, seq1 being sequence of S holds (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k)

proof end;

theorem Th17: :: NDIFF_1:17

for k being Element of NAT

for S being RealNormSpace

for seq being sequence of S st seq is non-zero holds

seq ^\ k is non-zero

for S being RealNormSpace

for seq being sequence of S st seq is non-zero holds

seq ^\ k is non-zero

proof end;

:: deftheorem Def4 defines -convergent NDIFF_1:def 4 :

for S being RealNormSpace

for x being Point of S

for IT being sequence of S holds

( IT is x -convergent iff ( IT is convergent & lim IT = x ) );

for S being RealNormSpace

for x being Point of S

for IT being sequence of S holds

( IT is x -convergent iff ( IT is convergent & lim IT = x ) );

theorem Th18: :: NDIFF_1:18

for X being RealNormSpace

for seq being sequence of X st seq is constant holds

( seq is convergent & ( for k being Element of NAT holds lim seq = seq . k ) )

for seq being sequence of X st seq is constant holds

( seq is convergent & ( for k being Element of NAT holds lim seq = seq . k ) )

proof end;

theorem Th19: :: NDIFF_1:19

for S being RealNormSpace

for seq being sequence of S

for x0 being Point of S

for r being Real st 0 < r & ( for n being Nat holds seq . n = (1 / (n + r)) * x0 ) holds

seq is convergent

for seq being sequence of S

for x0 being Point of S

for r being Real st 0 < r & ( for n being Nat holds seq . n = (1 / (n + r)) * x0 ) holds

seq is convergent

proof end;

theorem Th20: :: NDIFF_1:20

for S being RealNormSpace

for seq being sequence of S

for x0 being Point of S

for r being Real st 0 < r & ( for n being Nat holds seq . n = (1 / (n + r)) * x0 ) holds

lim seq = 0. S

for seq being sequence of S

for x0 being Point of S

for r being Real st 0 < r & ( for n being Nat holds seq . n = (1 / (n + r)) * x0 ) holds

lim seq = 0. S

proof end;

registration

let S be non trivial RealNormSpace;

ex b_{1} being sequence of S st

( b_{1} is non-zero & b_{1} is 0. S -convergent )

end;
cluster V1() V4( NAT ) V5( the carrier of S) V6() Function-like total quasi_total non-zero 0. S -convergent for Element of K16(K17(NAT, the carrier of S));

existence ex b

( b

proof end;

registration

let S be RealNormSpace;

ex b_{1} being sequence of S st b_{1} is 0. S -convergent

end;
cluster V1() V4( NAT ) V5( the carrier of S) V6() Function-like total quasi_total 0. S -convergent for Element of K16(K17(NAT, the carrier of S));

existence ex b

proof end;

theorem :: NDIFF_1:21

for S being RealNormSpace

for a being non-zero 0 -convergent Real_Sequence

for z being Point of S st z <> 0. S holds

( a * z is non-zero & a * z is 0. S -convergent )

for a being non-zero 0 -convergent Real_Sequence

for z being Point of S st z <> 0. S holds

( a * z is non-zero & a * z is 0. S -convergent )

proof end;

theorem :: NDIFF_1:22

for S being RealNormSpace

for Y being Subset of S holds

( ( for r being Point of S holds

( r in Y iff r in the carrier of S ) ) iff Y = the carrier of S )

for Y being Subset of S holds

( ( for r being Point of S holds

( r in Y iff r in the carrier of S ) ) iff Y = the carrier of S )

proof end;

registration

let S be RealNormSpace;

ex b_{1} being sequence of S st b_{1} is constant

end;
cluster V1() V4( NAT ) V5( the carrier of S) V6() Function-like constant total quasi_total for Element of K16(K17(NAT, the carrier of S));

existence ex b

proof end;

:: deftheorem Def5 defines RestFunc-like NDIFF_1:def 5 :

for S, T being RealNormSpace

for IT being PartFunc of S,T holds

( IT is RestFunc-like iff ( IT is total & ( for h being 0. b_{1} -convergent sequence of S st h is non-zero holds

( (||.h.|| ") (#) (IT /* h) is convergent & lim ((||.h.|| ") (#) (IT /* h)) = 0. T ) ) ) );

for S, T being RealNormSpace

for IT being PartFunc of S,T holds

( IT is RestFunc-like iff ( IT is total & ( for h being 0. b

( (||.h.|| ") (#) (IT /* h) is convergent & lim ((||.h.|| ") (#) (IT /* h)) = 0. T ) ) ) );

registration

let S, T be RealNormSpace;

ex b_{1} being PartFunc of S,T st b_{1} is RestFunc-like

end;
cluster V1() V4( the carrier of S) V5( the carrier of T) Function-like RestFunc-like for Element of K16(K17( the carrier of S, the carrier of T));

existence ex b

proof end;

theorem :: NDIFF_1:23

for S, T being RealNormSpace

for R being PartFunc of S,T 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 Point of S st z <> 0. S & ||.z.|| < d holds

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

for R being PartFunc of S,T 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 Point of S st z <> 0. S & ||.z.|| < d holds

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

proof end;

theorem Th24: :: NDIFF_1:24

for S, T being RealNormSpace

for R being RestFunc of S,T

for s being 0. b_{1} -convergent sequence of S st s is non-zero holds

( R /* s is convergent & lim (R /* s) = 0. T )

for R being RestFunc of S,T

for s being 0. b

( R /* s is convergent & lim (R /* s) = 0. T )

proof end;

theorem Th25: :: NDIFF_1:25

for S, T being RealNormSpace

for h1, h2 being PartFunc of S,T

for seq being sequence of S st h1 is total & h2 is total holds

( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )

for h1, h2 being PartFunc of S,T

for seq being sequence of S st h1 is total & h2 is total holds

( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )

proof end;

theorem Th26: :: NDIFF_1:26

for S, T being RealNormSpace

for h being PartFunc of S,T

for seq being sequence of S

for r being Real st h is total holds

(r (#) h) /* seq = r * (h /* seq)

for h being PartFunc of S,T

for seq being sequence of S

for r being Real st h is total holds

(r (#) h) /* seq = r * (h /* seq)

proof end;

theorem Th27: :: NDIFF_1:27

for S, T being RealNormSpace

for f being PartFunc of S,T

for x0 being Point of S holds

( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Nat holds s1 . n <> x0 ) holds

( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) )

for f being PartFunc of S,T

for x0 being Point of S holds

( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Nat holds s1 . n <> x0 ) holds

( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) )

proof end;

theorem Th28: :: NDIFF_1:28

for S, T being RealNormSpace

for R1, R2 being RestFunc of S,T holds

( R1 + R2 is RestFunc of S,T & R1 - R2 is RestFunc of S,T )

for R1, R2 being RestFunc of S,T holds

( R1 + R2 is RestFunc of S,T & R1 - R2 is RestFunc of S,T )

proof end;

theorem Th29: :: NDIFF_1:29

for S, T being RealNormSpace

for r being Real

for R being RestFunc of S,T holds r (#) R is RestFunc of S,T

for r being Real

for R being RestFunc of S,T holds r (#) R is RestFunc of S,T

proof end;

definition

let S, T be RealNormSpace;

let f be PartFunc of S,T;

let x0 be Point of S;

end;
let f be PartFunc of S,T;

let x0 be Point of S;

pred f is_differentiable_in x0 means :: NDIFF_1:def 6

ex N being Neighbourhood of x0 st

( N c= dom f & ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st

for x being Point of S st x in N holds

(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) );

ex N being Neighbourhood of x0 st

( N c= dom f & ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st

for x being Point of S st x in N holds

(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) );

:: deftheorem defines is_differentiable_in NDIFF_1:def 6 :

for S, T being RealNormSpace

for f being PartFunc of S,T

for x0 being Point of S holds

( f is_differentiable_in x0 iff ex N being Neighbourhood of x0 st

( N c= dom f & ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st

for x being Point of S st x in N holds

(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) );

for S, T being RealNormSpace

for f being PartFunc of S,T

for x0 being Point of S holds

( f is_differentiable_in x0 iff ex N being Neighbourhood of x0 st

( N c= dom f & ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st

for x being Point of S st x in N holds

(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) );

definition

let S, T be RealNormSpace;

let f be PartFunc of S,T;

let x0 be Point of S;

assume A1: f is_differentiable_in x0 ;

ex b_{1} being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex N being Neighbourhood of x0 st

( N c= dom f & ex R being RestFunc of S,T st

for x being Point of S st x in N holds

(f /. x) - (f /. x0) = (b_{1} . (x - x0)) + (R /. (x - x0)) )
by A1;

uniqueness

for b_{1}, b_{2} being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) st ex N being Neighbourhood of x0 st

( N c= dom f & ex R being RestFunc of S,T st

for x being Point of S st x in N holds

(f /. x) - (f /. x0) = (b_{1} . (x - x0)) + (R /. (x - x0)) ) & ex N being Neighbourhood of x0 st

( N c= dom f & ex R being RestFunc of S,T st

for x being Point of S st x in N holds

(f /. x) - (f /. x0) = (b_{2} . (x - x0)) + (R /. (x - x0)) ) holds

b_{1} = b_{2}

end;
let f be PartFunc of S,T;

let x0 be Point of S;

assume A1: f is_differentiable_in x0 ;

func diff (f,x0) -> Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) means :Def7: :: NDIFF_1:def 7

ex N being Neighbourhood of x0 st

( N c= dom f & ex R being RestFunc of S,T st

for x being Point of S st x in N holds

(f /. x) - (f /. x0) = (it . (x - x0)) + (R /. (x - x0)) );

existence ex N being Neighbourhood of x0 st

( N c= dom f & ex R being RestFunc of S,T st

for x being Point of S st x in N holds

(f /. x) - (f /. x0) = (it . (x - x0)) + (R /. (x - x0)) );

ex b

( N c= dom f & ex R being RestFunc of S,T st

for x being Point of S st x in N holds

(f /. x) - (f /. x0) = (b

uniqueness

for b

( N c= dom f & ex R being RestFunc of S,T st

for x being Point of S st x in N holds

(f /. x) - (f /. x0) = (b

( N c= dom f & ex R being RestFunc of S,T st

for x being Point of S st x in N holds

(f /. x) - (f /. x0) = (b

b

proof end;

:: deftheorem Def7 defines diff NDIFF_1:def 7 :

for S, T being RealNormSpace

for f being PartFunc of S,T

for x0 being Point of S st f is_differentiable_in x0 holds

for b_{5} being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) holds

( b_{5} = diff (f,x0) iff ex N being Neighbourhood of x0 st

( N c= dom f & ex R being RestFunc of S,T st

for x being Point of S st x in N holds

(f /. x) - (f /. x0) = (b_{5} . (x - x0)) + (R /. (x - x0)) ) );

for S, T being RealNormSpace

for f being PartFunc of S,T

for x0 being Point of S st f is_differentiable_in x0 holds

for b

( b

( N c= dom f & ex R being RestFunc of S,T st

for x being Point of S st x in N holds

(f /. x) - (f /. x0) = (b

definition

let X be set ;

let S, T be RealNormSpace;

let f be PartFunc of S,T;

end;
let S, T be RealNormSpace;

let f be PartFunc of S,T;

pred f is_differentiable_on X means :: NDIFF_1:def 8

( X c= dom f & ( for x being Point of S st x in X holds

f | X is_differentiable_in x ) );

( X c= dom f & ( for x being Point of S st x in X holds

f | X is_differentiable_in x ) );

:: deftheorem defines is_differentiable_on NDIFF_1:def 8 :

for X being set

for S, T being RealNormSpace

for f being PartFunc of S,T holds

( f is_differentiable_on X iff ( X c= dom f & ( for x being Point of S st x in X holds

f | X is_differentiable_in x ) ) );

for X being set

for S, T being RealNormSpace

for f being PartFunc of S,T holds

( f is_differentiable_on X iff ( X c= dom f & ( for x being Point of S st x in X holds

f | X is_differentiable_in x ) ) );

theorem Th30: :: NDIFF_1:30

for X being set

for S, T being RealNormSpace

for f being PartFunc of S,T st f is_differentiable_on X holds

X is Subset of S by XBOOLE_1:1;

for S, T being RealNormSpace

for f being PartFunc of S,T st f is_differentiable_on X holds

X is Subset of S by XBOOLE_1:1;

theorem Th31: :: NDIFF_1:31

for S, T being RealNormSpace

for f being PartFunc of S,T

for Z being Subset of S st Z is open holds

( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Point of S st x in Z holds

f is_differentiable_in x ) ) )

for f being PartFunc of S,T

for Z being Subset of S st Z is open holds

( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Point of S st x in Z holds

f is_differentiable_in x ) ) )

proof end;

theorem :: NDIFF_1:32

for S, T being RealNormSpace

for f being PartFunc of S,T

for Y being Subset of S st f is_differentiable_on Y holds

Y is open

for f being PartFunc of S,T

for Y being Subset of S st f is_differentiable_on Y holds

Y is open

proof end;

definition

let S, T be RealNormSpace;

let f be PartFunc of S,T;

let X be set ;

assume A1: f is_differentiable_on X ;

ex b_{1} being PartFunc of S,(R_NormSpace_of_BoundedLinearOperators (S,T)) st

( dom b_{1} = X & ( for x being Point of S st x in X holds

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

for b_{1}, b_{2} being PartFunc of S,(R_NormSpace_of_BoundedLinearOperators (S,T)) st dom b_{1} = X & ( for x being Point of S st x in X holds

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

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

b_{1} = b_{2}

end;
let f be PartFunc of S,T;

let X be set ;

assume A1: f is_differentiable_on X ;

func f `| X -> PartFunc of S,(R_NormSpace_of_BoundedLinearOperators (S,T)) means :Def9: :: NDIFF_1:def 9

( dom it = X & ( for x being Point of S st x in X holds

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

existence ( dom it = X & ( for x being Point of S 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 Def9 defines `| NDIFF_1:def 9 :

for S, T being RealNormSpace

for f being PartFunc of S,T

for X being set st f is_differentiable_on X holds

for b_{5} being PartFunc of S,(R_NormSpace_of_BoundedLinearOperators (S,T)) holds

( b_{5} = f `| X iff ( dom b_{5} = X & ( for x being Point of S st x in X holds

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

for S, T being RealNormSpace

for f being PartFunc of S,T

for X being set st f is_differentiable_on X holds

for b

( b

b

theorem :: NDIFF_1:33

for S, T being RealNormSpace

for f being PartFunc of S,T

for Z being Subset of S st Z is open & Z c= dom f & ex r being Point of T st rng f = {r} holds

( f is_differentiable_on Z & ( for x being Point of S st x in Z holds

(f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) )

for f being PartFunc of S,T

for Z being Subset of S st Z is open & Z c= dom f & ex r being Point of T st rng f = {r} holds

( f is_differentiable_on Z & ( for x being Point of S st x in Z holds

(f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) )

proof end;

registration

let S be RealNormSpace;

let h be 0. S -convergent sequence of S;

let n be Element of NAT ;

coherence

for b_{1} being sequence of S st b_{1} = h ^\ n holds

b_{1} is 0. S -convergent

end;
let h be 0. S -convergent sequence of S;

let n be Element of NAT ;

coherence

for b

b

proof end;

registration

let S be non trivial RealNormSpace;

let h be non-zero 0. S -convergent sequence of S;

let n be Element of NAT ;

coherence

for b_{1} being sequence of S st b_{1} = h ^\ n holds

( b_{1} is 0. S -convergent & b_{1} is non-zero )
by Th17;

end;
let h be non-zero 0. S -convergent sequence of S;

let n be Element of NAT ;

coherence

for b

( b

theorem Th34: :: NDIFF_1:34

for S, T being RealNormSpace

for f being PartFunc of S,T

for x0 being Point of S

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

for h being 0. b_{1} -convergent sequence of S st h is non-zero holds

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

( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T )

for f being PartFunc of S,T

for x0 being Point of S

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

for h being 0. b

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

( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T )

proof end;

theorem Th35: :: NDIFF_1:35

for S, T being RealNormSpace

for f1, f2 being PartFunc of S,T

for x0 being Point of S 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 f1, f2 being PartFunc of S,T

for x0 being Point of S 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 Th36: :: NDIFF_1:36

for S, T being RealNormSpace

for f1, f2 being PartFunc of S,T

for x0 being Point of S 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 f1, f2 being PartFunc of S,T

for x0 being Point of S 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 Th37: :: NDIFF_1:37

for S, T being RealNormSpace

for r being Real

for f being PartFunc of S,T

for x0 being Point of S st f is_differentiable_in x0 holds

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

for r being Real

for f being PartFunc of S,T

for x0 being Point of S st f is_differentiable_in x0 holds

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

proof end;

theorem :: NDIFF_1:38

for S being RealNormSpace

for f being PartFunc of S,S

for Z being Subset of S st Z is open & Z c= dom f & f | Z = id Z holds

( f is_differentiable_on Z & ( for x being Point of S st x in Z holds

(f `| Z) /. x = id the carrier of S ) )

for f being PartFunc of S,S

for Z being Subset of S st Z is open & Z c= dom f & f | Z = id Z holds

( f is_differentiable_on Z & ( for x being Point of S st x in Z holds

(f `| Z) /. x = id the carrier of S ) )

proof end;

theorem :: NDIFF_1:39

for S, T being RealNormSpace

for Z being Subset of S st Z is open holds

for f1, f2 being PartFunc of S,T 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 Point of S st x in Z holds

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

for Z being Subset of S st Z is open holds

for f1, f2 being PartFunc of S,T 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 Point of S st x in Z holds

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

proof end;

theorem :: NDIFF_1:40

for S, T being RealNormSpace

for Z being Subset of S st Z is open holds

for f1, f2 being PartFunc of S,T 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 Point of S st x in Z holds

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

for Z being Subset of S st Z is open holds

for f1, f2 being PartFunc of S,T 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 Point of S st x in Z holds

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

proof end;

theorem :: NDIFF_1:41

for S, T being RealNormSpace

for Z being Subset of S st Z is open holds

for r being Real

for f being PartFunc of S,T st Z c= dom (r (#) f) & f is_differentiable_on Z holds

( r (#) f is_differentiable_on Z & ( for x being Point of S st x in Z holds

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

for Z being Subset of S st Z is open holds

for r being Real

for f being PartFunc of S,T st Z c= dom (r (#) f) & f is_differentiable_on Z holds

( r (#) f is_differentiable_on Z & ( for x being Point of S st x in Z holds

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

proof end;

theorem :: NDIFF_1:42

for S, T being RealNormSpace

for f being PartFunc of S,T

for Z being Subset of S st Z is open & Z c= dom f & f | Z is constant holds

( f is_differentiable_on Z & ( for x being Point of S st x in Z holds

(f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) )

for f being PartFunc of S,T

for Z being Subset of S st Z is open & Z c= dom f & f | Z is constant holds

( f is_differentiable_on Z & ( for x being Point of S st x in Z holds

(f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) )

proof end;

theorem :: NDIFF_1:43

for S being RealNormSpace

for f being PartFunc of S,S

for r being Real

for p being Point of S

for Z being Subset of S st Z is open & Z c= dom f & ( for x being Point of S st x in Z holds

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

( f is_differentiable_on Z & ( for x being Point of S st x in Z holds

(f `| Z) /. x = r * (FuncUnit S) ) )

for f being PartFunc of S,S

for r being Real

for p being Point of S

for Z being Subset of S st Z is open & Z c= dom f & ( for x being Point of S st x in Z holds

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

( f is_differentiable_on Z & ( for x being Point of S st x in Z holds

(f `| Z) /. x = r * (FuncUnit S) ) )

proof end;

theorem Th44: :: NDIFF_1:44

for S, T being RealNormSpace

for f being PartFunc of S,T

for x0 being Point of S st f is_differentiable_in x0 holds

f is_continuous_in x0

for f being PartFunc of S,T

for x0 being Point of S st f is_differentiable_in x0 holds

f is_continuous_in x0

proof end;

theorem :: NDIFF_1:45

for X being set

for S, T being RealNormSpace

for f being PartFunc of S,T st f is_differentiable_on X holds

f is_continuous_on X by Th44;

for S, T being RealNormSpace

for f being PartFunc of S,T st f is_differentiable_on X holds

f is_continuous_on X by Th44;

theorem :: NDIFF_1:46

for X being set

for S, T being RealNormSpace

for f being PartFunc of S,T

for Z being Subset of S st Z is open & f is_differentiable_on X & Z c= X holds

f is_differentiable_on Z

for S, T being RealNormSpace

for f being PartFunc of S,T

for Z being Subset of S st Z is open & f is_differentiable_on X & Z c= X holds

f is_differentiable_on Z

proof end;

theorem :: NDIFF_1:47

for S, T being RealNormSpace

for f being PartFunc of S,T

for x0 being Point of S st f is_differentiable_in x0 holds

ex N being Neighbourhood of x0 st

( N c= dom f & ex R being RestFunc of S,T st

( R /. (0. S) = 0. T & R is_continuous_in 0. S & ( for x being Point of S st x in N holds

(f /. x) - (f /. x0) = ((diff (f,x0)) . (x - x0)) + (R /. (x - x0)) ) ) )

for f being PartFunc of S,T

for x0 being Point of S st f is_differentiable_in x0 holds

ex N being Neighbourhood of x0 st

( N c= dom f & ex R being RestFunc of S,T st

( R /. (0. S) = 0. T & R is_continuous_in 0. S & ( for x being Point of S st x in N holds

(f /. x) - (f /. x0) = ((diff (f,x0)) . (x - x0)) + (R /. (x - x0)) ) ) )

proof end;

definition

let S be non trivial RealNormSpace;

let T be RealNormSpace;

let IT be PartFunc of S,T;

compatibility

( IT is RestFunc-like iff ( IT is total & ( for h being non-zero 0. S -convergent sequence of S holds

( (||.h.|| ") (#) (IT /* h) is convergent & lim ((||.h.|| ") (#) (IT /* h)) = 0. T ) ) ) );

;

end;
let T be RealNormSpace;

let IT be PartFunc of S,T;

redefine attr IT is RestFunc-like means :: NDIFF_1:def 10

( IT is total & ( for h being non-zero 0. S -convergent sequence of S holds

( (||.h.|| ") (#) (IT /* h) is convergent & lim ((||.h.|| ") (#) (IT /* h)) = 0. T ) ) );

correctness ( IT is total & ( for h being non-zero 0. S -convergent sequence of S holds

( (||.h.|| ") (#) (IT /* h) is convergent & lim ((||.h.|| ") (#) (IT /* h)) = 0. T ) ) );

compatibility

( IT is RestFunc-like iff ( IT is total & ( for h being non-zero 0. S -convergent sequence of S holds

( (||.h.|| ") (#) (IT /* h) is convergent & lim ((||.h.|| ") (#) (IT /* h)) = 0. T ) ) ) );

;

:: deftheorem defines RestFunc-like NDIFF_1:def 10 :

for S being non trivial RealNormSpace

for T being RealNormSpace

for IT being PartFunc of S,T holds

( IT is RestFunc-like iff ( IT is total & ( for h being non-zero 0. b_{1} -convergent sequence of S holds

( (||.h.|| ") (#) (IT /* h) is convergent & lim ((||.h.|| ") (#) (IT /* h)) = 0. T ) ) ) );

for S being non trivial RealNormSpace

for T being RealNormSpace

for IT being PartFunc of S,T holds

( IT is RestFunc-like iff ( IT is total & ( for h being non-zero 0. b

( (||.h.|| ") (#) (IT /* h) is convergent & lim ((||.h.|| ") (#) (IT /* h)) = 0. T ) ) ) );

:: RCOMP_1:37 --> NFCONT_1:4