environ
vocabularies HIDDEN, NUMBERS, REAL_1, ZFMISC_1, NORMSP_1, PRE_TOPC, PARTFUN1, FUNCT_1, NAT_1, FDIFF_1, SUBSET_1, RELAT_1, LOPBAN_1, ORDINAL4, RCOMP_1, TARSKI, ARYTM_3, VALUED_1, FUNCT_2, ARYTM_1, CARD_1, XXREAL_0, XBOOLE_0, CARD_3, FINSEQ_1, NDIFF_6;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, CARD_3, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, FINSEQ_1, STRUCT_0, PRE_TOPC, RLVECT_1, NORMSP_1, VFUNCT_1, LOPBAN_1, NFCONT_1, NDIFF_1;
definitions ;
theorems TARSKI, ZFMISC_1, XBOOLE_0, XBOOLE_1, BINOP_1, NAT_1, RELAT_1, FUNCT_1, VFUNCT_1, INT_1, FUNCT_2, FINSEQ_1, NDIFF_1, XREAL_1, XXREAL_0, RELSET_1, PRVECT_3, XTUPLE_0, PARTFUN1;
schemes FUNCT_2, NAT_1, BINOP_1, RECDEF_1;
registrations RELSET_1, STRUCT_0, ORDINAL1, XREAL_0, FUNCT_1, INT_1, FUNCT_2, XBOOLE_0, SUBSET_1, FINSEQ_1, CARD_3, LOPBAN_1, PRVECT_3, NAT_1, AOFA_A00;
constructors HIDDEN, NFCONT_1, VFUNCT_1, NDIFF_1, RELSET_1, PRVECT_2;
requirements HIDDEN, SUBSET, REAL, NUMERALS, ARITHM;
equalities XCMPLX_0, BINOP_1;
expansions ;
theorem
for
D,
E,
F being non
empty set ex
I being
Function of
(Funcs (D,(Funcs (E,F)))),
(Funcs ([:D,E:],F)) st
(
I is
bijective & ( for
f being
Function of
D,
(Funcs (E,F)) for
d,
e being
object st
d in D &
e in E holds
(I . f) . (
d,
e)
= (f . d) . e ) )
theorem Th2:
for
D,
E,
F being non
empty set ex
I being
Function of
(Funcs (D,(Funcs (E,F)))),
(Funcs ([:E,D:],F)) st
(
I is
bijective & ( for
f being
Function of
D,
(Funcs (E,F)) for
e,
d being
object st
e in E &
d in D holds
(I . f) . (
e,
d)
= (f . d) . e ) )
definition
let S,
T be
RealNormSpace;
let f be
PartFunc of
S,
T;
let Z be
Subset of
S;
existence
ex b1 being Function st
( dom b1 = NAT & b1 . 0 = f | Z & ( for i being Nat holds b1 . (i + 1) = (modetrans ((b1 . i),S,(diff_SP (i,S,T)))) `| Z ) )
uniqueness
for b1, b2 being Function st dom b1 = NAT & b1 . 0 = f | Z & ( for i being Nat holds b1 . (i + 1) = (modetrans ((b1 . i),S,(diff_SP (i,S,T)))) `| Z ) & dom b2 = NAT & b2 . 0 = f | Z & ( for i being Nat holds b2 . (i + 1) = (modetrans ((b2 . i),S,(diff_SP (i,S,T)))) `| Z ) holds
b1 = b2
end;
theorem Th19:
for
S,
T being
RealNormSpace for
Z being
Subset of
S for
n being
Nat for
f being
PartFunc of
S,
T st 1
<= n &
f is_differentiable_on n,
Z holds
for
i being
Nat st
i <= n holds
(
(diff_SP (S,T)) . i is
RealNormSpace &
(diff (f,Z)) . i is
PartFunc of
S,
(diff_SP (i,S,T)) &
dom (diff (f,i,Z)) = Z )
theorem Th20:
for
S,
T being
RealNormSpace for
Z being
Subset of
S for
n being
Nat for
f,
g being
PartFunc of
S,
T st 1
<= n &
f is_differentiable_on n,
Z &
g is_differentiable_on n,
Z holds
for
i being
Nat st
i <= n holds
diff (
(f + g),
i,
Z)
= (diff (f,i,Z)) + (diff (g,i,Z))
theorem Th22:
for
S,
T being
RealNormSpace for
Z being
Subset of
S for
n being
Nat for
f,
g being
PartFunc of
S,
T st 1
<= n &
f is_differentiable_on n,
Z &
g is_differentiable_on n,
Z holds
for
i being
Nat st
i <= n holds
diff (
(f - g),
i,
Z)
= (diff (f,i,Z)) - (diff (g,i,Z))