begin
:: deftheorem defines max+ RFUNCT_3:def 1 :
:: deftheorem defines max- RFUNCT_3:def 2 :
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
Lm1:
for n being Element of NAT
for D being non empty set
for f being FinSequence of D st len f <= n holds
f | n = f
Lm2:
for f being Function
for x being set st not x in rng f holds
f " {x} = {}
begin
theorem
canceled;
theorem
canceled;
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem
theorem
:: deftheorem Def3 defines PartFunc-set RFUNCT_3:def 3 :
definition
let D be non
empty set ;
let E be
real-membered set ;
let F1,
F2 be
Element of
PFuncs D,
E;
+redefine func F1 + F2 -> Element of
PFuncs D,
REAL ;
coherence
F1 + F2 is Element of PFuncs D,REAL
-redefine func F1 - F2 -> Element of
PFuncs D,
REAL ;
coherence
F1 - F2 is Element of PFuncs D,REAL
(#)redefine func F1 (#) F2 -> Element of
PFuncs D,
REAL ;
coherence
F1 (#) F2 is Element of PFuncs D,REAL
/redefine func F1 / F2 -> Element of
PFuncs D,
REAL ;
coherence
F1 / F2 is Element of PFuncs D,REAL
end;
definition
let D be non
empty set ;
func addpfunc D -> BinOp of
PFuncs D,
REAL means :
Def4:
for
F1,
F2 being
Element of
PFuncs D,
REAL holds
it . F1,
F2 = F1 + F2;
existence
ex b1 being BinOp of PFuncs D,REAL st
for F1, F2 being Element of PFuncs D,REAL holds b1 . F1,F2 = F1 + F2
uniqueness
for b1, b2 being BinOp of PFuncs D,REAL st ( for F1, F2 being Element of PFuncs D,REAL holds b1 . F1,F2 = F1 + F2 ) & ( for F1, F2 being Element of PFuncs D,REAL holds b2 . F1,F2 = F1 + F2 ) holds
b1 = b2
end;
:: deftheorem Def4 defines addpfunc RFUNCT_3:def 4 :
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
:: deftheorem defines Sum RFUNCT_3:def 5 :
theorem Th21:
theorem
canceled;
theorem Th23:
theorem Th24:
theorem
theorem Th26:
theorem
theorem
:: deftheorem Def6 defines CHI RFUNCT_3:def 6 :
definition
let D be non
empty set ;
let f be
FinSequence of
PFuncs D,
REAL ;
let R be
FinSequence of
REAL ;
func R (#) f -> FinSequence of
PFuncs D,
REAL means :
Def7:
(
len it = min (len R),
(len f) & ( for
n being
Element of
NAT st
n in dom it holds
for
F being
PartFunc of ,
for
r being
Real st
r = R . n &
F = f . n holds
it . n = r (#) F ) );
existence
ex b1 being FinSequence of PFuncs D,REAL st
( len b1 = min (len R),(len f) & ( for n being Element of NAT st n in dom b1 holds
for F being PartFunc of ,
for r being Real st r = R . n & F = f . n holds
b1 . n = r (#) F ) )
uniqueness
for b1, b2 being FinSequence of PFuncs D,REAL st len b1 = min (len R),(len f) & ( for n being Element of NAT st n in dom b1 holds
for F being PartFunc of ,
for r being Real st r = R . n & F = f . n holds
b1 . n = r (#) F ) & len b2 = min (len R),(len f) & ( for n being Element of NAT st n in dom b2 holds
for F being PartFunc of ,
for r being Real st r = R . n & F = f . n holds
b2 . n = r (#) F ) holds
b1 = b2
end;
:: deftheorem Def7 defines (#) RFUNCT_3:def 7 :
:: deftheorem Def8 defines # RFUNCT_3:def 8 :
:: deftheorem Def9 defines is_common_for_dom RFUNCT_3:def 9 :
theorem Th29:
theorem
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem
theorem
:: deftheorem Def10 defines max+ RFUNCT_3:def 10 :
:: deftheorem Def11 defines max- RFUNCT_3:def 11 :
theorem
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem
theorem
theorem
theorem Th47:
theorem
theorem Th49:
theorem
theorem Th51:
theorem
theorem Th53:
theorem
:: deftheorem RFUNCT_3:def 12 :
canceled;
:: deftheorem Def13 defines is_convex_on RFUNCT_3:def 13 :
theorem Th55:
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th62:
theorem
theorem Th64:
theorem
:: deftheorem Def14 defines FinS RFUNCT_3:def 14 :
theorem Th66:
theorem Th67:
theorem Th68:
theorem Th69:
theorem Th70:
theorem Th71:
theorem Th72:
theorem Th73:
defpred S1[ Element of NAT ] means for D being non empty set
for F being PartFunc of ,
for X, Y being set
for Z being finite set st Z = dom (F | Y) & dom (F | X) is finite & Y c= X & $1 = card Z & ( for d1, d2 being Element of D st d1 in dom (F | Y) & d2 in dom (F | (X \ Y)) holds
F . d1 >= F . d2 ) holds
FinS F,X = (FinS F,Y) ^ (FinS F,(X \ Y));
Lm3:
S1[ 0 ]
Lm4:
for n being Element of NAT st S1[n] holds
S1[n + 1]
theorem
theorem Th75:
theorem Th76:
theorem
theorem
theorem Th79:
:: deftheorem defines Sum RFUNCT_3:def 15 :
theorem Th80:
theorem Th81:
theorem
theorem
theorem
theorem
theorem
theorem