:: NDIFF_1 semantic presentation

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 )

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

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 )

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

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;

definition

let S be ZeroStr ;
let f be sequence of S;
attr f is being_not_0 means :Def1: :: NDIFF_1:def 1
rng f c= the carrier of S \ {(0. S)};

end;

:: deftheorem Def1 defines being_not_0 NDIFF_1:def 1 :

notation

let S be ZeroStr ;
let f be sequence of S;
synonym f is_not_0 for being_not_0 f;

end;

theorem Th6: :: NDIFF_1:6

for S being RealNormSpace
for seq being sequence of S holds
( seq is being_not_0 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 being_not_0 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;
func a (#) S -> sequence of RNS means :Def2: :: NDIFF_1:def 2
for n being Nat holds it . n = (a . n) * (S . n);
existence

proof end;

uniqueness

proof end;

end;

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

definition

let RNS be RealLinearSpace;
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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines * NDIFF_1:def 3 :

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)

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)

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)

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)

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)

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

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)

proof end;

theorem Th15: :: NDIFF_1:15

for k being Nat
for S being RealNormSpace
for seq, seq1 being sequence of S holds (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k)

proof end;

theorem Th16: :: NDIFF_1:16

for k being Nat
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 Nat
for S being RealNormSpace
for seq being sequence of S st seq is_not_0 holds
seq ^\ k is_not_0

proof end;

theorem Th18: :: NDIFF_1:18

for k being Nat
for S being RealNormSpace
for seq being sequence of S holds seq ^\ k is subsequence of seq

proof end;

theorem Th19: :: NDIFF_1:19

for S being RealNormSpace
for seq, seq1 being sequence of S st seq is constant & seq1 is subsequence of seq holds
seq1 is constant

proof end;

theorem Th20: :: NDIFF_1:20

for S being RealNormSpace
for seq, seq1 being sequence of S st seq is constant & seq1 is subsequence of seq holds
seq = seq1

proof end;

definition

let S be RealNormSpace;
let IT be sequence of S;
attr IT is convergent_to_0 means :Def4: :: NDIFF_1:def 4
( IT is_not_0 & IT is convergent & lim IT = 0. S );

end;

:: deftheorem Def4 defines convergent_to_0 NDIFF_1:def 4 :

theorem Th21: :: NDIFF_1:21

for X being RealNormSpace
for seq being sequence of X st seq is constant holds
( seq is convergent & ( for k being Nat holds lim seq = seq . k ) )

proof end;

theorem Th22: :: NDIFF_1:22

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

proof end;

theorem Th23: :: NDIFF_1:23

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

proof end;

theorem :: NDIFF_1:24

for S being RealNormSpace
for a being convergent_to_0 Real_Sequence
for z being Point of S st z <> 0. S holds
a * z is convergent_to_0

proof end;

theorem :: NDIFF_1:25

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 )

proof end;

registration

let S be non trivial RealNormSpace;
cluster convergent_to_0 Relation of NAT ,the carrier of S;
existence

proof end;

end;

registration

let S be non trivial RealNormSpace;
cluster V49 Relation of NAT ,the carrier of S;
existence

proof end;

end;

definition

let S, T be non trivial RealNormSpace;
let IT be PartFunc of S,T;
attr IT is REST-like means :Def5: :: NDIFF_1:def 5
( IT is total & ( for h being convergent_to_0 sequence of S holds
( (||.h.|| " ) (#) (IT * h) is convergent & lim ((||.h.|| " ) (#) (IT * h)) = 0. T ) ) );

end;

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

registration

let S, T be non trivial RealNormSpace;
cluster REST-like Relation of the carrier of S,the carrier of T;
existence

proof end;

end;

definition

let S, T be non trivial RealNormSpace;
mode REST of S,T is REST-like PartFunc of S,T;

end;

theorem :: NDIFF_1:26

for S, T being non trivial RealNormSpace
for R being PartFunc of S,T st R is total holds
( R is REST-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 Th27: :: NDIFF_1:27

for S, T being non trivial RealNormSpace
for R being REST of S,T
for s being convergent_to_0 sequence of S holds
( R * s is convergent & lim (R * s) = 0. T )

proof end;

theorem Th28: :: NDIFF_1:28

for n being Nat
for S being non trivial RealNormSpace
for seq being sequence of S holds rng (seq ^\ n) c= rng seq

proof end;

theorem Th29: :: NDIFF_1:29

for n being Nat
for S, T being non trivial RealNormSpace
for h being PartFunc of S,T
for seq being sequence of S st rng seq c= dom h holds
(h * seq) ^\ n = h * (seq ^\ n)

proof end;

theorem Th30: :: NDIFF_1:30

for S, T being non trivial 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) )

proof end;

theorem Th31: :: NDIFF_1:31

for S, T being non trivial 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)

proof end;

theorem Th32: :: NDIFF_1:32

for T, S being non trivial 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) ) ) ) )

