:: Functions from a Set to a Set
:: by Czes{\l}aw Byli\'nski
::
:: Received April 6, 1989
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem Def1 defines quasi_total FUNCT_2:def 1 :
theorem :: FUNCT_2:1
canceled;
theorem :: FUNCT_2:2
canceled;
theorem :: FUNCT_2:3
theorem Th4: :: FUNCT_2:4
theorem :: FUNCT_2:5
theorem Th6: :: FUNCT_2:6
theorem Th7: :: FUNCT_2:7
theorem :: FUNCT_2:8
theorem :: FUNCT_2:9
:: deftheorem Def2 defines Funcs FUNCT_2:def 2 :
theorem :: FUNCT_2:10
canceled;
theorem Th11: :: FUNCT_2:11
theorem :: FUNCT_2:12
theorem :: FUNCT_2:13
canceled;
theorem :: FUNCT_2:14
canceled;
theorem :: FUNCT_2:15
canceled;
theorem :: FUNCT_2:16
theorem Th17: :: FUNCT_2:17
theorem Th18: :: FUNCT_2:18
for
X,
Y being
set for
f1,
f2 being
Function of
X,
Y st ( for
x being
set st
x in X holds
f1 . x = f2 . x ) holds
f1 = f2
theorem Th19: :: FUNCT_2:19
theorem :: FUNCT_2:20
theorem Th21: :: FUNCT_2:21
theorem :: FUNCT_2:22
theorem :: FUNCT_2:23
theorem :: FUNCT_2:24
theorem :: FUNCT_2:25
theorem :: FUNCT_2:26
theorem :: FUNCT_2:27
theorem :: FUNCT_2:28
theorem :: FUNCT_2:29
theorem :: FUNCT_2:30
theorem Th31: :: FUNCT_2:31
theorem :: FUNCT_2:32
theorem :: FUNCT_2:33
canceled;
theorem :: FUNCT_2:34
theorem :: FUNCT_2:35
theorem :: FUNCT_2:36
theorem :: FUNCT_2:37
theorem Th38: :: FUNCT_2:38
theorem :: FUNCT_2:39
canceled;
theorem :: FUNCT_2:40
for
X,
Y,
Z being
set for
f being
Function of
X,
Y st
X c= Z holds
f | Z = f
theorem :: FUNCT_2:41
theorem :: FUNCT_2:42
canceled;
theorem :: FUNCT_2:43
theorem :: FUNCT_2:44
theorem :: FUNCT_2:45
theorem :: FUNCT_2:46
for
X,
Y,
Q being
set for
f being
Function of
X,
Y st
Y <> {} holds
for
x being
set holds
(
x in f " Q iff (
x in X &
f . x in Q ) )
theorem :: FUNCT_2:47
theorem Th48: :: FUNCT_2:48
theorem :: FUNCT_2:49
theorem Th50: :: FUNCT_2:50
theorem :: FUNCT_2:51
theorem :: FUNCT_2:52
canceled;
theorem :: FUNCT_2:53
theorem :: FUNCT_2:54
canceled;
theorem :: FUNCT_2:55
canceled;
theorem :: FUNCT_2:56
canceled;
theorem :: FUNCT_2:57
canceled;
theorem :: FUNCT_2:58
canceled;
theorem :: FUNCT_2:59
theorem :: FUNCT_2:60
theorem :: FUNCT_2:61
theorem Th62: :: FUNCT_2:62
theorem :: FUNCT_2:63
canceled;
theorem :: FUNCT_2:64
theorem Th65: :: FUNCT_2:65
theorem Th66: :: FUNCT_2:66
theorem Th67: :: FUNCT_2:67
theorem :: FUNCT_2:68
canceled;
theorem :: FUNCT_2:69
canceled;
theorem :: FUNCT_2:70
canceled;
theorem :: FUNCT_2:71
canceled;
theorem :: FUNCT_2:72
canceled;
theorem Th73: :: FUNCT_2:73
theorem :: FUNCT_2:74
canceled;
theorem :: FUNCT_2:75
theorem :: FUNCT_2:76
theorem Th77: :: FUNCT_2:77
theorem :: FUNCT_2:78
canceled;
theorem :: FUNCT_2:79
canceled;
theorem :: FUNCT_2:80
canceled;
theorem :: FUNCT_2:81
canceled;
theorem :: FUNCT_2:82
canceled;
:: deftheorem Def3 defines onto FUNCT_2:def 3 :
:: deftheorem Def4 defines bijective FUNCT_2:def 4 :
theorem Th83: :: FUNCT_2:83
theorem :: FUNCT_2:84
canceled;
theorem :: FUNCT_2:85
theorem :: FUNCT_2:86
theorem :: FUNCT_2:87
theorem :: FUNCT_2:88
theorem :: FUNCT_2:89
canceled;
theorem :: FUNCT_2:90
canceled;
theorem :: FUNCT_2:91
canceled;
theorem Th92: :: FUNCT_2:92
theorem :: FUNCT_2:93
canceled;
theorem :: FUNCT_2:94
canceled;
theorem :: FUNCT_2:95
canceled;
theorem :: FUNCT_2:96
canceled;
theorem :: FUNCT_2:97
canceled;
theorem :: FUNCT_2:98
canceled;
theorem :: FUNCT_2:99
canceled;
theorem :: FUNCT_2:100
canceled;
theorem :: FUNCT_2:101
canceled;
theorem :: FUNCT_2:102
canceled;
theorem :: FUNCT_2:103
canceled;
theorem :: FUNCT_2:104
canceled;
theorem :: FUNCT_2:105
canceled;
theorem :: FUNCT_2:106
canceled;
theorem :: FUNCT_2:107
canceled;
theorem :: FUNCT_2:108
canceled;
theorem :: FUNCT_2:109
canceled;
theorem :: FUNCT_2:110
canceled;
theorem :: FUNCT_2:111
canceled;
theorem :: FUNCT_2:112
canceled;
theorem Th113: :: FUNCT_2:113
for
X,
Y being
set for
f1,
f2 being
Function of
X,
Y st ( for
x being
Element of
X holds
f1 . x = f2 . x ) holds
f1 = f2
theorem :: FUNCT_2:114
canceled;
theorem Th115: :: FUNCT_2:115
for
X,
Y,
P being
set for
f being
Function of
X,
Y for
y being
set st
y in f .: P holds
ex
x being
set st
(
x in X &
x in P &
y = f . x )
theorem :: FUNCT_2:116
theorem :: FUNCT_2:117
canceled;
theorem :: FUNCT_2:118
canceled;
theorem :: FUNCT_2:119
canceled;
theorem :: FUNCT_2:120
canceled;
theorem Th121: :: FUNCT_2:121
scheme :: FUNCT_2:sch 5
Lambda1C{
F1()
-> set ,
F2()
-> set ,
P1[
set ],
F3(
set )
-> set ,
F4(
set )
-> set } :
ex
f being
Function of
F1(),
F2() st
for
x being
set st
x in F1() holds
( (
P1[
x] implies
f . x = F3(
x) ) & (
P1[
x] implies
f . x = F4(
x) ) )
provided
A1:
for
x being
set st
x in F1() holds
( (
P1[
x] implies
F3(
x)
in F2() ) & (
P1[
x] implies
F4(
x)
in F2() ) )
theorem :: FUNCT_2:122
canceled;
theorem :: FUNCT_2:123
canceled;
theorem :: FUNCT_2:124
canceled;
theorem :: FUNCT_2:125
canceled;
theorem :: FUNCT_2:126
canceled;
theorem :: FUNCT_2:127
canceled;
theorem :: FUNCT_2:128
canceled;
theorem :: FUNCT_2:129
canceled;
theorem :: FUNCT_2:130
theorem :: FUNCT_2:131
theorem :: FUNCT_2:132
theorem Th133: :: FUNCT_2:133
theorem :: FUNCT_2:134
theorem :: FUNCT_2:135
canceled;
theorem Th136: :: FUNCT_2:136
theorem :: FUNCT_2:137
canceled;
theorem :: FUNCT_2:138
canceled;
theorem :: FUNCT_2:139
canceled;
theorem :: FUNCT_2:140
canceled;
theorem :: FUNCT_2:141
theorem Th142: :: FUNCT_2:142
theorem :: FUNCT_2:143
theorem :: FUNCT_2:144
canceled;
theorem Th145: :: FUNCT_2:145
theorem :: FUNCT_2:146
theorem :: FUNCT_2:147
canceled;
theorem Th148: :: FUNCT_2:148
theorem :: FUNCT_2:149
canceled;
theorem :: FUNCT_2:150
canceled;
theorem :: FUNCT_2:151
canceled;
theorem :: FUNCT_2:152
theorem :: FUNCT_2:153
canceled;
theorem :: FUNCT_2:154
theorem Th155: :: FUNCT_2:155
theorem :: FUNCT_2:156
theorem :: FUNCT_2:157
canceled;
theorem Th158: :: FUNCT_2:158
theorem :: FUNCT_2:159
theorem :: FUNCT_2:160
theorem Th161: :: FUNCT_2:161
theorem :: FUNCT_2:162
theorem :: FUNCT_2:163
canceled;
theorem :: FUNCT_2:164
theorem :: FUNCT_2:165
theorem Th166: :: FUNCT_2:166
theorem Th167: :: FUNCT_2:167
theorem :: FUNCT_2:168
theorem :: FUNCT_2:169
definition
let A,
B,
C be non
empty set ;
canceled;let f be
Function of
A,
[:B,C:];
:: original: pr1redefine func pr1 f -> Function of
A,
B means :: FUNCT_2:def 6
for
x being
Element of
A holds
it . x = (f . x) `1 ;
coherence
pr1 f is Function of A,B
compatibility
for b1 being Function of A,B holds
( b1 = pr1 f iff for x being Element of A holds b1 . x = (f . x) `1 )
:: original: pr2redefine func pr2 f -> Function of
A,
C means :: FUNCT_2:def 7
for
x being
Element of
A holds
it . x = (f . x) `2 ;
coherence
pr2 f is Function of A,C
compatibility
for b1 being Function of A,C holds
( b1 = pr2 f iff for x being Element of A holds b1 . x = (f . x) `2 )
end;
:: deftheorem FUNCT_2:def 5 :
canceled;
:: deftheorem defines pr1 FUNCT_2:def 6 :
:: deftheorem defines pr2 FUNCT_2:def 7 :
:: deftheorem defines = FUNCT_2:def 8 :
:: deftheorem defines = FUNCT_2:def 9 :
for
A,
B being
set for
f1,
f2 being
Function of
A,
B holds
(
f1 = f2 iff for
a being
Element of
A holds
f1 . a = f2 . a );
theorem :: FUNCT_2:170
theorem Th171: :: FUNCT_2:171
theorem :: FUNCT_2:172
theorem :: FUNCT_2:173
theorem :: FUNCT_2:174
theorem :: FUNCT_2:175
theorem Th176: :: FUNCT_2:176
theorem :: FUNCT_2:177
theorem :: FUNCT_2:178
:: deftheorem Def10 defines " FUNCT_2:def 10 :
theorem :: FUNCT_2:179
:: deftheorem Def2 defines .: FUNCT_2:def 11 :
theorem :: FUNCT_2:180
theorem :: FUNCT_2:181
theorem :: FUNCT_2:182
theorem :: FUNCT_2:183
theorem :: FUNCT_2:184
:: deftheorem Def12 defines /* FUNCT_2:def 12 :
theorem Th185: :: FUNCT_2:185
theorem Th186: :: FUNCT_2:186
theorem :: FUNCT_2:187
theorem :: FUNCT_2:188
theorem :: FUNCT_2:189
theorem Th190: :: FUNCT_2:190
theorem :: FUNCT_2:191
theorem :: FUNCT_2:192
theorem :: FUNCT_2:193
theorem Th194: :: FUNCT_2:194
theorem :: FUNCT_2:195