begin
theorem Th1:
theorem Th2:
theorem
theorem Th4:
theorem
:: deftheorem Def1 defines non-zero NDIFF_1:def 1 :
theorem Th6:
theorem Th7:
:: deftheorem Def2 defines (#) NDIFF_1:def 2 :
:: deftheorem Def3 defines * NDIFF_1:def 3 :
theorem
theorem Th9:
theorem Th10:
theorem
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem
canceled;
theorem
canceled;
theorem
canceled;
:: deftheorem Def4 defines convergent_to_0 NDIFF_1:def 4 :
theorem Th21:
theorem Th22:
theorem Th23:
theorem
theorem
:: deftheorem Def5 defines REST-like NDIFF_1:def 5 :
theorem
theorem Th27:
theorem
canceled;
theorem
canceled;
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
:: 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:
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
ex b1 being Point of (R_NormSpace_of_BoundedLinearOperators S,T) 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) = (b1 . (x - x0)) + (R /. (x - x0)) )
uniqueness
for b1, b2 being Point of (R_NormSpace_of_BoundedLinearOperators S,T) st 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) = (b1 . (x - x0)) + (R /. (x - x0)) ) & 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) = (b2 . (x - x0)) + (R /. (x - x0)) ) holds
b1 = b2
end;
:: deftheorem Def7 defines diff NDIFF_1:def 7 :
:: deftheorem Def8 defines is_differentiable_on NDIFF_1:def 8 :
theorem Th35:
theorem Th36:
theorem
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:
(
dom it = X & ( for
x being
Point of
S st
x in X holds
it /. x = diff f,
x ) );
existence
ex b1 being PartFunc of S,(R_NormSpace_of_BoundedLinearOperators S,T) st
( dom b1 = X & ( for x being Point of S st x in X holds
b1 /. x = diff f,x ) )
uniqueness
for b1, b2 being PartFunc of S,(R_NormSpace_of_BoundedLinearOperators S,T) st dom b1 = X & ( for x being Point of S st x in X holds
b1 /. x = diff f,x ) & dom b2 = X & ( for x being Point of S st x in X holds
b2 /. x = diff f,x ) holds
b1 = b2
end;
:: deftheorem Def9 defines `| NDIFF_1:def 9 :
theorem
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th49:
theorem
theorem
theorem