:: ORDERS_2 semantic presentation

definition

attr c₁ is strict;
struct RelStr -> 1-sorted ;
aggr RelStr(# carrier, InternalRel #) -> RelStr ;
sel InternalRel c₁ -> Relation of the carrier of c₁;

end;

registration

let X be non empty set ;
let R be Relation of X;
cluster RelStr(# X,R #) -> non empty ;
coherence

proof end;

end;

definition

let A be RelStr ;
canceled;
canceled;
canceled;
attr A is reflexive means :Def4: :: ORDERS_2:def 4
the InternalRel of A is_reflexive_in the carrier of A;
attr A is transitive means :Def5: :: ORDERS_2:def 5
the InternalRel of A is_transitive_in the carrier of A;
attr A is antisymmetric means :Def6: :: ORDERS_2:def 6
the InternalRel of A is_antisymmetric_in the carrier of A;

end;

:: deftheorem ORDERS_2:def 1 :

:: deftheorem ORDERS_2:def 2 :

:: deftheorem ORDERS_2:def 3 :

:: deftheorem Def4 defines reflexive ORDERS_2:def 4 :

:: deftheorem Def5 defines transitive ORDERS_2:def 5 :

:: deftheorem Def6 defines antisymmetric ORDERS_2:def 6 :

registration

cluster non empty strict reflexive transitive antisymmetric RelStr ;
existence

proof end;

end;

definition

mode Poset is reflexive transitive antisymmetric RelStr ;

end;

registration

let A be Poset;
cluster the InternalRel of A -> reflexive antisymmetric transitive total ;
coherence

proof end;

end;

registration

let X be set ;
let O be Order of X;
cluster RelStr(# X,O #) -> reflexive transitive antisymmetric ;
coherence

proof end;

end;

Lm1: for x being set
for A being non empty Poset
for S being Subset of A st x in S holds
x is Element of A
;

definition

let A be RelStr ;
let a1, a2 be Element of A;
canceled;
canceled;
pred a1 <= a2 means :Def9: :: ORDERS_2:def 9
[a1,a2] in the InternalRel of A;

end;

:: deftheorem ORDERS_2:def 7 :

:: deftheorem ORDERS_2:def 8 :

:: deftheorem Def9 defines <= ORDERS_2:def 9 :

notation

let A be RelStr ;
let a1, a2 be Element of A;
synonym a2 >= a1 for a1 <= a2;

end;

definition

let A be RelStr ;
let a1, a2 be Element of A;
pred a1 < a2 means :Def10: :: ORDERS_2:def 10
( a1 <= a2 & a1 <> a2 );
irreflexivity ;

end;

:: deftheorem Def10 defines < ORDERS_2:def 10 :

notation

let A be RelStr ;
let a1, a2 be Element of A;
synonym a2 > a1 for a1 < a2;

end;

theorem :: ORDERS_2:1

canceled;

theorem :: ORDERS_2:2

canceled;

theorem :: ORDERS_2:3

canceled;

theorem :: ORDERS_2:4

canceled;

theorem :: ORDERS_2:5

canceled;

theorem :: ORDERS_2:6

canceled;

theorem :: ORDERS_2:7

canceled;

theorem :: ORDERS_2:8

canceled;

theorem :: ORDERS_2:9

canceled;

theorem :: ORDERS_2:10

canceled;

theorem :: ORDERS_2:11

canceled;

theorem :: ORDERS_2:12

canceled;

theorem :: ORDERS_2:13

canceled;

theorem :: ORDERS_2:14

canceled;

theorem :: ORDERS_2:15

canceled;

theorem :: ORDERS_2:16

canceled;

theorem :: ORDERS_2:17

canceled;

theorem :: ORDERS_2:18

canceled;

theorem :: ORDERS_2:19

canceled;

theorem :: ORDERS_2:20

canceled;

theorem :: ORDERS_2:21

canceled;

theorem :: ORDERS_2:22

canceled;

theorem :: ORDERS_2:23

canceled;

theorem Th24: :: ORDERS_2:24

for A being non empty reflexive RelStr
for a being Element of A holds a <= a

proof end;

definition

let A be non empty reflexive RelStr ;
let a1, a2 be Element of A;
:: original: <=
redefine pred a1 <= a2;
reflexivity by Th24;

end;

theorem Th25: :: ORDERS_2:25

for A being antisymmetric RelStr
for a1, a2 being Element of A st a1 <= a2 & a2 <= a1 holds
a1 = a2

proof end;

theorem Th26: :: ORDERS_2:26

for A being transitive RelStr
for a1, a2, a3 being Element of A st a1 <= a2 & a2 <= a3 holds
a1 <= a3

proof end;

theorem :: ORDERS_2:27

canceled;

theorem Th28: :: ORDERS_2:28

for A being antisymmetric RelStr
for a1, a2 being Element of A holds
( not a1 < a2 or not a2 < a1 )

proof end;

theorem Th29: :: ORDERS_2:29

for A being transitive antisymmetric RelStr
for a1, a2, a3 being Element of A st a1 < a2 & a2 < a3 holds
a1 < a3

proof end;

theorem Th30: :: ORDERS_2:30

for A being antisymmetric RelStr
for a1, a2 being Element of A st a1 <= a2 holds
not a2 < a1

proof end;

theorem :: ORDERS_2:31

canceled;

theorem Th32: :: ORDERS_2:32

for A being transitive antisymmetric RelStr
for a1, a2, a3 being Element of A st ( ( a1 < a2 & a2 <= a3 ) or ( a1 <= a2 & a2 < a3 ) ) holds
a1 < a3

proof end;

definition

let A be RelStr ;
let IT be Subset of A;
attr IT is strongly_connected means :Def11: :: ORDERS_2:def 11
the InternalRel of A is_strongly_connected_in IT;

end;

:: deftheorem Def11 defines strongly_connected ORDERS_2:def 11 :

registration

let A be RelStr ;
cluster {} A -> strongly_connected ;
coherence

proof end;

end;

registration

let A be RelStr ;
cluster strongly_connected Element of bool the carrier of A;
existence

proof end;

end;

definition

let A be RelStr ;
mode Chain of A is strongly_connected Subset of A;

end;

theorem :: ORDERS_2:33

canceled;

theorem :: ORDERS_2:34

canceled;

theorem Th35: :: ORDERS_2:35

for A being non empty reflexive RelStr
for a being Element of A holds {a} is Chain of A

proof end;

theorem Th36: :: ORDERS_2:36

for A being non empty reflexive RelStr
for a1, a2 being Element of A holds
( {a1,a2} is Chain of A iff ( a1 <= a2 or a2 <= a1 ) )

proof end;

theorem :: ORDERS_2:37

for A being RelStr
for C being Chain of A
for S being Subset of A st S c= C holds
S is Chain of A

proof end;

theorem Th38: :: ORDERS_2:38

for A being reflexive RelStr
for a1, a2 being Element of A holds
( ( a1 <= a2 or a2 <= a1 ) iff ex C being Chain of A st
( a1 in C & a2 in C ) )

proof end;

theorem Th39: :: ORDERS_2:39

for A being reflexive antisymmetric RelStr
for a1, a2 being Element of A holds
( ex C being Chain of A st
( a1 in C & a2 in C ) iff ( a1 < a2 iff not a2 <= a1 ) )

proof end;

theorem Th40: :: ORDERS_2:40

for A being RelStr
for T being Subset of A st the InternalRel of A well_orders T holds
T is Chain of A

proof end;

definition

let A be non empty Poset;
let S be Subset of A;
func UpperCone S -> Subset of A equals :: ORDERS_2:def 12
{ a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a2 < a1 } ;
coherence

proof end;

end;

:: deftheorem defines UpperCone ORDERS_2:def 12 :

definition

let A be non empty Poset;
let S be Subset of A;
func LowerCone S -> Subset of A equals :: ORDERS_2:def 13
{ a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a1 < a2 } ;
coherence

proof end;

end;

:: deftheorem defines LowerCone ORDERS_2:def 13 :

theorem :: ORDERS_2:41

canceled;

theorem :: ORDERS_2:42

canceled;

theorem Th43: :: ORDERS_2:43

for A being non empty Poset holds UpperCone ({} A) = the carrier of A

proof end;

theorem :: ORDERS_2:44

for A being non empty Poset holds UpperCone ([#] A) = {}

proof end;

theorem :: ORDERS_2:45

for A being non empty Poset holds LowerCone ({} A) = the carrier of A

proof end;

theorem :: ORDERS_2:46

for A being non empty Poset holds LowerCone ([#] A) = {}

proof end;

theorem Th47: :: ORDERS_2:47

for A being non empty Poset
for a being Element of A
for S being Subset of A st a in S holds
not a in UpperCone S

proof end;

theorem :: ORDERS_2:48

for A being non empty Poset
for a being Element of A holds not a in UpperCone {a}

proof end;

theorem Th49: :: ORDERS_2:49

for A being non empty Poset
for a being Element of A
for S being Subset of A st a in S holds
not a in LowerCone S

proof end;

theorem Th50: :: ORDERS_2:50

for A being non empty Poset
for a being Element of A holds not a in LowerCone {a}

proof end;

theorem :: ORDERS_2:51

for A being non empty Poset
for c, a being Element of A holds
( c < a iff a in UpperCone {c} )

proof end;

theorem Th52: :: ORDERS_2:52

for A being non empty Poset
for a, c being Element of A holds
( a < c iff a in LowerCone {c} )

proof end;

definition

let A be non empty Poset;
let S be Subset of A;
let a be Element of A;
func InitSegm S,a -> Subset of A equals :: ORDERS_2:def 14
(LowerCone {a}) /\ S;
correctness ;

end;

:: deftheorem defines InitSegm ORDERS_2:def 14 :

definition

let A be non empty Poset;
let S be Subset of A;
mode Initial_Segm of S -> Subset of A means :Def15: :: ORDERS_2:def 15
ex a being Element of A st
( a in S & it = InitSegm S,a ) if S <> {}
otherwise it = {} ;
existence

proof end;

consistency ;

end;

:: deftheorem Def15 defines Initial_Segm ORDERS_2:def 15 :

theorem :: ORDERS_2:53

canceled;

theorem :: ORDERS_2:54

canceled;

theorem :: ORDERS_2:55

canceled;

theorem Th56: :: ORDERS_2:56

for x being set
for A being non empty Poset
for a being Element of A
for S being Subset of A holds
( x in InitSegm S,a iff ( x in LowerCone {a} & x in S ) ) by XBOOLE_0:def 3;

theorem Th57: :: ORDERS_2:57

for A being non empty Poset
for a, b being Element of A
for S being Subset of A holds
( a in InitSegm S,b iff ( a < b & a in S ) )

proof end;

theorem :: ORDERS_2:58

canceled;

theorem :: ORDERS_2:59

canceled;

theorem :: ORDERS_2:60

for A being non empty Poset
for a being Element of A holds InitSegm ({} A),a = {} ;

theorem Th61: :: ORDERS_2:61

for A being non empty Poset
for a being Element of A
for S being Subset of A holds InitSegm S,a c= S by XBOOLE_1:17;

theorem Th62: :: ORDERS_2:62

for A being non empty Poset
for a being Element of A
for S being Subset of A holds not a in InitSegm S,a

proof end;

theorem :: ORDERS_2:63

canceled;

theorem :: ORDERS_2:64

for A being non empty Poset
for a1, a2 being Element of A
for S being Subset of A st a1 < a2 holds
InitSegm S,a1 c= InitSegm S,a2

proof end;

theorem Th65: :: ORDERS_2:65

for A being non empty Poset
for a being Element of A
for S, T being Subset of A st S c= T holds
InitSegm S,a c= InitSegm T,a

proof end;

theorem :: ORDERS_2:66

canceled;

theorem Th67: :: ORDERS_2:67

for A being non empty Poset
for S being Subset of A
for I being Initial_Segm of S holds I c= S

proof end;

theorem Th68: :: ORDERS_2:68

for A being non empty Poset
for S being Subset of A holds
( S <> {} iff not S is Initial_Segm of S )

proof end;

theorem Th69: :: ORDERS_2:69

for A being non empty Poset
for S, T being Subset of A st ( S <> {} or T <> {} ) & S is Initial_Segm of T holds
not T is Initial_Segm of S

proof end;

theorem Th70: :: ORDERS_2:70

for A being non empty Poset
for a1, a2 being Element of A
for S, T being Subset of A st a1 < a2 & a1 in S & a2 in T & T is Initial_Segm of S holds
a1 in T

proof end;

theorem Th71: :: ORDERS_2:71

for A being non empty Poset
for a being Element of A
for S, T being Subset of A st a in S & S is Initial_Segm of T holds
InitSegm S,a = InitSegm T,a

proof end;

theorem :: ORDERS_2:72

for A being non empty Poset
for S, T being Subset of A st S c= T & the InternalRel of A well_orders T & ( for a1, a2 being Element of A st a2 in S & a1 < a2 holds
a1 in S ) & not S = T holds
S is Initial_Segm of T

proof end;

theorem Th73: :: ORDERS_2:73

for A being non empty Poset
for S, T being Subset of A st S c= T & the InternalRel of A well_orders T & ( for a1, a2 being Element of A st a2 in S & a1 in T & a1 < a2 holds
a1 in S ) & not S = T holds
S is Initial_Segm of T

proof end;

definition

let A be non empty Poset;
let f be Choice_Function of BOOL the carrier of A;
mode Chain of f -> Chain of A means :Def16: :: ORDERS_2:def 16
( it <> {} & the InternalRel of A well_orders it & ( for a being Element of A st a in it holds
f . (UpperCone (InitSegm it,a)) = a ) );
existence

proof end;

end;

:: deftheorem Def16 defines Chain ORDERS_2:def 16 :

theorem :: ORDERS_2:74

canceled;

theorem :: ORDERS_2:75

canceled;

theorem :: ORDERS_2:76

canceled;

theorem :: ORDERS_2:77

canceled;

theorem Th78: :: ORDERS_2:78

for A being non empty Poset
for f being Choice_Function of BOOL the carrier of A holds {(f . the carrier of A)} is Chain of f

proof end;

theorem Th79: :: ORDERS_2:79

for A being non empty Poset
for f being Choice_Function of BOOL the carrier of A
for fC being Chain of f holds f . the carrier of A in fC

proof end;

theorem Th80: :: ORDERS_2:80

for A being non empty Poset
for a, b being Element of A
for f being Choice_Function of BOOL the carrier of A
for fC being Chain of f st a in fC & b = f . the carrier of A holds
b <= a

proof end;

theorem :: ORDERS_2:81

for A being non empty Poset
for a being Element of A
for f being Choice_Function of BOOL the carrier of A
for fC being Chain of f st a = f . the carrier of A holds
InitSegm fC,a = {}

proof end;

theorem :: ORDERS_2:82

for A being non empty Poset
for f being Choice_Function of BOOL the carrier of A
for fC1, fC2 being Chain of f holds fC1 meets fC2

proof end;

theorem Th83: :: ORDERS_2:83

for A being non empty Poset
for f being Choice_Function of BOOL the carrier of A
for fC1, fC2 being Chain of f st fC1 <> fC2 holds
( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 )

proof end;

theorem Th84: :: ORDERS_2:84

for A being non empty Poset
for f being Choice_Function of BOOL the carrier of A
for fC1, fC2 being Chain of f holds
( fC1 c< fC2 iff fC1 is Initial_Segm of fC2 )

proof end;

definition

let A be non empty Poset;
let f be Choice_Function of BOOL the carrier of A;
func Chains f -> set means :Def17: :: ORDERS_2:def 17
for x being set holds
( x in it iff x is Chain of f );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def17 defines Chains ORDERS_2:def 17 :

registration

let A be non empty Poset;
let f be Choice_Function of BOOL the carrier of A;
cluster Chains f -> non empty ;
coherence

proof end;

end;

Lm2: for A being non empty Poset
for f being Choice_Function of BOOL the carrier of A holds union (Chains f) is Subset of A

proof end;

Lm3: for A being non empty Poset
for f being Choice_Function of BOOL the carrier of A holds union (Chains f) is Chain of A

proof end;

theorem :: ORDERS_2:85

canceled;

theorem :: ORDERS_2:86

canceled;

theorem Th87: :: ORDERS_2:87

for A being non empty Poset
for f being Choice_Function of BOOL the carrier of A holds union (Chains f) <> {}

proof end;

theorem Th88: :: ORDERS_2:88

for A being non empty Poset
for S being Subset of A
for f being Choice_Function of BOOL the carrier of A
for fC being Chain of f st fC <> union (Chains f) & S = union (Chains f) holds
fC is Initial_Segm of S

proof end;

theorem Th89: :: ORDERS_2:89

for A being non empty Poset
for f being Choice_Function of BOOL the carrier of A holds union (Chains f) is Chain of f

proof end;

theorem :: ORDERS_2:90

canceled;

theorem :: ORDERS_2:91

canceled;

theorem :: ORDERS_2:92

canceled;

theorem :: ORDERS_2:93

canceled;

theorem :: ORDERS_2:94

canceled;

theorem :: ORDERS_2:95

canceled;

theorem :: ORDERS_2:96

canceled;

theorem :: ORDERS_2:97

canceled;

theorem :: ORDERS_2:98

canceled;

theorem :: ORDERS_2:99

canceled;

theorem :: ORDERS_2:100

canceled;

theorem :: ORDERS_2:101

canceled;

theorem :: ORDERS_2:102

canceled;

theorem :: ORDERS_2:103

canceled;

theorem :: ORDERS_2:104

canceled;

theorem :: ORDERS_2:105

canceled;

theorem :: ORDERS_2:106

canceled;

theorem Th107: :: ORDERS_2:107

for A being non empty Poset
for S being Subset of A holds field (the InternalRel of A |_2 S) = S

proof end;

theorem :: ORDERS_2:108

for A being non empty Poset
for S being Subset of A st the InternalRel of A |_2 S is_linear-order holds
S is Chain of A

proof end;

theorem :: ORDERS_2:109

for A being non empty Poset
for C being Chain of A holds the InternalRel of A |_2 C is_linear-order

proof end;

theorem :: ORDERS_2:110

canceled;

theorem :: ORDERS_2:111

canceled;

theorem :: ORDERS_2:112

canceled;

theorem :: ORDERS_2:113

canceled;

theorem :: ORDERS_2:114

canceled;

theorem :: ORDERS_2:115

canceled;

theorem :: ORDERS_2:116

canceled;

theorem :: ORDERS_2:117

canceled;

theorem :: ORDERS_2:118

canceled;

theorem :: ORDERS_2:119

canceled;

theorem :: ORDERS_2:120

canceled;

theorem :: ORDERS_2:121

canceled;

theorem :: ORDERS_2:122

canceled;

theorem :: ORDERS_2:123

canceled;

theorem :: ORDERS_2:124

canceled;

theorem :: ORDERS_2:125

canceled;

theorem :: ORDERS_2:126

canceled;

theorem :: ORDERS_2:127

canceled;

theorem :: ORDERS_2:128

canceled;

theorem :: ORDERS_2:129

canceled;

theorem :: ORDERS_2:130

canceled;

theorem :: ORDERS_2:131

canceled;

theorem :: ORDERS_2:132

canceled;

theorem :: ORDERS_2:133

canceled;

theorem :: ORDERS_2:134

canceled;

theorem :: ORDERS_2:135

for A being non empty Poset
for S being Subset of A st the InternalRel of A linearly_orders S holds
S is Chain of A

proof end;

theorem :: ORDERS_2:136

for A being non empty Poset
for C being Chain of A holds the InternalRel of A linearly_orders C

proof end;

theorem :: ORDERS_2:137

canceled;

theorem :: ORDERS_2:138

canceled;

theorem :: ORDERS_2:139

canceled;

theorem :: ORDERS_2:140

canceled;

theorem :: ORDERS_2:141

canceled;

theorem :: ORDERS_2:142

canceled;

theorem :: ORDERS_2:143

canceled;

theorem :: ORDERS_2:144

canceled;

theorem :: ORDERS_2:145

canceled;

theorem :: ORDERS_2:146

canceled;

theorem :: ORDERS_2:147

canceled;

theorem :: ORDERS_2:148

canceled;

theorem :: ORDERS_2:149

canceled;

theorem :: ORDERS_2:150

canceled;

theorem :: ORDERS_2:151

canceled;

theorem :: ORDERS_2:152

canceled;

theorem :: ORDERS_2:153

canceled;

theorem :: ORDERS_2:154

canceled;

theorem :: ORDERS_2:155

canceled;

theorem :: ORDERS_2:156

canceled;

theorem :: ORDERS_2:157

canceled;

theorem :: ORDERS_2:158

for A being non empty Poset
for a being Element of A holds
( a is_minimal_in the InternalRel of A iff for b being Element of A holds not b < a )

proof end;

theorem :: ORDERS_2:159

for A being non empty Poset
for a being Element of A holds
( a is_maximal_in the InternalRel of A iff for b being Element of A holds not a < b )

proof end;

theorem :: ORDERS_2:160

for A being non empty Poset
for a being Element of A holds
( a is_superior_of the InternalRel of A iff for b being Element of A st a <> b holds
b < a )

proof end;

theorem :: ORDERS_2:161

for A being non empty Poset
for a being Element of A holds
( a is_inferior_of the InternalRel of A iff for b being Element of A st a <> b holds
a < b )

proof end;

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

proof end;

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

proof end;

theorem Th162: :: ORDERS_2:162

for A being non empty Poset st ( for C being Chain of A ex a being Element of A st
for b being Element of A st b in C holds
b <= a ) holds
ex a being Element of A st
for b being Element of A holds not a < b

proof end;

theorem :: ORDERS_2:163

for A being non empty Poset st ( for C being Chain of A ex a being Element of A st
for b being Element of A st b in C holds
a <= b ) holds
ex a being Element of A st
for b being Element of A holds not b < a

proof end;