:: by Adam Grabowski

::

:: Received January 22, 1996

:: Copyright (c) 1996-2021 Association of Mizar Users

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

for IT being RelStr holds

( IT is discrete iff the InternalRel of IT = id the carrier of IT );

registration

existence

ex b_{1} being Poset st

( b_{1} is strict & b_{1} is discrete & not b_{1} is empty )

end;
ex b

( b

proof end;

registration

coherence

RelStr(# {},(id {}) #) is empty ;

let P be empty RelStr ;

coherence

the InternalRel of P is empty ;

end;
RelStr(# {},(id {}) #) is empty ;

let P be empty RelStr ;

coherence

the InternalRel of P is empty ;

definition

let P be RelStr ;

let IT be Subset of P;

end;
let IT be Subset of P;

attr IT is disconnected means :: 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) );

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

:: deftheorem 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) ) );

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

definition
end;

:: deftheorem defines disconnected ORDERS_3:def 3 :

for IT being RelStr holds

( IT is disconnected iff [#] IT is disconnected );

for IT being RelStr holds

( IT is disconnected iff [#] IT is disconnected );

theorem :: ORDERS_3:3

for T being non empty RelStr

for a being Element of T st T is reflexive & [#] T = {a} holds

T is discrete

for a being Element of T st T is reflexive & [#] T = {a} holds

T is discrete

proof end;

theorem Th5: :: ORDERS_3:5

for DP being non empty discrete Poset st ex a, b being Element of DP st a <> b holds

DP is disconnected

DP is disconnected

proof end;

registration

existence

ex b_{1} being non empty Poset st

( b_{1} is strict & b_{1} is connected )

ex b_{1} being non empty Poset st

( b_{1} is strict & b_{1} is disconnected & b_{1} is discrete )

end;
ex b

( b

proof end;

cluster non empty strict V68() reflexive transitive antisymmetric discrete disconnected for RelStr ;

existence ex b

( b

proof end;

definition

let IT be set ;

end;
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;

for a being set st a in IT holds

a is non empty Poset;

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

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
end;

definition

let P be non empty POSet_set;

:: original: Element

redefine mode Element of P -> non empty Poset;

coherence

for b_{1} being Element of P holds b_{1} is non empty Poset
by Def4;

end;
:: original: Element

redefine mode Element of P -> non empty Poset;

coherence

for b

:: deftheorem 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 );

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

Lm1: 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;

definition

let A, B be RelStr ;

ex b_{1} being set st

for a being set holds

( a in b_{1} 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 b_{1}, b_{2} being set st ( for a being set holds

( a in b_{1} 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 b_{2} 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

b_{1} = b_{2}

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

ex b

for a being set holds

( a in b

( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) )

proof end;

uniqueness for b

( a in b

( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) ) ) & ( for a being set holds

( a in b

( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) ) ) holds

b

proof end;

:: deftheorem Def6 defines MonFuncs ORDERS_3:def 6 :

for A, B being RelStr

for b_{3} being set holds

( b_{3} = MonFuncs (A,B) iff for a being set holds

( a in b_{3} 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, B being RelStr

for b

( b

( a in b

( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) ) );

theorem Th6: :: ORDERS_3:6

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)

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;

definition

let X be set ;

ex b_{1} being set st

for a being set holds

( a in b_{1} iff ex s being 1-sorted st

( s in X & a = the carrier of s ) )

for b_{1}, b_{2} being set st ( for a being set holds

( a in b_{1} iff ex s being 1-sorted st

( s in X & a = the carrier of s ) ) ) & ( for a being set holds

( a in b_{2} iff ex s being 1-sorted st

( s in X & a = the carrier of s ) ) ) holds

b_{1} = b_{2}

end;
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 for a being set holds

( a in it iff ex s being 1-sorted st

( s in X & a = the carrier of s ) );

ex b

for a being set holds

( a in b

( s in X & a = the carrier of s ) )

proof end;

uniqueness for b

( a in b

( s in X & a = the carrier of s ) ) ) & ( for a being set holds

( a in b

( s in X & a = the carrier of s ) ) ) holds

b

proof end;

:: deftheorem Def7 defines Carr ORDERS_3:def 7 :

for X, b_{2} being set holds

( b_{2} = Carr X iff for a being set holds

( a in b_{2} iff ex s being 1-sorted st

( s in X & a = the carrier of s ) ) );

for X, b

( b

( a in b

( s in X & a = the carrier of s ) ) );

Lm2: for P being non empty POSet_set

for A being Element of P holds the carrier of A in Carr P

by Def7;

registration
end;

definition

let P be non empty POSet_set;

ex b_{1} being strict with_triple-like_morphisms Category st

( the carrier of b_{1} = 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 b_{1} ) & ( for m being Morphism of b_{1} 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 b_{1}

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

for b_{1}, b_{2} being strict with_triple-like_morphisms Category st the carrier of b_{1} = 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 b_{1} ) & ( for m being Morphism of b_{1} 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 b_{1}

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 carrier of b_{2} = 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 b_{2} ) & ( for m being Morphism of b_{2} 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 b_{2}

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

b_{1} = b_{2}

end;
func POSCat P -> strict with_triple-like_morphisms Category means :: ORDERS_3:def 8

( the carrier 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 ( the carrier 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)] ) );

ex b

( the carrier of b

for f being Element of Funcs (Carr P) st f in MonFuncs (a,b) holds

[[a,b],f] is Morphism of b

( m = [[a,b],f] & f in MonFuncs (a,b) ) ) & ( for m1, m2 being Morphism of b

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 b

for f being Element of Funcs (Carr P) st f in MonFuncs (a,b) holds

[[a,b],f] is Morphism of b

( m = [[a,b],f] & f in MonFuncs (a,b) ) ) & ( for m1, m2 being Morphism of b

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 carrier of b

for f being Element of Funcs (Carr P) st f in MonFuncs (a,b) holds

[[a,b],f] is Morphism of b

( m = [[a,b],f] & f in MonFuncs (a,b) ) ) & ( for m1, m2 being Morphism of b

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

b

proof end;

:: deftheorem defines POSCat ORDERS_3:def 8 :

for P being non empty POSet_set

for b_{2} being strict with_triple-like_morphisms Category holds

( b_{2} = POSCat P iff ( the carrier of b_{2} = 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 b_{2} ) & ( for m being Morphism of b_{2} 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 b_{2}

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

for P being non empty POSet_set

for b

( b

for f being Element of Funcs (Carr P) st f in MonFuncs (a,b) holds

[[a,b],f] is Morphism of b

( m = [[a,b],f] & f in MonFuncs (a,b) ) ) & ( for m1, m2 being Morphism of b

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{ F_{1}() -> non empty set , F_{2}( object , object ) -> functional set } :

AltCatEx{ F

ex C being strict AltCatStr st

( the carrier of C = F_{1}() & ( for i, j being Element of F_{1}() holds

( the Arrows of C . (i,j) = F_{2}(i,j) & ( for i, j, k being Element of F_{1}() holds the Comp of C . (i,j,k) = FuncComp (F_{2}(i,j),F_{2}(j,k)) ) ) ) )

provided( the carrier of C = F

( the Arrows of C . (i,j) = F

A1:
for i, j, k being Element of F_{1}()

for f, g being Function st f in F_{2}(i,j) & g in F_{2}(j,k) holds

g * f in F_{2}(i,k)

for f, g being Function st f in F

g * f in F

proof end;

scheme :: ORDERS_3:sch 2

AltCatUniq{ F_{1}() -> non empty set , F_{2}( object , object ) -> functional set } :

AltCatUniq{ F

for C1, C2 being strict AltCatStr st the carrier of C1 = F_{1}() & ( for i, j being Element of F_{1}() holds

( the Arrows of C1 . (i,j) = F_{2}(i,j) & ( for i, j, k being Element of F_{1}() holds the Comp of C1 . (i,j,k) = FuncComp (F_{2}(i,j),F_{2}(j,k)) ) ) ) & the carrier of C2 = F_{1}() & ( for i, j being Element of F_{1}() holds

( the Arrows of C2 . (i,j) = F_{2}(i,j) & ( for i, j, k being Element of F_{1}() holds the Comp of C2 . (i,j,k) = FuncComp (F_{2}(i,j),F_{2}(j,k)) ) ) ) holds

C1 = C2

( the Arrows of C1 . (i,j) = F

( the Arrows of C2 . (i,j) = F

C1 = C2

proof end;

definition

let P be non empty POSet_set;

ex b_{1} being strict AltCatStr st

( the carrier of b_{1} = P & ( for i, j being Element of P holds

( the Arrows of b_{1} . (i,j) = MonFuncs (i,j) & ( for i, j, k being Element of P holds the Comp of b_{1} . (i,j,k) = FuncComp ((MonFuncs (i,j)),(MonFuncs (j,k))) ) ) ) )

for b_{1}, b_{2} being strict AltCatStr st the carrier of b_{1} = P & ( for i, j being Element of P holds

( the Arrows of b_{1} . (i,j) = MonFuncs (i,j) & ( for i, j, k being Element of P holds the Comp of b_{1} . (i,j,k) = FuncComp ((MonFuncs (i,j)),(MonFuncs (j,k))) ) ) ) & the carrier of b_{2} = P & ( for i, j being Element of P holds

( the Arrows of b_{2} . (i,j) = MonFuncs (i,j) & ( for i, j, k being Element of P holds the Comp of b_{2} . (i,j,k) = FuncComp ((MonFuncs (i,j)),(MonFuncs (j,k))) ) ) ) holds

b_{1} = b_{2}

end;
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 ( 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))) ) ) ) );

ex b

( the carrier of b

( the Arrows of b

proof end;

uniqueness for b

( the Arrows of b

( the Arrows of b

b

proof end;

:: deftheorem Def9 defines POSAltCat ORDERS_3:def 9 :

for P being non empty POSet_set

for b_{2} being strict AltCatStr holds

( b_{2} = POSAltCat P iff ( the carrier of b_{2} = P & ( for i, j being Element of P holds

( the Arrows of b_{2} . (i,j) = MonFuncs (i,j) & ( for i, j, k being Element of P holds the Comp of b_{2} . (i,j,k) = FuncComp ((MonFuncs (i,j)),(MonFuncs (j,k))) ) ) ) ) );

for P being non empty POSet_set

for b

( b

( the Arrows of b

registration

let P be non empty POSet_set;

coherence

( POSAltCat P is transitive & not POSAltCat P is empty )

end;
coherence

( POSAltCat P is transitive & not POSAltCat P is empty )

proof end;

registration

let P be non empty POSet_set;

coherence

( POSAltCat P is associative & POSAltCat P is with_units )

end;
coherence

( POSAltCat P is associative & POSAltCat P is with_units )

proof end;

theorem :: ORDERS_3:12

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)

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;