:: Properties of Partial Functions from a Domain to the Set of Real Numbers
:: by Jaros{\l}aw Kotowicz and Yuji Sakai
::
:: Received March 15, 1993
:: Copyright (c) 1993 Association of Mizar Users
:: deftheorem defines max+ RFUNCT_3:def 1 :
:: deftheorem defines max- RFUNCT_3:def 2 :
theorem Th1: :: RFUNCT_3:1
theorem Th2: :: RFUNCT_3:2
theorem Th3: :: RFUNCT_3:3
theorem Th4: :: RFUNCT_3:4
theorem Th5: :: RFUNCT_3:5
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} = {}
theorem :: RFUNCT_3:6
canceled;
theorem :: RFUNCT_3:7
canceled;
theorem Th8: :: RFUNCT_3:8
theorem Th9: :: RFUNCT_3:9
theorem Th10: :: RFUNCT_3:10
theorem Th11: :: RFUNCT_3:11
theorem Th12: :: RFUNCT_3:12
theorem Th13: :: RFUNCT_3:13
theorem :: RFUNCT_3:14
theorem :: RFUNCT_3:15
:: 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;
:: original: +redefine func F1 + F2 -> Element of
PFuncs D,
REAL ;
coherence
F1 + F2 is Element of PFuncs D,REAL
:: original: -redefine func F1 - F2 -> Element of
PFuncs D,
REAL ;
coherence
F1 - F2 is Element of PFuncs D,REAL
:: original: (#)redefine func F1 (#) F2 -> Element of
PFuncs D,
REAL ;
coherence
F1 (#) F2 is Element of PFuncs D,REAL
:: original: /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:
:: RFUNCT_3:def 4
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: :: RFUNCT_3:16
theorem Th17: :: RFUNCT_3:17
theorem Th18: :: RFUNCT_3:18
theorem Th19: :: RFUNCT_3:19
theorem Th20: :: RFUNCT_3:20
:: deftheorem defines Sum RFUNCT_3:def 5 :
theorem Th21: :: RFUNCT_3:21
theorem :: RFUNCT_3:22
canceled;
theorem Th23: :: RFUNCT_3:23
theorem Th24: :: RFUNCT_3:24
theorem :: RFUNCT_3:25
theorem Th26: :: RFUNCT_3:26
theorem :: RFUNCT_3:27
theorem :: RFUNCT_3:28
:: 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:
:: RFUNCT_3:def 7
(
len it = min (len R),
(len f) & ( for
n being
Element of
NAT st
n in dom it holds
for
F being
PartFunc of
D,
REAL 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 D, REAL
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 D, REAL
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 D, REAL
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: :: RFUNCT_3:29
theorem :: RFUNCT_3:30
theorem Th31: :: RFUNCT_3:31
theorem Th32: :: RFUNCT_3:32
theorem Th33: :: RFUNCT_3:33
theorem Th34: :: RFUNCT_3:34
theorem :: RFUNCT_3:35
theorem :: RFUNCT_3:36
:: deftheorem Def10 defines max+ RFUNCT_3:def 10 :
:: deftheorem Def11 defines max- RFUNCT_3:def 11 :
theorem :: RFUNCT_3:37
theorem Th38: :: RFUNCT_3:38
theorem Th39: :: RFUNCT_3:39
theorem Th40: :: RFUNCT_3:40
theorem Th41: :: RFUNCT_3:41
theorem Th42: :: RFUNCT_3:42
theorem Th43: :: RFUNCT_3:43
theorem :: RFUNCT_3:44
theorem :: RFUNCT_3:45
theorem :: RFUNCT_3:46
theorem Th47: :: RFUNCT_3:47
theorem :: RFUNCT_3:48
theorem Th49: :: RFUNCT_3:49
theorem :: RFUNCT_3:50
theorem Th51: :: RFUNCT_3:51
theorem :: RFUNCT_3:52
theorem Th53: :: RFUNCT_3:53
theorem :: RFUNCT_3:54
:: deftheorem RFUNCT_3:def 12 :
canceled;
:: deftheorem Def13 defines is_convex_on RFUNCT_3:def 13 :
theorem Th55: :: RFUNCT_3:55
theorem :: RFUNCT_3:56
theorem :: RFUNCT_3:57
theorem :: RFUNCT_3:58
theorem :: RFUNCT_3:59
theorem :: RFUNCT_3:60
theorem :: RFUNCT_3:61
theorem Th62: :: RFUNCT_3:62
theorem :: RFUNCT_3:63
theorem Th64: :: RFUNCT_3:64
theorem :: RFUNCT_3:65
:: deftheorem Def14 defines FinS RFUNCT_3:def 14 :
theorem Th66: :: RFUNCT_3:66
theorem Th67: :: RFUNCT_3:67
theorem Th68: :: RFUNCT_3:68
theorem Th69: :: RFUNCT_3:69
theorem Th70: :: RFUNCT_3:70
theorem Th71: :: RFUNCT_3:71
theorem Th72: :: RFUNCT_3:72
theorem Th73: :: RFUNCT_3:73
defpred S1[ Element of NAT ] means for D being non empty set
for F being PartFunc of D, REAL
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 :: RFUNCT_3:74
theorem Th75: :: RFUNCT_3:75
theorem Th76: :: RFUNCT_3:76
theorem :: RFUNCT_3:77
theorem :: RFUNCT_3:78
theorem Th79: :: RFUNCT_3:79
:: deftheorem defines Sum RFUNCT_3:def 15 :
theorem Th80: :: RFUNCT_3:80
theorem Th81: :: RFUNCT_3:81
theorem :: RFUNCT_3:82
theorem :: RFUNCT_3:83
theorem :: RFUNCT_3:84
theorem :: RFUNCT_3:85
theorem :: RFUNCT_3:86
theorem :: RFUNCT_3:87