:: by Wojciech A. Trybulec

::

:: Received August 30, 1989

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

Lm1: for Y being set holds

( ex X being set st

( X <> {} & X in Y ) iff union Y <> {} )

proof end;

definition

let M be non empty set ;

assume A1: not {} in M ;

ex b_{1} being Function of M,(union M) st

for X being set st X in M holds

b_{1} . X in X

end;
assume A1: not {} in M ;

mode Choice_Function of M -> Function of M,(union M) means :Def1: :: ORDERS_1:def 1

for X being set st X in M holds

it . X in X;

existence for X being set st X in M holds

it . X in X;

ex b

for X being set st X in M holds

b

proof end;

:: deftheorem Def1 defines Choice_Function ORDERS_1:def 1 :

for M being non empty set st not {} in M holds

for b_{2} being Function of M,(union M) holds

( b_{2} is Choice_Function of M iff for X being set st X in M holds

b_{2} . X in X );

for M being non empty set st not {} in M holds

for b

( b

b

registration
end;

definition
end;

Lm2: for X being set

for R being total Relation of X holds field R = X

proof end;

theorem :: ORDERS_1:4

for X, x, y being set

for O being Order of X st x in X & y in X & [x,y] in O & [y,x] in O holds

x = y

for O being Order of X st x in X & y in X & [x,y] in O & [y,x] in O holds

x = y

proof end;

theorem :: ORDERS_1:5

for X, x, y, z being set

for O being Order of X st x in X & y in X & z in X & [x,y] in O & [y,z] in O holds

[x,z] in O

for O being Order of X st x in X & y in X & z in X & [x,y] in O & [y,z] in O holds

[x,z] in O

proof end;

theorem :: ORDERS_1:6

theorem :: ORDERS_1:7

for X being set

for P being Relation holds

( P is_strongly_connected_in X iff ( P is_reflexive_in X & P is_connected_in X ) )

for P being Relation holds

( P is_strongly_connected_in X iff ( P is_reflexive_in X & P is_connected_in X ) )

proof end;

theorem Th9: :: ORDERS_1:9

for X, Y being set

for P being Relation st P is_antisymmetric_in X & Y c= X holds

P is_antisymmetric_in Y

for P being Relation st P is_antisymmetric_in X & Y c= X holds

P is_antisymmetric_in Y

proof end;

theorem :: ORDERS_1:11

for X, Y being set

for P being Relation st P is_strongly_connected_in X & Y c= X holds

P is_strongly_connected_in Y

for P being Relation st P is_strongly_connected_in X & Y c= X holds

P is_strongly_connected_in Y

proof end;

begin

::

:: Orders.

::

:: Orders.

::

definition

let R be Relation;

end;
attr R is being_partial-order means :Def4: :: ORDERS_1:def 4

( R is reflexive & R is transitive & R is antisymmetric );

( R is reflexive & R is transitive & R is antisymmetric );

attr R is being_linear-order means :Def5: :: ORDERS_1:def 5

( R is reflexive & R is transitive & R is antisymmetric & R is connected );

( R is reflexive & R is transitive & R is antisymmetric & R is connected );

:: deftheorem defines being_quasi-order ORDERS_1:def 3 :

for R being Relation holds

( R is being_quasi-order iff ( R is reflexive & R is transitive ) );

for R being Relation holds

( R is being_quasi-order iff ( R is reflexive & R is transitive ) );

:: deftheorem Def4 defines being_partial-order ORDERS_1:def 4 :

for R being Relation holds

( R is being_partial-order iff ( R is reflexive & R is transitive & R is antisymmetric ) );

for R being Relation holds

( R is being_partial-order iff ( R is reflexive & R is transitive & R is antisymmetric ) );

:: deftheorem Def5 defines being_linear-order ORDERS_1:def 5 :

for R being Relation holds

( R is being_linear-order iff ( R is reflexive & R is transitive & R is antisymmetric & R is connected ) );

for R being Relation holds

( R is being_linear-order iff ( R is reflexive & R is transitive & R is antisymmetric & R is connected ) );

Lm3: for R being Relation st R is connected holds

R ~ is connected

proof end;

theorem :: ORDERS_1:19

for R being Relation st R is well-ordering holds

( R is being_quasi-order & R is being_partial-order & R is being_linear-order )

( R is being_quasi-order & R is being_partial-order & R is being_linear-order )

proof end;

theorem :: ORDERS_1:20

for R being Relation st R is being_linear-order holds

( R is being_quasi-order & R is being_partial-order )

( R is being_quasi-order & R is being_partial-order )

proof end;

theorem :: ORDERS_1:22

theorem :: ORDERS_1:24

Lm4: for R being Relation holds R c= [:(field R),(field R):]

proof end;

Lm5: for R being Relation

for X being set st R is reflexive & X c= field R holds

field (R |_2 X) = X

proof end;

theorem :: ORDERS_1:26

for R being Relation

for X being set st R is being_partial-order holds

R |_2 X is being_partial-order

for X being set st R is being_partial-order holds

R |_2 X is being_partial-order

proof end;

registration

for b_{1} being Relation st b_{1} is empty holds

( b_{1} is being_quasi-order & b_{1} is being_partial-order & b_{1} is being_linear-order & b_{1} is well-ordering )
end;

cluster empty Relation-like -> well-ordering being_quasi-order being_partial-order being_linear-order for set ;

coherence for b

( b

proof end;

registration
end;

definition

let R be Relation;

let X be set ;

end;
let X be set ;

pred R partially_orders X means :Def7: :: ORDERS_1:def 7

( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X );

( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X );

pred R linearly_orders X means :: ORDERS_1:def 8

( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X & R is_connected_in X );

( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X & R is_connected_in X );

:: deftheorem Def6 defines quasi_orders ORDERS_1:def 6 :

for R being Relation

for X being set holds

( R quasi_orders X iff ( R is_reflexive_in X & R is_transitive_in X ) );

for R being Relation

for X being set holds

( R quasi_orders X iff ( R is_reflexive_in X & R is_transitive_in X ) );

:: deftheorem Def7 defines partially_orders ORDERS_1:def 7 :

for R being Relation

for X being set holds

( R partially_orders X iff ( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X ) );

for R being Relation

for X being set holds

( R partially_orders X iff ( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X ) );

:: deftheorem defines linearly_orders ORDERS_1:def 8 :

for R being Relation

for X being set holds

( R linearly_orders X iff ( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X & R is_connected_in X ) );

for R being Relation

for X being set holds

( R linearly_orders X iff ( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X & R is_connected_in X ) );

theorem Th28: :: ORDERS_1:28

for R being Relation

for X being set st R well_orders X holds

( R quasi_orders X & R partially_orders X & R linearly_orders X )

for X being set st R well_orders X holds

( R quasi_orders X & R partially_orders X & R linearly_orders X )

proof end;

theorem Th29: :: ORDERS_1:29

for R being Relation

for X being set st R linearly_orders X holds

( R quasi_orders X & R partially_orders X )

for X being set st R linearly_orders X holds

( R quasi_orders X & R partially_orders X )

proof end;

Lm6: for R being Relation

for X being set st R is_reflexive_in X holds

R |_2 X is reflexive

proof end;

Lm7: for R being Relation

for X being set st R is_transitive_in X holds

R |_2 X is transitive

proof end;

Lm8: for R being Relation

for X being set st R is_antisymmetric_in X holds

R |_2 X is antisymmetric

proof end;

Lm9: for R being Relation

for X being set st R is_connected_in X holds

R |_2 X is connected

proof end;

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

proof end;

Lm11: for R being Relation

for X being set st R is_reflexive_in X holds

R ~ is_reflexive_in X

proof end;

Lm12: for R being Relation

for X being set st R is_transitive_in X holds

R ~ is_transitive_in X

proof end;

Lm13: for R being Relation

for X being set st R is_antisymmetric_in X holds

R ~ is_antisymmetric_in X

proof end;

Lm14: for R being Relation

for X being set st R is_connected_in X holds

R ~ is_connected_in X

proof end;

theorem :: ORDERS_1:46

theorem :: ORDERS_1:47

definition

let R be Relation;

let X be set ;

end;
let X be set ;

pred X has_upper_Zorn_property_wrt R means :Def9: :: ORDERS_1:def 9

for Y being set st Y c= X & R |_2 Y is being_linear-order holds

ex x being set st

( x in X & ( for y being set st y in Y holds

[y,x] in R ) );

for Y being set st Y c= X & R |_2 Y is being_linear-order holds

ex x being set st

( x in X & ( for y being set st y in Y holds

[y,x] in R ) );

pred X has_lower_Zorn_property_wrt R means :: ORDERS_1:def 10

for Y being set st Y c= X & R |_2 Y is being_linear-order holds

ex x being set st

( x in X & ( for y being set st y in Y holds

[x,y] in R ) );

for Y being set st Y c= X & R |_2 Y is being_linear-order holds

ex x being set st

( x in X & ( for y being set st y in Y holds

[x,y] in R ) );

:: deftheorem Def9 defines has_upper_Zorn_property_wrt ORDERS_1:def 9 :

for R being Relation

for X being set holds

( X has_upper_Zorn_property_wrt R iff for Y being set st Y c= X & R |_2 Y is being_linear-order holds

ex x being set st

( x in X & ( for y being set st y in Y holds

[y,x] in R ) ) );

for R being Relation

for X being set holds

( X has_upper_Zorn_property_wrt R iff for Y being set st Y c= X & R |_2 Y is being_linear-order holds

ex x being set st

( x in X & ( for y being set st y in Y holds

[y,x] in R ) ) );

:: deftheorem defines has_lower_Zorn_property_wrt ORDERS_1:def 10 :

for R being Relation

for X being set holds

( X has_lower_Zorn_property_wrt R iff for Y being set st Y c= X & R |_2 Y is being_linear-order holds

ex x being set st

( x in X & ( for y being set st y in Y holds

[x,y] in R ) ) );

for R being Relation

for X being set holds

( X has_lower_Zorn_property_wrt R iff for Y being set st Y c= X & R |_2 Y is being_linear-order holds

ex x being set st

( x in X & ( for y being set st y in Y holds

[x,y] in R ) ) );

Lm15: for R being Relation

for X being set holds (R |_2 X) ~ = (R ~) |_2 X

proof end;

Lm16: now :: thesis: for R being Relation holds R |_2 {} = {}

let R be Relation; :: thesis: R |_2 {} = {}

thus R |_2 {} = ({} |` R) | {} by WELLORD1:10

.= {} ; :: thesis: verum

end;
thus R |_2 {} = ({} |` R) | {} by WELLORD1:10

.= {} ; :: thesis: verum

theorem Th51: :: ORDERS_1:51

for R being Relation

for X being set holds

( X has_upper_Zorn_property_wrt R iff X has_lower_Zorn_property_wrt R ~ )

for X being set holds

( X has_upper_Zorn_property_wrt R iff X has_lower_Zorn_property_wrt R ~ )

proof end;

theorem :: ORDERS_1:52

for R being Relation

for X being set holds

( X has_upper_Zorn_property_wrt R ~ iff X has_lower_Zorn_property_wrt R )

for X being set holds

( X has_upper_Zorn_property_wrt R ~ iff X has_lower_Zorn_property_wrt R )

proof end;

definition

let R be Relation;

let x be set ;

end;
let x be set ;

pred x is_maximal_in R means :Def11: :: ORDERS_1:def 11

( x in field R & ( for y being set holds

( not y in field R or not y <> x or not [x,y] in R ) ) );

( x in field R & ( for y being set holds

( not y in field R or not y <> x or not [x,y] in R ) ) );

pred x is_minimal_in R means :Def12: :: ORDERS_1:def 12

( x in field R & ( for y being set holds

( not y in field R or not y <> x or not [y,x] in R ) ) );

( x in field R & ( for y being set holds

( not y in field R or not y <> x or not [y,x] in R ) ) );

pred x is_superior_of R means :Def13: :: ORDERS_1:def 13

( x in field R & ( for y being set st y in field R & y <> x holds

[y,x] in R ) );

( x in field R & ( for y being set st y in field R & y <> x holds

[y,x] in R ) );

:: deftheorem Def11 defines is_maximal_in ORDERS_1:def 11 :

for R being Relation

for x being set holds

( x is_maximal_in R iff ( x in field R & ( for y being set holds

( not y in field R or not y <> x or not [x,y] in R ) ) ) );

for R being Relation

for x being set holds

( x is_maximal_in R iff ( x in field R & ( for y being set holds

( not y in field R or not y <> x or not [x,y] in R ) ) ) );

:: deftheorem Def12 defines is_minimal_in ORDERS_1:def 12 :

for R being Relation

for x being set holds

( x is_minimal_in R iff ( x in field R & ( for y being set holds

( not y in field R or not y <> x or not [y,x] in R ) ) ) );

for R being Relation

for x being set holds

( x is_minimal_in R iff ( x in field R & ( for y being set holds

( not y in field R or not y <> x or not [y,x] in R ) ) ) );

:: deftheorem Def13 defines is_superior_of ORDERS_1:def 13 :

for R being Relation

for x being set holds

( x is_superior_of R iff ( x in field R & ( for y being set st y in field R & y <> x holds

[y,x] in R ) ) );

for R being Relation

for x being set holds

( x is_superior_of R iff ( x in field R & ( for y being set st y in field R & y <> x holds

[y,x] in R ) ) );

:: deftheorem Def14 defines is_inferior_of ORDERS_1:def 14 :

for R being Relation

for x being set holds

( x is_inferior_of R iff ( x in field R & ( for y being set st y in field R & y <> x holds

[x,y] in R ) ) );

for R being Relation

for x being set holds

( x is_inferior_of R iff ( x in field R & ( for y being set st y in field R & y <> x holds

[x,y] in R ) ) );

theorem :: ORDERS_1:53

for R being Relation

for x being set st x is_inferior_of R & R is antisymmetric holds

x is_minimal_in R

for x being set st x is_inferior_of R & R is antisymmetric holds

x is_minimal_in R

proof end;

theorem :: ORDERS_1:54

for R being Relation

for x being set st x is_superior_of R & R is antisymmetric holds

x is_maximal_in R

for x being set st x is_superior_of R & R is antisymmetric holds

x is_maximal_in R

proof end;

theorem :: ORDERS_1:57

for R being Relation

for x, X being set st x in X & x is_superior_of R & X c= field R & R is reflexive holds

X has_upper_Zorn_property_wrt R

for x, X being set st x in X & x is_superior_of R & X c= field R & R is reflexive holds

X has_upper_Zorn_property_wrt R

proof end;

theorem :: ORDERS_1:58

for R being Relation

for x, X being set st x in X & x is_inferior_of R & X c= field R & R is reflexive holds

X has_lower_Zorn_property_wrt R

for x, X being set st x in X & x is_inferior_of R & X c= field R & R is reflexive holds

X has_lower_Zorn_property_wrt R

proof end;

Lm17: for R being Relation

for X, Y being set st R well_orders X & Y c= X holds

R well_orders Y

proof end;

theorem Th63: :: ORDERS_1:63

for R being Relation

for X being set st R partially_orders X & field R = X & X has_upper_Zorn_property_wrt R holds

ex x being set st x is_maximal_in R

for X being set st R partially_orders X & field R = X & X has_upper_Zorn_property_wrt R holds

ex x being set st x is_maximal_in R

proof end;

theorem Th64: :: ORDERS_1:64

for R being Relation

for X being set st R partially_orders X & field R = X & X has_lower_Zorn_property_wrt R holds

ex x being set st x is_minimal_in R

for X being set st R partially_orders X & field R = X & X has_lower_Zorn_property_wrt R holds

ex x being set st x is_minimal_in R

proof end;

theorem Th65: :: ORDERS_1:65

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 ) )

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 ) )

