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 :
:: 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 ,;
let X be
set ;
assume A1:
f is_differentiable_on X
;
func f `| X -> PartFunc of ,
means :
Def9:
(
dom it = X & ( for
x being
Point of st
x in X holds
it /. x = diff f,
x ) );
existence
ex b1 being PartFunc of , st
( dom b1 = X & ( for x being Point of st x in X holds
b1 /. x = diff f,x ) )
uniqueness
for b1, b2 being PartFunc of , st dom b1 = X & ( for x being Point of st x in X holds
b1 /. x = diff f,x ) & dom b2 = X & ( for x being Point of 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