:: Partially Ordered Sets
:: by Wojciech A. Trybulec
::
:: Received August 30, 1989
:: Copyright (c) 1990 Association of Mizar Users
Lm1:
for Y being set holds
( ex X being set st
( X <> {} & X in Y ) iff union Y <> {} )
:: deftheorem Def1 defines Choice_Function ORDERS_1:def 1 :
:: deftheorem defines BOOL ORDERS_1:def 2 :
theorem :: ORDERS_1:1
canceled;
theorem :: ORDERS_1:2
canceled;
theorem :: ORDERS_1:3
canceled;
theorem :: ORDERS_1:4
theorem Th5: :: ORDERS_1:5
Lm2:
for X being set
for R being total Relation of X holds field R = X
theorem :: ORDERS_1:6
canceled;
theorem :: ORDERS_1:7
canceled;
theorem :: ORDERS_1:8
canceled;
theorem :: ORDERS_1:9
canceled;
theorem :: ORDERS_1:10
canceled;
theorem :: ORDERS_1:11
canceled;
theorem Th12: :: ORDERS_1:12
theorem :: ORDERS_1:13
theorem :: ORDERS_1:14
theorem :: ORDERS_1:15
canceled;
theorem :: ORDERS_1:16
canceled;
theorem :: ORDERS_1:17
canceled;
theorem :: ORDERS_1:18
canceled;
theorem :: ORDERS_1:19
canceled;
theorem :: ORDERS_1:20
canceled;
theorem :: ORDERS_1:21
canceled;
theorem :: ORDERS_1:22
canceled;
theorem :: ORDERS_1:23
canceled;
theorem :: ORDERS_1:24
canceled;
theorem :: ORDERS_1:25
canceled;
theorem :: ORDERS_1:26
canceled;
theorem :: ORDERS_1:27
canceled;
theorem :: ORDERS_1:28
canceled;
theorem :: ORDERS_1:29
canceled;
theorem :: ORDERS_1:30
canceled;
theorem :: ORDERS_1:31
canceled;
theorem :: ORDERS_1:32
canceled;
theorem :: ORDERS_1:33
canceled;
theorem :: ORDERS_1:34
canceled;
theorem :: ORDERS_1:35
canceled;
theorem :: ORDERS_1:36
canceled;
theorem :: ORDERS_1:37
canceled;
theorem :: ORDERS_1:38
canceled;
theorem :: ORDERS_1:39
canceled;
theorem :: ORDERS_1:40
canceled;
theorem :: ORDERS_1:41
canceled;
theorem :: ORDERS_1:42
canceled;
theorem :: ORDERS_1:43
canceled;
theorem :: ORDERS_1:44
canceled;
theorem :: ORDERS_1:45
canceled;
theorem :: ORDERS_1:46
canceled;
theorem :: ORDERS_1:47
canceled;
theorem :: ORDERS_1:48
canceled;
theorem :: ORDERS_1:49
canceled;
theorem :: ORDERS_1:50
canceled;
theorem :: ORDERS_1:51
canceled;
theorem :: ORDERS_1:52
canceled;
theorem :: ORDERS_1:53
canceled;
theorem :: ORDERS_1:54
canceled;
theorem :: ORDERS_1:55
canceled;
theorem :: ORDERS_1:56
canceled;
theorem :: ORDERS_1:57
canceled;
theorem :: ORDERS_1:58
canceled;
theorem :: ORDERS_1:59
canceled;
theorem :: ORDERS_1:60
canceled;
theorem :: ORDERS_1:61
canceled;
theorem :: ORDERS_1:62
canceled;
theorem :: ORDERS_1:63
canceled;
theorem :: ORDERS_1:64
canceled;
theorem :: ORDERS_1:65
canceled;
theorem :: ORDERS_1:66
canceled;
theorem :: ORDERS_1:67
canceled;
theorem :: ORDERS_1:68
canceled;
theorem :: ORDERS_1:69
canceled;
theorem :: ORDERS_1:70
canceled;
theorem :: ORDERS_1:71
canceled;
theorem :: ORDERS_1:72
canceled;
theorem :: ORDERS_1:73
canceled;
theorem :: ORDERS_1:74
canceled;
theorem :: ORDERS_1:75
canceled;
theorem :: ORDERS_1:76
canceled;
theorem :: ORDERS_1:77
canceled;
theorem :: ORDERS_1:78
canceled;
theorem :: ORDERS_1:79
canceled;
theorem :: ORDERS_1:80
canceled;
theorem :: ORDERS_1:81
canceled;
theorem :: ORDERS_1:82
canceled;
theorem :: ORDERS_1:83
canceled;
theorem :: ORDERS_1:84
canceled;
theorem :: ORDERS_1:85
canceled;
theorem :: ORDERS_1:86
canceled;
theorem :: ORDERS_1:87
canceled;
theorem :: ORDERS_1:88
canceled;
theorem :: ORDERS_1:89
canceled;
theorem :: ORDERS_1:90
canceled;
theorem :: ORDERS_1:91
theorem :: ORDERS_1:92
theorem Th93: :: ORDERS_1:93
theorem Th94: :: ORDERS_1:94
theorem Th95: :: ORDERS_1:95
theorem :: ORDERS_1:96
theorem :: ORDERS_1:97
theorem Th98: :: ORDERS_1:98
theorem Th99: :: ORDERS_1:99
theorem :: ORDERS_1:100
:: deftheorem defines being_quasi-order ORDERS_1:def 3 :
:: deftheorem Def4 defines being_partial-order ORDERS_1:def 4 :
:: deftheorem Def5 defines being_linear-order ORDERS_1:def 5 :
theorem :: ORDERS_1:101
canceled;
theorem :: ORDERS_1:102
canceled;
theorem :: ORDERS_1:103
canceled;
theorem :: ORDERS_1:104
theorem :: ORDERS_1:105
Lm3:
for R being Relation st R is connected holds
R ~ is connected
theorem Th106: :: ORDERS_1:106
theorem :: ORDERS_1:107
theorem :: ORDERS_1:108
theorem Th109: :: ORDERS_1:109
theorem :: ORDERS_1:110
theorem :: ORDERS_1:111
theorem :: ORDERS_1:112
Lm4:
for R being Relation holds R c= [:(field R),(field R):]
Lm5:
for R being Relation
for X being set st R is reflexive & X c= field R holds
field (R |_2 X) = X
theorem :: ORDERS_1:113
theorem :: ORDERS_1:114
theorem :: ORDERS_1:115
theorem :: ORDERS_1:116
canceled;
theorem :: ORDERS_1:117
canceled;
theorem :: ORDERS_1:118
canceled;
theorem Th119: :: ORDERS_1:119
theorem Th120: :: ORDERS_1:120
:: deftheorem Def6 defines quasi_orders ORDERS_1:def 6 :
:: deftheorem Def7 defines partially_orders ORDERS_1:def 7 :
:: deftheorem defines linearly_orders ORDERS_1:def 8 :
theorem :: ORDERS_1:121
canceled;
theorem :: ORDERS_1:122
canceled;
theorem :: ORDERS_1:123
canceled;
theorem Th124: :: ORDERS_1:124
theorem Th125: :: ORDERS_1:125
theorem :: ORDERS_1:126
theorem Th127: :: ORDERS_1:127
theorem :: ORDERS_1:128
Lm6:
for R being Relation
for X being set st R is_reflexive_in X holds
R |_2 X is reflexive
Lm7:
for R being Relation
for X being set st R is_transitive_in X holds
R |_2 X is transitive
Lm8:
for R being Relation
for X being set st R is_antisymmetric_in X holds
R |_2 X is antisymmetric
Lm9:
for R being Relation
for X being set st R is_connected_in X holds
R |_2 X is connected
theorem :: ORDERS_1:129
theorem Th130: :: ORDERS_1:130
theorem :: ORDERS_1:131
theorem :: ORDERS_1:132
Lm10:
for R being Relation
for X, Y being set st R is_connected_in X & Y c= X holds
R is_connected_in Y
theorem :: ORDERS_1:133
theorem :: ORDERS_1:134
theorem :: ORDERS_1:135
Lm11:
for R being Relation
for X being set st R is_reflexive_in X holds
R ~ is_reflexive_in X
Lm12:
for R being Relation
for X being set st R is_transitive_in X holds
R ~ is_transitive_in X
Lm13:
for R being Relation
for X being set st R is_antisymmetric_in X holds
R ~ is_antisymmetric_in X
Lm14:
for R being Relation
for X being set st R is_connected_in X holds
R ~ is_connected_in X
theorem :: ORDERS_1:136
theorem Th137: :: ORDERS_1:137
theorem :: ORDERS_1:138
theorem :: ORDERS_1:139
theorem :: ORDERS_1:140
theorem Th141: :: ORDERS_1:141
theorem :: ORDERS_1:142
theorem :: ORDERS_1:143
theorem :: ORDERS_1:144
canceled;
theorem :: ORDERS_1:145
canceled;
theorem :: ORDERS_1:146
:: deftheorem Def9 defines has_upper_Zorn_property_wrt ORDERS_1:def 9 :
:: deftheorem defines has_lower_Zorn_property_wrt ORDERS_1:def 10 :
Lm15:
for R being Relation
for X being set holds (R |_2 X) ~ = (R ~ ) |_2 X
theorem :: ORDERS_1:147
canceled;
theorem :: ORDERS_1:148
canceled;
theorem Th149: :: ORDERS_1:149
theorem :: ORDERS_1:150
theorem Th151: :: ORDERS_1:151
theorem :: ORDERS_1:152
:: deftheorem Def11 defines is_maximal_in ORDERS_1:def 11 :
:: deftheorem Def12 defines is_minimal_in ORDERS_1:def 12 :
:: deftheorem Def13 defines is_superior_of ORDERS_1:def 13 :
:: deftheorem Def14 defines is_inferior_of ORDERS_1:def 14 :
theorem :: ORDERS_1:153
canceled;
theorem :: ORDERS_1:154
canceled;
theorem :: ORDERS_1:155
canceled;
theorem :: ORDERS_1:156
canceled;
theorem :: ORDERS_1:157
theorem :: ORDERS_1:158
theorem :: ORDERS_1:159
theorem :: ORDERS_1:160
theorem :: ORDERS_1:161
theorem :: ORDERS_1:162
theorem Th163: :: ORDERS_1:163
theorem :: ORDERS_1:164
theorem :: ORDERS_1:165
theorem :: ORDERS_1:166
Lm17:
for R being Relation
for X, Y being set st R well_orders X & Y c= X holds
R well_orders Y
theorem :: ORDERS_1:167
canceled;
theorem :: ORDERS_1:168
canceled;
theorem :: ORDERS_1:169
canceled;
theorem :: ORDERS_1:170
canceled;
theorem :: ORDERS_1:171
canceled;
theorem :: ORDERS_1:172
canceled;
theorem Th173: :: ORDERS_1:173
theorem Th174: :: ORDERS_1:174
theorem Th175: :: ORDERS_1:175
for
X being
set st
X <> {} & ( for
Z being
set st
Z c= X &
Z is
c=-linear holds
ex
Y being
set st
(
Y in X & ( for
X1 being
set st
X1 in Z holds
X1 c= Y ) ) ) holds
ex
Y being
set st
(
Y in X & ( for
Z being
set st
Z in X &
Z <> Y holds
not
Y c= Z ) )
theorem Th176: :: ORDERS_1:176
for
X being
set st
X <> {} & ( for
Z being
set st
Z c= X &
Z is
c=-linear holds
ex
Y being
set st
(
Y in X & ( for
X1 being
set st
X1 in Z holds
Y c= X1 ) ) ) holds
ex
Y being
set st
(
Y in X & ( for
Z being
set st
Z in X &
Z <> Y holds
not
Z c= Y ) )
theorem Th177: :: ORDERS_1:177
theorem :: ORDERS_1:178
scheme :: ORDERS_1:sch 1
ZornMax{
F1()
-> non
empty set ,
P1[
set ,
set ] } :
ex
x being
Element of
F1() st
for
y being
Element of
F1() st
x <> y holds
not
P1[
x,
y]
provided
A1:
for
x being
Element of
F1() holds
P1[
x,
x]
and A2:
for
x,
y being
Element of
F1() st
P1[
x,
y] &
P1[
y,
x] holds
x = y
and A3:
for
x,
y,
z being
Element of
F1() st
P1[
x,
y] &
P1[
y,
z] holds
P1[
x,
z]
and A4:
for
X being
set st
X c= F1() & ( for
x,
y being
Element of
F1() st
x in X &
y in X &
P1[
x,
y] holds
P1[
y,
x] ) holds
ex
y being
Element of
F1() st
for
x being
Element of
F1() st
x in X holds
P1[
x,
y]
scheme :: ORDERS_1:sch 2
ZornMin{
F1()
-> non
empty set ,
P1[
set ,
set ] } :
ex
x being
Element of
F1() st
for
y being
Element of
F1() st
x <> y holds
not
P1[
y,
x]
provided
A1:
for
x being
Element of
F1() holds
P1[
x,
x]
and A2:
for
x,
y being
Element of
F1() st
P1[
x,
y] &
P1[
y,
x] holds
x = y
and A3:
for
x,
y,
z being
Element of
F1() st
P1[
x,
y] &
P1[
y,
z] holds
P1[
x,
z]
and A4:
for
X being
set st
X c= F1() & ( for
x,
y being
Element of
F1() st
x in X &
y in X &
P1[
x,
y] holds
P1[
y,
x] ) holds
ex
y being
Element of
F1() st
for
x being
Element of
F1() st
x in X holds
P1[
y,
x]
theorem :: ORDERS_1:179
theorem :: ORDERS_1:180
theorem :: ORDERS_1:181
theorem :: ORDERS_1:182
theorem :: ORDERS_1:183
theorem :: ORDERS_1:184
theorem :: ORDERS_1:185
theorem :: ORDERS_1:186
theorem :: ORDERS_1:187
theorem :: ORDERS_1:188
theorem :: ORDERS_1:189
theorem :: ORDERS_1:190
theorem :: ORDERS_1:191
theorem :: ORDERS_1:192
theorem :: ORDERS_1:193
theorem :: ORDERS_1:194
theorem :: ORDERS_1:195
theorem Th196: :: ORDERS_1:196
theorem :: ORDERS_1:197