proof end;

theorem Th66: :: ORDERS_1:66

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 ) )

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 ) )

proof end;

theorem Th67: :: ORDERS_1:67

for X being set st X <> {} & ( for Z being set st Z <> {} & Z c= X & Z is c=-linear holds

union Z in X ) holds

ex Y being set st

( Y in X & ( for Z being set st Z in X & Z <> Y holds

not Y c= Z ) )

union Z in X ) holds

ex Y being set st

( Y in X & ( for Z being set st Z in X & Z <> Y holds

not Y c= Z ) )

proof end;

theorem :: ORDERS_1:68

for X being set st X <> {} & ( for Z being set st Z <> {} & Z c= X & Z is c=-linear holds

meet Z in X ) holds

ex Y being set st

( Y in X & ( for Z being set st Z in X & Z <> Y holds

not Z c= Y ) )

meet Z in X ) holds

ex Y being set st

( Y in X & ( for Z being set st Z in X & Z <> Y holds

not Z c= Y ) )

proof end;

scheme :: ORDERS_1:sch 1

ZornMax{ F_{1}() -> non empty set , P_{1}[ set , set ] } :

provided

ZornMax{ F

provided

A1:
for x being Element of F_{1}() holds P_{1}[x,x]
and

A2: for x, y being Element of F_{1}() st P_{1}[x,y] & P_{1}[y,x] holds

x = y and

A3: for x, y, z being Element of F_{1}() st P_{1}[x,y] & P_{1}[y,z] holds

P_{1}[x,z]
and

A4: for X being set st X c= F_{1}() & ( for x, y being Element of F_{1}() st x in X & y in X & P_{1}[x,y] holds

P_{1}[y,x] ) holds

ex y being Element of F_{1}() st

for x being Element of F_{1}() st x in X holds

P_{1}[x,y]

A2: for x, y being Element of F

x = y and

A3: for x, y, z being Element of F

P

A4: for X being set st X c= F

P

ex y being Element of F

for x being Element of F

P

proof end;

scheme :: ORDERS_1:sch 2

ZornMin{ F_{1}() -> non empty set , P_{1}[ set , set ] } :

provided

ZornMin{ F

provided

A1:
for x being Element of F_{1}() holds P_{1}[x,x]
and

A2: for x, y being Element of F_{1}() st P_{1}[x,y] & P_{1}[y,x] holds

x = y and

A3: for x, y, z being Element of F_{1}() st P_{1}[x,y] & P_{1}[y,z] holds

P_{1}[x,z]
and

A4: for X being set st X c= F_{1}() & ( for x, y being Element of F_{1}() st x in X & y in X & P_{1}[x,y] holds

P_{1}[y,x] ) holds

ex y being Element of F_{1}() st

for x being Element of F_{1}() st x in X holds

P_{1}[y,x]

A2: for x, y being Element of F

x = y and

A3: for x, y, z being Element of F

P

A4: for X being set st X c= F

P

ex y being Element of F

for x being Element of F

P

proof end;

::

:: Orders - continuation.

::

:: Orders - continuation.

::

theorem :: ORDERS_1:69

for R being Relation

for X being set st R partially_orders X & field R = X holds

ex P being Relation st

( R c= P & P linearly_orders X & field P = X )

for X being set st R partially_orders X & field R = X holds

ex P being Relation st

( R c= P & P linearly_orders X & field P = X )

proof end;

::

:: Auxiliary theorems.

::

:: Auxiliary theorems.

::

theorem :: ORDERS_1:71

theorem :: ORDERS_1:72

theorem :: ORDERS_1:73

theorem :: ORDERS_1:74

for R being Relation

for X being set st R is_antisymmetric_in X holds

R |_2 X is antisymmetric by Lm8;

for X being set st R is_antisymmetric_in X holds

R |_2 X is antisymmetric by Lm8;

theorem :: ORDERS_1:75

theorem :: ORDERS_1:76

for R being Relation

for X, Y being set st R is_connected_in X & Y c= X holds

R is_connected_in Y by Lm10;

for X, Y being set st R is_connected_in X & Y c= X holds

R is_connected_in Y by Lm10;

theorem :: ORDERS_1:77

theorem :: ORDERS_1:79

theorem :: ORDERS_1:80

theorem :: ORDERS_1:81

for R being Relation

for X being set st R is_antisymmetric_in X holds

R ~ is_antisymmetric_in X by Lm13;

for X being set st R is_antisymmetric_in X holds

R ~ is_antisymmetric_in X by Lm13;

theorem :: ORDERS_1:82

theorem :: ORDERS_1:83

begin

:: from COMPTS_1

theorem :: ORDERS_1:85

for f being Function

for Z being set st Z is finite & Z c= rng f holds

ex Y being set st

( Y c= dom f & Y is finite & f .: Y = Z )

for Z being set st Z is finite & Z c= rng f holds

ex Y being set st

( Y c= dom f & Y is finite & f .: Y = Z )

proof end;

:: from AMISTD_3, 2006.03.26, A.T.

:: from AMISTD_3, 2010.01.10, A.T

registration
end;

:: Orders.

::