proof end;

theorem Th33: :: NDIFF_1:33

for T, S being non trivial RealNormSpace
for R1, R2 being REST of S,T holds
( R1 + R2 is REST of S,T & R1 - R2 is REST of S,T )

proof end;

theorem Th34: :: NDIFF_1:34

for T, S being non trivial RealNormSpace
for r being Real
for R being REST of S,T holds r (#) R is REST of S,T

proof end;

definition

let S, T be non trivial RealNormSpace;
let f be PartFunc of S,T;
let x0 be Point of S;
pred f is_differentiable_in x0 means :Def6: :: 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 REST 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)) );

end;

:: deftheorem Def6 defines is_differentiable_in NDIFF_1:def 6 :

definition

let S, T be non trivial RealNormSpace;
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 REST 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines diff NDIFF_1:def 7 :

definition

let X be set ;
let S, T be non trivial RealNormSpace;
let f be PartFunc of S,T;
pred f is_differentiable_on X means :Def8: :: 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 ) );

end;

:: deftheorem Def8 defines is_differentiable_on NDIFF_1:def 8 :

theorem Th35: :: NDIFF_1:35

for X being set
for S, T being non trivial RealNormSpace
for f being PartFunc of S,T st f is_differentiable_on X holds
X is Subset of S

proof end;

theorem Th36: :: NDIFF_1:36

for S, T being non trivial 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 ) ) )

proof end;

theorem :: NDIFF_1:37

for S, T being non trivial RealNormSpace
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 non trivial RealNormSpace;
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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines `| NDIFF_1:def 9 :

theorem :: NDIFF_1:38

for S, T being non trivial 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) ) )

proof end;

registration

let S be non trivial RealNormSpace;
let h be convergent_to_0 sequence of S;
let n be Nat;
cluster h ^\ n -> convergent_to_0 ;
coherence

proof end;

end;

registration

let S be non trivial RealNormSpace;
let c be V49 sequence of S;
let n be Nat;
cluster c ^\ n -> V49 ;
coherence

proof end;

end;

theorem Th39: :: NDIFF_1:39

for S, T being non trivial 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 convergent_to_0 sequence of S
for c being V49 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 Th40: :: NDIFF_1:40

for T, S being non trivial 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) )

proof end;

theorem Th41: :: NDIFF_1:41

for T, S being non trivial 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) )

proof end;

theorem Th42: :: NDIFF_1:42

for T, S being non trivial 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) )

proof end;

theorem :: NDIFF_1:43

for S being non trivial 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 ) )

proof end;

theorem :: NDIFF_1:44

for S, T being non trivial 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) ) )

proof end;

theorem :: NDIFF_1:45

for S, T being non trivial 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) ) )

proof end;

theorem :: NDIFF_1:46

for S, T being non trivial 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) ) )

proof end;

theorem :: NDIFF_1:47

for S, T being non trivial RealNormSpace
for f being PartFunc of S,T
for Z being Subset of S st Z is open & Z c= dom f & f is_constant_on Z 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:48

for S being non trivial 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) ) )

proof end;

theorem Th49: :: NDIFF_1:49

for T, S being non trivial 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

proof end;

theorem :: NDIFF_1:50

for X being set
for S, T being non trivial RealNormSpace
for f being PartFunc of S,T st f is_differentiable_on X holds
f is_continuous_on X

proof end;

theorem :: NDIFF_1:51

for X being set
for T, S being non trivial 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:52

for T, S being non trivial 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 REST 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;