:: Partial Functions
:: by Czes{\l}aw Byli\'nski
::
:: Received September 18, 1989
:: Copyright (c) 1990 Association of Mizar Users
theorem :: PARTFUN1:1
canceled;
theorem Th2: :: PARTFUN1:2
theorem Th3: :: PARTFUN1:3
Lm1:
dom {} = {}
;
theorem :: PARTFUN1:4
canceled;
theorem :: PARTFUN1:5
canceled;
theorem :: PARTFUN1:6
canceled;
theorem :: PARTFUN1:7
canceled;
theorem :: PARTFUN1:8
canceled;
theorem :: PARTFUN1:9
canceled;
theorem :: PARTFUN1:10
canceled;
theorem :: PARTFUN1:11
canceled;
theorem :: PARTFUN1:12
canceled;
theorem :: PARTFUN1:13
canceled;
theorem :: PARTFUN1:14
canceled;
theorem :: PARTFUN1:15
canceled;
theorem :: PARTFUN1:16
canceled;
theorem :: PARTFUN1:17
canceled;
theorem :: PARTFUN1:18
canceled;
theorem :: PARTFUN1:19
canceled;
theorem :: PARTFUN1:20
canceled;
theorem :: PARTFUN1:21
canceled;
theorem :: PARTFUN1:22
canceled;
theorem :: PARTFUN1:23
canceled;
theorem :: PARTFUN1:24
canceled;
theorem :: PARTFUN1:25
canceled;
theorem :: PARTFUN1:26
theorem Th27: :: PARTFUN1:27
theorem :: PARTFUN1:28
canceled;
theorem :: PARTFUN1:29
canceled;
theorem :: PARTFUN1:30
canceled;
theorem :: PARTFUN1:31
canceled;
theorem :: PARTFUN1:32
canceled;
theorem :: PARTFUN1:33
canceled;
theorem :: PARTFUN1:34
scheme :: PARTFUN1:sch 2
PartFuncEx{
F1()
-> set ,
F2()
-> set ,
P1[
set ,
set ] } :
ex
f being
PartFunc of
F1(),
F2() st
( ( for
x being
set holds
(
x in dom f iff (
x in F1() & ex
y being
set st
P1[
x,
y] ) ) ) & ( for
x being
set st
x in dom f holds
P1[
x,
f . x] ) )
provided
A1:
for
x,
y being
set st
x in F1() &
P1[
x,
y] holds
y in F2()
and A2:
for
x,
y1,
y2 being
set st
x in F1() &
P1[
x,
y1] &
P1[
x,
y2] holds
y1 = y2
theorem :: PARTFUN1:35
canceled;
theorem :: PARTFUN1:36
theorem :: PARTFUN1:37
theorem :: PARTFUN1:38
theorem :: PARTFUN1:39
theorem :: PARTFUN1:40
canceled;
theorem :: PARTFUN1:41
canceled;
theorem :: PARTFUN1:42
canceled;
theorem :: PARTFUN1:43
theorem Th44: :: PARTFUN1:44
theorem :: PARTFUN1:45
theorem :: PARTFUN1:46
theorem Th47: :: PARTFUN1:47
theorem :: PARTFUN1:48
canceled;
theorem :: PARTFUN1:49
theorem :: PARTFUN1:50
canceled;
theorem :: PARTFUN1:51
canceled;
theorem :: PARTFUN1:52
canceled;
theorem :: PARTFUN1:53
canceled;
theorem :: PARTFUN1:54
canceled;
theorem :: PARTFUN1:55
canceled;
theorem :: PARTFUN1:56
canceled;
theorem :: PARTFUN1:57
canceled;
theorem :: PARTFUN1:58
canceled;
theorem :: PARTFUN1:59
canceled;
theorem :: PARTFUN1:60
canceled;
theorem :: PARTFUN1:61
canceled;
theorem :: PARTFUN1:62
canceled;
theorem :: PARTFUN1:63
canceled;
theorem :: PARTFUN1:64
canceled;
theorem :: PARTFUN1:65
canceled;
theorem :: PARTFUN1:66
canceled;
theorem :: PARTFUN1:67
canceled;
theorem :: PARTFUN1:68
canceled;
theorem Th69: :: PARTFUN1:69
theorem :: PARTFUN1:70
theorem :: PARTFUN1:71
theorem :: PARTFUN1:72
theorem Th73: :: PARTFUN1:73
theorem :: PARTFUN1:74
:: deftheorem PARTFUN1:def 1 :
canceled;
:: deftheorem PARTFUN1:def 2 :
canceled;
:: deftheorem defines <: PARTFUN1:def 3 :
theorem :: PARTFUN1:75
canceled;
theorem Th76: :: PARTFUN1:76
theorem Th77: :: PARTFUN1:77
theorem Th78: :: PARTFUN1:78
theorem Th79: :: PARTFUN1:79
theorem Th80: :: PARTFUN1:80
theorem :: PARTFUN1:81
theorem Th82: :: PARTFUN1:82
theorem Th83: :: PARTFUN1:83
theorem :: PARTFUN1:84
theorem Th85: :: PARTFUN1:85
theorem :: PARTFUN1:86
theorem :: PARTFUN1:87
theorem :: PARTFUN1:88
canceled;
theorem :: PARTFUN1:89
canceled;
theorem :: PARTFUN1:90
canceled;
theorem Th91: :: PARTFUN1:91
theorem Th92: :: PARTFUN1:92
theorem :: PARTFUN1:93
theorem Th94: :: PARTFUN1:94
theorem :: PARTFUN1:95
theorem :: PARTFUN1:96
canceled;
theorem :: PARTFUN1:97
:: deftheorem Def4 defines total PARTFUN1:def 4 :
theorem :: PARTFUN1:98
canceled;
theorem :: PARTFUN1:99
canceled;
theorem :: PARTFUN1:100
canceled;
theorem :: PARTFUN1:101
canceled;
theorem :: PARTFUN1:102
canceled;
theorem :: PARTFUN1:103
canceled;
theorem :: PARTFUN1:104
canceled;
theorem :: PARTFUN1:105
canceled;
theorem :: PARTFUN1:106
canceled;
theorem :: PARTFUN1:107
canceled;
theorem :: PARTFUN1:108
canceled;
theorem :: PARTFUN1:109
canceled;
theorem :: PARTFUN1:110
canceled;
theorem :: PARTFUN1:111
canceled;
theorem :: PARTFUN1:112
canceled;
theorem Th113: :: PARTFUN1:113
theorem :: PARTFUN1:114
theorem :: PARTFUN1:115
theorem :: PARTFUN1:116
theorem :: PARTFUN1:117
:: deftheorem Def5 defines PFuncs PARTFUN1:def 5 :
theorem :: PARTFUN1:118
canceled;
theorem Th119: :: PARTFUN1:119
theorem Th120: :: PARTFUN1:120
theorem :: PARTFUN1:121
theorem :: PARTFUN1:122
theorem :: PARTFUN1:123
theorem :: PARTFUN1:124
canceled;
theorem :: PARTFUN1:125
canceled;
theorem :: PARTFUN1:126
canceled;
theorem :: PARTFUN1:127
canceled;
theorem :: PARTFUN1:128
:: deftheorem Def6 defines tolerates PARTFUN1:def 6 :
theorem :: PARTFUN1:129
canceled;
theorem Th130: :: PARTFUN1:130
theorem Th131: :: PARTFUN1:131
theorem Th132: :: PARTFUN1:132
theorem :: PARTFUN1:133
canceled;
theorem :: PARTFUN1:134
canceled;
theorem :: PARTFUN1:135
theorem Th136: :: PARTFUN1:136
theorem :: PARTFUN1:137
canceled;
theorem :: PARTFUN1:138
theorem :: PARTFUN1:139
theorem :: PARTFUN1:140
theorem Th141: :: PARTFUN1:141
theorem :: PARTFUN1:142
theorem :: PARTFUN1:143
theorem :: PARTFUN1:144
theorem :: PARTFUN1:145
theorem Th146: :: PARTFUN1:146
theorem :: PARTFUN1:147
theorem Th148: :: PARTFUN1:148
theorem :: PARTFUN1:149
canceled;
theorem :: PARTFUN1:150
canceled;
theorem :: PARTFUN1:151
canceled;
theorem :: PARTFUN1:152
canceled;
theorem :: PARTFUN1:153
canceled;
theorem :: PARTFUN1:154
canceled;
theorem :: PARTFUN1:155
canceled;
theorem :: PARTFUN1:156
canceled;
theorem :: PARTFUN1:157
canceled;
theorem Th158: :: PARTFUN1:158
theorem :: PARTFUN1:159
canceled;
theorem :: PARTFUN1:160
canceled;
theorem :: PARTFUN1:161
canceled;
theorem Th162: :: PARTFUN1:162
:: deftheorem Def7 defines TotFuncs PARTFUN1:def 7 :
theorem :: PARTFUN1:163
canceled;
theorem :: PARTFUN1:164
canceled;
theorem :: PARTFUN1:165
canceled;
theorem :: PARTFUN1:166
canceled;
theorem :: PARTFUN1:167
canceled;
theorem Th168: :: PARTFUN1:168
theorem Th169: :: PARTFUN1:169
theorem :: PARTFUN1:170
canceled;
theorem Th171: :: PARTFUN1:171
theorem :: PARTFUN1:172
canceled;
theorem :: PARTFUN1:173
canceled;
theorem Th174: :: PARTFUN1:174
theorem :: PARTFUN1:175
theorem :: PARTFUN1:176
theorem :: PARTFUN1:177
canceled;
theorem :: PARTFUN1:178
canceled;
theorem :: PARTFUN1:179
canceled;
theorem :: PARTFUN1:180
canceled;
theorem :: PARTFUN1:181
canceled;
theorem :: PARTFUN1:182
canceled;
theorem :: PARTFUN1:183
canceled;
theorem :: PARTFUN1:184
canceled;
theorem :: PARTFUN1:185
theorem :: PARTFUN1:186
Lm3:
for X being set
for R being Relation of X st R = id X holds
R is total
Lm4:
for X being set
for R being Relation st R = id X holds
( R is reflexive & R is symmetric & R is antisymmetric & R is transitive )
Lm5:
for X being set holds id X is Relation of X
theorem Th187: :: PARTFUN1:187
theorem :: PARTFUN1:188
:: deftheorem defines /. PARTFUN1:def 8 :