:: ORDERS_3 semantic presentation

definition

let c₁ be RelStr ;
attr a₁ is discrete means :Def1: :: ORDERS_3:def 1
the InternalRel of a₁ = id the carrier of a₁;

end;

:: deftheorem Def1 defines discrete ORDERS_3:def 1 :

registration

cluster non empty strict discrete RelStr ;
existence

proof end;

cluster empty strict discrete RelStr ;
existence

proof end;

end;

Lemma2: for b₁ being empty RelStr holds the InternalRel of b₁ = {}

proof end;

registration

cluster RelStr(# {} ,(id {} ) #) -> empty ;
coherence by STRUCT_0:def 1;
let c₁ be empty RelStr ;
cluster the InternalRel of a₁ -> empty ;
coherence by Lemma2;

end;

Lemma3: for b₁ being RelStr st b₁ is empty holds
b₁ is discrete

proof end;

registration

cluster empty -> discrete RelStr ;
coherence by Lemma3;

end;

definition

let c₁ be RelStr ;
let c₂ be Subset of c₁;
attr a₂ is disconnected means :Def2: :: ORDERS_3:def 2
ex b₁, b₂ being Subset of a₁ st
( b₁ <> {} & b₂ <> {} & a₂ = b₁ \/ b₂ & b₁ misses b₂ & the InternalRel of a₁ = (the InternalRel of a₁ |_2 b₁) \/ (the InternalRel of a₁ |_2 b₂) );

end;

:: deftheorem Def2 defines disconnected ORDERS_3:def 2 :

notation

let c₁ be RelStr ;
let c₂ be Subset of c₁;
antonym connected c₂ for disconnected c₂;

end;

definition

let c₁ be RelStr ;
attr a₁ is disconnected means :Def3: :: ORDERS_3:def 3
[#] a₁ is disconnected;

end;

:: deftheorem Def3 defines disconnected ORDERS_3:def 3 :

notation

let c₁ be RelStr ;
antonym connected c₁ for disconnected c₁;

end;

theorem Th1: :: ORDERS_3:1

for b₁ being non empty discrete RelStr
for b₂, b₃ being Element of b₁ holds
( b₂ <= b₃ iff b₂ = b₃ )

proof end;

theorem Th2: :: ORDERS_3:2

for b₁ being Relation
for b₂ being set st b₁ is Order of {b₂} holds
b₁ = id {b₂}

proof end;

theorem Th3: :: ORDERS_3:3

for b₁ being non empty RelStr
for b₂ being Element of b₁ st b₁ is reflexive & [#] b₁ = {b₂} holds
b₁ is discrete

proof end;

theorem Th4: :: ORDERS_3:4

for b₁ being non empty RelStr
for b₂ being set st [#] b₁ = {b₂} holds
not b₁ is disconnected

proof end;

theorem Th5: :: ORDERS_3:5

for b₁ being non empty discrete Poset st ex b₂, b₃ being Element of b₁ st b₂ <> b₃ holds
b₁ is disconnected

proof end;

registration

cluster non empty strict connected RelStr ;
existence

proof end;

cluster non empty strict discrete disconnected RelStr ;
existence

proof end;

end;

definition

let c₁ be set ;
attr a₁ is POSet_set-like means :Def4: :: ORDERS_3:def 4
for b₁ being set st b₁ in a₁ holds
b₁ is non empty Poset;

end;

:: deftheorem Def4 defines POSet_set-like ORDERS_3:def 4 :

registration

cluster non empty POSet_set-like set ;
existence

proof end;

end;

definition

mode POSet_set is POSet_set-like set ;

end;

definition

let c₁ be non empty POSet_set;
redefine mode Element as Element of c₁ -> non empty Poset;
coherence by Def4;

end;

definition

let c₁, c₂ be RelStr ;
let c₃ be Function of c₁,c₂;
attr a₃ is monotone means :Def5: :: ORDERS_3:def 5
for b₁, b₂ being Element of a₁ st b₁ <= b₂ holds
for b₃, b₄ being Element of a₂ st b₃ = a₃ . b₁ & b₄ = a₃ . b₂ holds
b₃ <= b₄;

end;

:: deftheorem Def5 defines monotone ORDERS_3:def 5 :

Lemma10: for b₁, b₂, b₃ being non empty RelStr
for b₄ being Function of b₁,b₂
for b₅ being Function of b₂,b₃ st b₄ is monotone & b₅ is monotone holds
ex b₆ being Function of b₁,b₃ st
( b₆ = b₅ * b₄ & b₆ is monotone )

proof end;

Lemma11: for b₁ being non empty RelStr holds id b₁ is monotone

proof end;

definition

let c₁, c₂ be RelStr ;
func MonFuncs c₁,c₂ -> set means :Def6: :: ORDERS_3:def 6
for b₁ being set holds
( b₁ in a₃ iff ex b₂ being Function of a₁,a₂ st
( b₁ = b₂ & b₂ in Funcs the carrier of a₁,the carrier of a₂ & b₂ is monotone ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines MonFuncs ORDERS_3:def 6 :

theorem Th6: :: ORDERS_3:6

for b₁, b₂, b₃ being non empty RelStr
for b₄, b₅ being Function st b₄ in MonFuncs b₁,b₂ & b₅ in MonFuncs b₂,b₃ holds
b₅ * b₄ in MonFuncs b₁,b₃

proof end;

theorem Th7: :: ORDERS_3:7

for b₁ being non empty RelStr holds id the carrier of b₁ in MonFuncs b₁,b₁

proof end;

registration

let c₁ be non empty RelStr ;
cluster MonFuncs a₁,a₁ -> non empty ;
coherence by Th7;

end;

definition

let c₁ be set ;
func Carr c₁ -> set means :Def7: :: ORDERS_3:def 7
for b₁ being set holds
( b₁ in a₂ iff ex b₂ being 1-sorted st
( b₂ in a₁ & b₁ = the carrier of b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines Carr ORDERS_3:def 7 :

Lemma16: for b₁ being non empty POSet_set
for b₂ being Element of b₁ holds the carrier of b₂ in Carr b₁
by Def7;

registration

let c₁ be non empty POSet_set;
cluster Carr a₁ -> non empty ;
coherence by Lemma16;

end;

theorem Th8: :: ORDERS_3:8

for b₁ being 1-sorted holds Carr {b₁} = {the carrier of b₁}

proof end;

theorem Th9: :: ORDERS_3:9

for b₁, b₂ being 1-sorted holds Carr {b₁,b₂} = {the carrier of b₁,the carrier of b₂}

proof end;

theorem Th10: :: ORDERS_3:10

for b₁ being non empty POSet_set
for b₂, b₃ being Element of b₁ holds MonFuncs b₂,b₃ c= Funcs (Carr b₁)

proof end;

theorem Th11: :: ORDERS_3:11

for b₁, b₂ being RelStr holds MonFuncs b₁,b₂ c= Funcs the carrier of b₁,the carrier of b₂

proof end;

registration

let c₁, c₂ be non empty Poset;
cluster MonFuncs a₁,a₂ -> functional ;
coherence

proof end;

end;

definition

let c₁ be non empty POSet_set;
func POSCat c₁ -> strict with_triple-like_morphisms Category means :: ORDERS_3:def 8
( the Objects of a₂ = a₁ & ( for b₁, b₂ being Element of a₁
for b₃ being Element of Funcs (Carr a₁) st b₃ in MonFuncs b₁,b₂ holds
[[b₁,b₂],b₃] is Morphism of a₂ ) & ( for b₁ being Morphism of a₂ ex b₂, b₃ being Element of a₁ex b₄ being Element of Funcs (Carr a₁) st
( b₁ = [[b₂,b₃],b₄] & b₄ in MonFuncs b₂,b₃ ) ) & ( for b₁, b₂ being Morphism of a₂
for b₃, b₄, b₅ being Element of a₁
for b₆, b₇ being Element of Funcs (Carr a₁) st b₁ = [[b₃,b₄],b₆] & b₂ = [[b₄,b₅],b₇] holds
b₂ * b₁ = [[b₃,b₅],(b₇ * b₆)] ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines POSCat ORDERS_3:def 8 :

scheme :: ORDERS_3:sch 1
s1{ F₁() -> non empty set , F₂( set , set ) -> functional set } :

ex b₁ being strict AltCatStr st
( the carrier of b₁ = F₁() & ( for b₂, b₃ being Element of F₁() holds
( the Arrows of b₁ . b₂,b₃ = F₂(b₂,b₃) & ( for b₄, b₅, b₆ being Element of F₁() holds the Comp of b₁ . b₄,b₅,b₆ = FuncComp F₂(b₄,b₅),F₂(b₅,b₆) ) ) ) )

provided

E19: for b₁, b₂, b₃ being Element of F₁()
for b₄, b₅ being Function st b₄ in F₂(b₁,b₂) & b₅ in F₂(b₂,b₃) holds
b₅ * b₄ in F₂(b₁,b₃)

proof end;

scheme :: ORDERS_3:sch 2
s2{ F₁() -> non empty set , F₂( set , set ) -> functional set } :

for b₁, b₂ being strict AltCatStr st the carrier of b₁ = F₁() & ( for b₃, b₄ being Element of F₁() holds
( the Arrows of b₁ . b₃,b₄ = F₂(b₃,b₄) & ( for b₅, b₆, b₇ being Element of F₁() holds the Comp of b₁ . b₅,b₆,b₇ = FuncComp F₂(b₅,b₆),F₂(b₆,b₇) ) ) ) & the carrier of b₂ = F₁() & ( for b₃, b₄ being Element of F₁() holds
( the Arrows of b₂ . b₃,b₄ = F₂(b₃,b₄) & ( for b₅, b₆, b₇ being Element of F₁() holds the Comp of b₂ . b₅,b₆,b₇ = FuncComp F₂(b₅,b₆),F₂(b₆,b₇) ) ) ) holds
b₁ = b₂

proof end;

definition

let c₁ be non empty POSet_set;
func POSAltCat c₁ -> strict AltCatStr means :Def9: :: ORDERS_3:def 9
( the carrier of a₂ = a₁ & ( for b₁, b₂ being Element of a₁ holds
( the Arrows of a₂ . b₁,b₂ = MonFuncs b₁,b₂ & ( for b₃, b₄, b₅ being Element of a₁ holds the Comp of a₂ . b₃,b₄,b₅ = FuncComp (MonFuncs b₃,b₄),(MonFuncs b₄,b₅) ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines POSAltCat ORDERS_3:def 9 :

registration

let c₁ be non empty POSet_set;
cluster POSAltCat a₁ -> non empty transitive strict ;
coherence

proof end;

end;

registration

let c₁ be non empty POSet_set;
cluster POSAltCat a₁ -> non empty transitive strict associative with_units ;
coherence

proof end;

end;

theorem Th12: :: ORDERS_3:12

for b₁ being non empty POSet_set
for b₂, b₃ being object of (POSAltCat b₁)
for b₄, b₅ being Element of b₁ st b₂ = b₄ & b₃ = b₅ holds
<^b₂,b₃^> c= Funcs the carrier of b₄,the carrier of b₅

proof end;