:: ORDERS_3 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let IT be RelStr ;
attr IT is discrete means :Def1: :: ORDERS_3:def 1
the InternalRel of IT = id the carrier of IT;
end;

:: deftheorem Def1 defines discrete ORDERS_3:def 1 :
for IT being RelStr holds
( IT is discrete iff the InternalRel of IT = id the carrier of IT );

registration
cluster non empty strict discrete RelStr ;
existence
ex b1 being Poset st
( b1 is strict & b1 is discrete & not b1 is empty )
proof end;
cluster empty strict discrete RelStr ;
existence
ex b1 being Poset st
( b1 is strict & b1 is discrete & b1 is empty )
proof end;
end;

Lm1: for P being empty RelStr holds the InternalRel of P = {}
proof end;

registration
cluster RelStr(# {} ,(id {} ) #) -> empty ;
coherence
RelStr(# {} ,(id {} ) #) is empty
by STRUCT_0:def 1;
let P be empty RelStr ;
cluster the InternalRel of P -> empty ;
coherence
the InternalRel of P is empty
by Lm1;
end;

Lm2: for P being RelStr st P is empty holds
P is discrete
proof end;

registration
cluster empty -> discrete RelStr ;
coherence
for b1 being RelStr st b1 is empty holds
b1 is discrete
by Lm2;
end;

definition
let P be RelStr ;
let IT be Subset of P;
attr IT is disconnected means :Def2: :: ORDERS_3:def 2
ex A, B being Subset of P st
( A <> {} & B <> {} & IT = A \/ B & A misses B & the InternalRel of P = (the InternalRel of P |_2 A) \/ (the InternalRel of P |_2 B) );
end;

:: deftheorem Def2 defines disconnected ORDERS_3:def 2 :
for P being RelStr
for IT being Subset of P holds
( IT is disconnected iff ex A, B being Subset of P st
( A <> {} & B <> {} & IT = A \/ B & A misses B & the InternalRel of P = (the InternalRel of P |_2 A) \/ (the InternalRel of P |_2 B) ) );

notation
let P be RelStr ;
let IT be Subset of P;
antonym connected IT for disconnected IT;
end;

definition
let IT be RelStr ;
attr IT is disconnected means :Def3: :: ORDERS_3:def 3
[#] IT is disconnected;
end;

:: deftheorem Def3 defines disconnected ORDERS_3:def 3 :
for IT being RelStr holds
( IT is disconnected iff [#] IT is disconnected );

notation
let IT be RelStr ;
antonym connected IT for disconnected IT;
end;

theorem :: ORDERS_3:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for DP being non empty discrete RelStr
for x, y being Element of DP holds
( x <= y iff x = y )
proof end;

theorem :: ORDERS_3:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Relation
for a being set st R is Order of {a} holds
R = id {a}
proof end;

theorem :: ORDERS_3:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty RelStr
for a being Element of T st T is reflexive & [#] T = {a} holds
T is discrete
proof end;

theorem Th4: :: ORDERS_3:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty RelStr
for a being set st [#] T = {a} holds
not T is disconnected
proof end;

theorem Th5: :: ORDERS_3:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for DP being non empty discrete Poset st ex a, b being Element of DP st a <> b holds
DP is disconnected
proof end;

registration
cluster non empty strict connected RelStr ;
existence
ex b1 being non empty Poset st
( b1 is strict & not b1 is disconnected )
proof end;
cluster non empty strict discrete disconnected RelStr ;
existence
ex b1 being non empty Poset st
( b1 is strict & b1 is disconnected & b1 is discrete )
proof end;
end;

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

:: deftheorem Def4 defines POSet_set-like ORDERS_3:def 4 :
for IT being set holds
( IT is POSet_set-like iff for a being set st a in IT holds
a is non empty Poset );

registration
cluster non empty POSet_set-like set ;
existence
ex b1 being set st
( not b1 is empty & b1 is POSet_set-like )
proof end;
end;

definition
mode POSet_set is POSet_set-like set ;
end;

definition
let P be non empty POSet_set;
:: original: Element
redefine mode Element of P -> non empty Poset;
coherence
for b1 being Element of P holds b1 is non empty Poset
by Def4;
end;

definition
let L1, L2 be RelStr ;
let f be Function of L1,L2;
attr f is monotone means :Def5: :: ORDERS_3:def 5
for x, y being Element of L1 st x <= y holds
for a, b being Element of L2 st a = f . x & b = f . y holds
a <= b;
end;

:: deftheorem Def5 defines monotone ORDERS_3:def 5 :
for L1, L2 being RelStr
for f being Function of L1,L2 holds
( f is monotone iff for x, y being Element of L1 st x <= y holds
for a, b being Element of L2 st a = f . x & b = f . y holds
a <= b );

Lm3: for A, B, C being non empty RelStr
for f being Function of A,B
for g being Function of B,C st f is monotone & g is monotone holds
ex gf being Function of A,C st
( gf = g * f & gf is monotone )
proof end;

Lm4: for T being non empty RelStr holds id T is monotone
proof end;

definition
let A, B be RelStr ;
func MonFuncs A,B -> set means :Def6: :: ORDERS_3:def 6
for a being set holds
( a in it iff ex f being Function of A,B st
( a = f & f in Funcs the carrier of A,the carrier of B & f is monotone ) );
existence
ex b1 being set st
for a being set holds
( a in b1 iff ex f being Function of A,B st
( a = f & f in Funcs the carrier of A,the carrier of B & f is monotone ) )
proof end;
uniqueness
for b1, b2 being set st ( for a being set holds
( a in b1 iff ex f being Function of A,B st
( a = f & f in Funcs the carrier of A,the carrier of B & f is monotone ) ) ) & ( for a being set holds
( a in b2 iff ex f being Function of A,B st
( a = f & f in Funcs the carrier of A,the carrier of B & f is monotone ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines MonFuncs ORDERS_3:def 6 :
for A, B being RelStr
for b3 being set holds
( b3 = MonFuncs A,B iff for a being set holds
( a in b3 iff ex f being Function of A,B st
( a = f & f in Funcs the carrier of A,the carrier of B & f is monotone ) ) );

theorem Th6: :: ORDERS_3:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being non empty RelStr
for f, g being Function st f in MonFuncs A,B & g in MonFuncs B,C holds
g * f in MonFuncs A,C
proof end;

theorem Th7: :: ORDERS_3:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty RelStr holds id the carrier of T in MonFuncs T,T
proof end;

registration
let T be non empty RelStr ;
cluster MonFuncs T,T -> non empty ;
coherence
not MonFuncs T,T is empty
by Th7;
end;

definition
let X be set ;
func Carr X -> set means :Def7: :: ORDERS_3:def 7
for a being set holds
( a in it iff ex s being 1-sorted st
( s in X & a = the carrier of s ) );
existence
ex b1 being set st
for a being set holds
( a in b1 iff ex s being 1-sorted st
( s in X & a = the carrier of s ) )
proof end;
uniqueness
for b1, b2 being set st ( for a being set holds
( a in b1 iff ex s being 1-sorted st
( s in X & a = the carrier of s ) ) ) & ( for a being set holds
( a in b2 iff ex s being 1-sorted st
( s in X & a = the carrier of s ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines Carr ORDERS_3:def 7 :
for X, b2 being set holds
( b2 = Carr X iff for a being set holds
( a in b2 iff ex s being 1-sorted st
( s in X & a = the carrier of s ) ) );

Lm5: for P being non empty POSet_set
for A being Element of P holds the carrier of A in Carr P
by Def7;

registration
let P be non empty POSet_set;
cluster Carr P -> non empty ;
coherence
not Carr P is empty
by Lm5;
end;

theorem :: ORDERS_3:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being 1-sorted holds Carr {f} = {the carrier of f}
proof end;

theorem :: ORDERS_3:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being 1-sorted holds Carr {f,g} = {the carrier of f,the carrier of g}
proof end;

theorem Th10: :: ORDERS_3:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty POSet_set
for A, B being Element of P holds MonFuncs A,B c= Funcs (Carr P)
proof end;

theorem Th11: :: ORDERS_3:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being RelStr holds MonFuncs A,B c= Funcs the carrier of A,the carrier of B
proof end;

registration
let A, B be non empty Poset;
cluster MonFuncs A,B -> functional ;
coherence
MonFuncs A,B is functional
proof end;
end;

definition
let P be non empty POSet_set;
func POSCat P -> strict with_triple-like_morphisms Category means :: ORDERS_3:def 8
( the Objects of it = P & ( for a, b being Element of P
for f being Element of Funcs (Carr P) st f in MonFuncs a,b holds
[[a,b],f] is Morphism of it ) & ( for m being Morphism of it ex a, b being Element of P ex f being Element of Funcs (Carr P) st
( m = [[a,b],f] & f in MonFuncs a,b ) ) & ( for m1, m2 being Morphism of it
for a1, a2, a3 being Element of P
for f1, f2 being Element of Funcs (Carr P) st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 * m1 = [[a1,a3],(f2 * f1)] ) );
existence
ex b1 being strict with_triple-like_morphisms Category st
( the Objects of b1 = P & ( for a, b being Element of P
for f being Element of Funcs (Carr P) st f in MonFuncs a,b holds
[[a,b],f] is Morphism of b1 ) & ( for m being Morphism of b1 ex a, b being Element of P ex f being Element of Funcs (Carr P) st
( m = [[a,b],f] & f in MonFuncs a,b ) ) & ( for m1, m2 being Morphism of b1
for a1, a2, a3 being Element of P
for f1, f2 being Element of Funcs (Carr P) st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 * m1 = [[a1,a3],(f2 * f1)] ) )
proof end;
uniqueness
for b1, b2 being strict with_triple-like_morphisms Category st the Objects of b1 = P & ( for a, b being Element of P
for f being Element of Funcs (Carr P) st f in MonFuncs a,b holds
[[a,b],f] is Morphism of b1 ) & ( for m being Morphism of b1 ex a, b being Element of P ex f being Element of Funcs (Carr P) st
( m = [[a,b],f] & f in MonFuncs a,b ) ) & ( for m1, m2 being Morphism of b1
for a1, a2, a3 being Element of P
for f1, f2 being Element of Funcs (Carr P) st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 * m1 = [[a1,a3],(f2 * f1)] ) & the Objects of b2 = P & ( for a, b being Element of P
for f being Element of Funcs (Carr P) st f in MonFuncs a,b holds
[[a,b],f] is Morphism of b2 ) & ( for m being Morphism of b2 ex a, b being Element of P ex f being Element of Funcs (Carr P) st
( m = [[a,b],f] & f in MonFuncs a,b ) ) & ( for m1, m2 being Morphism of b2
for a1, a2, a3 being Element of P
for f1, f2 being Element of Funcs (Carr P) st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 * m1 = [[a1,a3],(f2 * f1)] ) holds
b1 = b2
proof end;
end;

:: deftheorem defines POSCat ORDERS_3:def 8 :
for P being non empty POSet_set
for b2 being strict with_triple-like_morphisms Category holds
( b2 = POSCat P iff ( the Objects of b2 = P & ( for a, b being Element of P
for f being Element of Funcs (Carr P) st f in MonFuncs a,b holds
[[a,b],f] is Morphism of b2 ) & ( for m being Morphism of b2 ex a, b being Element of P ex f being Element of Funcs (Carr P) st
( m = [[a,b],f] & f in MonFuncs a,b ) ) & ( for m1, m2 being Morphism of b2
for a1, a2, a3 being Element of P
for f1, f2 being Element of Funcs (Carr P) st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 * m1 = [[a1,a3],(f2 * f1)] ) ) );

scheme :: ORDERS_3:sch 1
AltCatEx{ F1() -> non empty set , F2( set , set ) -> functional set } :
ex C being strict AltCatStr st
( the carrier of C = F1() & ( for i, j being Element of F1() holds
( the Arrows of C . i,j = F2(i,j) & ( for i, j, k being Element of F1() holds the Comp of C . i,j,k = FuncComp F2(i,j),F2(j,k) ) ) ) )
provided
A1: for i, j, k being Element of F1()
for f, g being Function st f in F2(i,j) & g in F2(j,k) holds
g * f in F2(i,k)
proof end;

scheme :: ORDERS_3:sch 2
AltCatUniq{ F1() -> non empty set , F2( set , set ) -> functional set } :
for C1, C2 being strict AltCatStr st the carrier of C1 = F1() & ( for i, j being Element of F1() holds
( the Arrows of C1 . i,j = F2(i,j) & ( for i, j, k being Element of F1() holds the Comp of C1 . i,j,k = FuncComp F2(i,j),F2(j,k) ) ) ) & the carrier of C2 = F1() & ( for i, j being Element of F1() holds
( the Arrows of C2 . i,j = F2(i,j) & ( for i, j, k being Element of F1() holds the Comp of C2 . i,j,k = FuncComp F2(i,j),F2(j,k) ) ) ) holds
C1 = C2
proof end;

definition
let P be non empty POSet_set;
func POSAltCat P -> strict AltCatStr means :Def9: :: ORDERS_3:def 9
( the carrier of it = P & ( for i, j being Element of P holds
( the Arrows of it . i,j = MonFuncs i,j & ( for i, j, k being Element of P holds the Comp of it . i,j,k = FuncComp (MonFuncs i,j),(MonFuncs j,k) ) ) ) );
existence
ex b1 being strict AltCatStr st
( the carrier of b1 = P & ( for i, j being Element of P holds
( the Arrows of b1 . i,j = MonFuncs i,j & ( for i, j, k being Element of P holds the Comp of b1 . i,j,k = FuncComp (MonFuncs i,j),(MonFuncs j,k) ) ) ) )
proof end;
uniqueness
for b1, b2 being strict AltCatStr st the carrier of b1 = P & ( for i, j being Element of P holds
( the Arrows of b1 . i,j = MonFuncs i,j & ( for i, j, k being Element of P holds the Comp of b1 . i,j,k = FuncComp (MonFuncs i,j),(MonFuncs j,k) ) ) ) & the carrier of b2 = P & ( for i, j being Element of P holds
( the Arrows of b2 . i,j = MonFuncs i,j & ( for i, j, k being Element of P holds the Comp of b2 . i,j,k = FuncComp (MonFuncs i,j),(MonFuncs j,k) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines POSAltCat ORDERS_3:def 9 :
for P being non empty POSet_set
for b2 being strict AltCatStr holds
( b2 = POSAltCat P iff ( the carrier of b2 = P & ( for i, j being Element of P holds
( the Arrows of b2 . i,j = MonFuncs i,j & ( for i, j, k being Element of P holds the Comp of b2 . i,j,k = FuncComp (MonFuncs i,j),(MonFuncs j,k) ) ) ) ) );

registration
let P be non empty POSet_set;
cluster POSAltCat P -> non empty transitive strict ;
coherence
( POSAltCat P is transitive & not POSAltCat P is empty )
proof end;
end;

registration
let P be non empty POSet_set;
cluster POSAltCat P -> non empty transitive strict associative with_units ;
coherence
( POSAltCat P is associative & POSAltCat P is with_units )
proof end;
end;

theorem :: ORDERS_3:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty POSet_set
for o1, o2 being object of (POSAltCat P)
for A, B being Element of P st o1 = A & o2 = B holds
<^o1,o2^> c= Funcs the carrier of A,the carrier of B
proof end;