:: YELLOW21 semantic presentation
begin
definition
let a be set ;
funca as_1-sorted -> 1-sorted equals :Def1: :: YELLOW21:def 1
a if a is 1-sorted
otherwise 1-sorted(# a #);
coherence
( ( a is 1-sorted implies a is 1-sorted ) & ( a is not 1-sorted implies 1-sorted(# a #) is 1-sorted ) ) ;
consistency
for b1 being 1-sorted holds verum ;
end;
:: deftheorem Def1 defines as_1-sorted YELLOW21:def_1_:_
for a being set holds
( ( a is 1-sorted implies a as_1-sorted = a ) & ( a is not 1-sorted implies a as_1-sorted = 1-sorted(# a #) ) );
definition
let W be set ;
defpred S1[ set ] means ( $1 is strict Poset & the carrier of ($1 as_1-sorted) in W );
func POSETS W -> set means :Def2: :: YELLOW21:def 2
for x being set holds
( x in it iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) );
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) ) ) & ( for x being set holds
( x in b2 iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) ) ) holds
b1 = b2
proof
let A, B be set ; ::_thesis: ( ( for x being set holds
( x in A iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) ) ) & ( for x being set holds
( x in B iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) ) ) implies A = B )
assume that
A1: for x being set holds
( x in A iff S1[x] ) and
A2: for x being set holds
( x in B iff S1[x] ) ; ::_thesis: A = B
thus A = B from XBOOLE_0:sch_2(A1, A2); ::_thesis: verum
end;
existence
ex b1 being set st
for x being set holds
( x in b1 iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) )
proof
defpred S2[ set , set ] means ex P being strict Poset st
( $2 = P & the InternalRel of P = $1 );
defpred S3[ set , set ] means $2 is Order of $1;
deffunc H1( set ) -> set = bool [:$1,$1:];
consider F being Function such that
A3: dom F = W and
A4: for x being set st x in W holds
for y being set holds
( y in F . x iff ( y in H1(x) & S3[x,y] ) ) from CARD_3:sch_2();
A5: now__::_thesis:_for_x,_y,_z_being_set_st_S2[x,y]_&_S2[x,z]_holds_
y_=_z
let x, y, z be set ; ::_thesis: ( S2[x,y] & S2[x,z] implies y = z )
assume S2[x,y] ; ::_thesis: ( S2[x,z] implies y = z )
then consider P1 being strict Poset such that
A6: ( y = P1 & the InternalRel of P1 = x ) ;
A7: dom the InternalRel of P1 = the carrier of P1 by ORDERS_1:14;
assume S2[x,z] ; ::_thesis: y = z
hence y = z by A6, A7, ORDERS_1:14; ::_thesis: verum
end;
consider A being set such that
A8: for x being set holds
( x in A iff ex y being set st
( y in Union F & S2[y,x] ) ) from TARSKI:sch_1(A5);
take A ; ::_thesis: for x being set holds
( x in A iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) )
let x be set ; ::_thesis: ( x in A iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) )
hereby ::_thesis: ( x is strict Poset & the carrier of (x as_1-sorted) in W implies x in A )
assume x in A ; ::_thesis: ( x is strict Poset & the carrier of (x as_1-sorted) in W )
then consider y being set such that
A9: y in Union F and
A10: ex P being strict Poset st
( x = P & the InternalRel of P = y ) by A8;
consider P being strict Poset such that
A11: x = P and
A12: the InternalRel of P = y by A10;
thus x is strict Poset by A11; ::_thesis: the carrier of (x as_1-sorted) in W
consider z being set such that
A13: z in W and
A14: y in F . z by A3, A9, CARD_5:2;
reconsider y = y as Order of z by A4, A13, A14;
( dom y = z & dom y = the carrier of P ) by A12, ORDERS_1:14;
hence the carrier of (x as_1-sorted) in W by A11, A13, Def1; ::_thesis: verum
end;
assume that
A15: x is strict Poset and
A16: the carrier of (x as_1-sorted) in W ; ::_thesis: x in A
reconsider P = x as strict Poset by A15;
A17: x as_1-sorted = P by Def1;
then the InternalRel of P in F . the carrier of P by A4, A16;
then the InternalRel of P in Union F by A3, A16, A17, CARD_5:2;
hence x in A by A8; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines POSETS YELLOW21:def_2_:_
for W being set
for b2 being set holds
( b2 = POSETS W iff for x being set holds
( x in b2 iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) ) );
registration
let W be non empty set ;
cluster POSETS W -> non empty ;
coherence
not POSETS W is empty
proof
set x = the Element of W;
set y = the Order of the Element of W;
RelStr(# the Element of W, the Order of the Element of W #) as_1-sorted = RelStr(# the Element of W, the Order of the Element of W #) by Def1;
hence not POSETS W is empty by Def2; ::_thesis: verum
end;
end;
registration
let W be with_non-empty_elements set ;
cluster POSETS W -> POSet_set-like ;
coherence
POSETS W is POSet_set-like
proof
let a be set ; :: according to ORDERS_3:def_4 ::_thesis: ( not a in POSETS W or a is RelStr )
assume A1: a in POSETS W ; ::_thesis: a is RelStr
then A2: the carrier of (a as_1-sorted) in W by Def2;
reconsider a = a as Poset by A1, Def2;
a = a as_1-sorted by Def1;
hence a is RelStr by A2; ::_thesis: verum
end;
end;
definition
let C be category;
attrC is carrier-underlaid means :Def3: :: YELLOW21:def 3
for a being object of C ex S being 1-sorted st
( a = S & the_carrier_of a = the carrier of S );
end;
:: deftheorem Def3 defines carrier-underlaid YELLOW21:def_3_:_
for C being category holds
( C is carrier-underlaid iff for a being object of C ex S being 1-sorted st
( a = S & the_carrier_of a = the carrier of S ) );
definition
let C be category;
attrC is lattice-wise means :Def4: :: YELLOW21:def 4
( C is semi-functional & C is set-id-inheriting & ( for a being object of C holds a is LATTICE ) & ( for a, b being object of C
for A, B being LATTICE st A = a & B = b holds
<^a,b^> c= MonFuncs (A,B) ) );
end;
:: deftheorem Def4 defines lattice-wise YELLOW21:def_4_:_
for C being category holds
( C is lattice-wise iff ( C is semi-functional & C is set-id-inheriting & ( for a being object of C holds a is LATTICE ) & ( for a, b being object of C
for A, B being LATTICE st A = a & B = b holds
<^a,b^> c= MonFuncs (A,B) ) ) );
definition
let C be category;
attrC is with_complete_lattices means :Def5: :: YELLOW21:def 5
( C is lattice-wise & ( for a being object of C holds a is complete LATTICE ) );
end;
:: deftheorem Def5 defines with_complete_lattices YELLOW21:def_5_:_
for C being category holds
( C is with_complete_lattices iff ( C is lattice-wise & ( for a being object of C holds a is complete LATTICE ) ) );
registration
cluster non empty transitive V110() with_units with_complete_lattices -> lattice-wise for AltCatStr ;
coherence
for b1 being category st b1 is with_complete_lattices holds
b1 is lattice-wise by Def5;
cluster non empty transitive V110() with_units lattice-wise -> concrete carrier-underlaid for AltCatStr ;
coherence
for b1 being category st b1 is lattice-wise holds
( b1 is concrete & b1 is carrier-underlaid )
proof
deffunc H1( set ) -> set = the carrier of (c1 as_1-sorted);
let C be category; ::_thesis: ( C is lattice-wise implies ( C is concrete & C is carrier-underlaid ) )
assume that
A1: ( C is semi-functional & C is set-id-inheriting ) and
A2: for a being object of C holds a is LATTICE and
A3: for a, b being object of C
for A, B being LATTICE st A = a & B = b holds
<^a,b^> c= MonFuncs (A,B) ; :: according to YELLOW21:def_4 ::_thesis: ( C is concrete & C is carrier-underlaid )
consider F being ManySortedSet of C such that
A4: for i being Element of C holds F . i = H1(i) from PBOOLE:sch_5();
C is para-functional
proof
take F ; :: according to YELLOW18:def_7 ::_thesis: for b1, b2 being Element of the carrier of C holds <^b1,b2^> c= Funcs ((F . b1),(F . b2))
let a, b be object of C; ::_thesis: <^a,b^> c= Funcs ((F . a),(F . b))
reconsider A = a, B = b as LATTICE by A2;
A5: <^a,b^> c= MonFuncs (A,B) by A3;
b as_1-sorted = B by Def1;
then A6: F . b = the carrier of B by A4;
a as_1-sorted = A by Def1;
then F . a = the carrier of A by A4;
then MonFuncs (A,B) c= Funcs ((F . a),(F . b)) by A6, ORDERS_3:11;
hence <^a,b^> c= Funcs ((F . a),(F . b)) by A5, XBOOLE_1:1; ::_thesis: verum
end;
hence C is concrete by A1; ::_thesis: C is carrier-underlaid
let a be object of C; :: according to YELLOW21:def_3 ::_thesis: ex S being 1-sorted st
( a = S & the_carrier_of a = the carrier of S )
reconsider S = a as LATTICE by A2;
( idm a in <^a,a^> & <^a,a^> c= MonFuncs (S,S) ) by A3;
then consider f being Function of S,S such that
A7: idm a = f and
A8: f in Funcs ( the carrier of S, the carrier of S) and
f is monotone by ORDERS_3:def_6;
take S ; ::_thesis: ( a = S & the_carrier_of a = the carrier of S )
thus a = S ; ::_thesis: the_carrier_of a = the carrier of S
thus the_carrier_of a = dom (id (the_carrier_of a)) by RELAT_1:45
.= dom f by A1, A7, YELLOW18:def_10
.= the carrier of S by A8, FUNCT_2:92 ; ::_thesis: verum
end;
end;
scheme :: YELLOW21:sch 1
localCLCatEx{ F1() -> non empty set , P1[ set , set , set ] } :
ex C being strict category st
( C is lattice-wise & the carrier of C = F1() & ( for a, b being LATTICE
for f being monotone Function of a,b holds
( f in the Arrows of C . (a,b) iff ( a in F1() & b in F1() & P1[a,b,f] ) ) ) )
provided
A1: for a being Element of F1() holds a is LATTICE and
A2: for a, b, c being LATTICE st a in F1() & b in F1() & c in F1() holds
for f being Function of a,b
for g being Function of b,c st P1[a,b,f] & P1[b,c,g] holds
P1[a,c,g * f] and
A3: for a being LATTICE st a in F1() holds
P1[a,a, id a]
proof
defpred S1[ set , set ] means ex a, b being LATTICE st
( $1 = [a,b] & ( for f being set holds
( f in $2 iff ( f in MonFuncs (a,b) & P1[a,b,f] ) ) ) );
set A = F1();
A4: now__::_thesis:_for_x_being_set_st_x_in_[:F1(),F1():]_holds_
ex_y_being_set_st_S1[x,y]
let x be set ; ::_thesis: ( x in [:F1(),F1():] implies ex y being set st S1[x,y] )
assume x in [:F1(),F1():] ; ::_thesis: ex y being set st S1[x,y]
then consider a, b being set such that
A5: ( a in F1() & b in F1() ) and
A6: x = [a,b] by ZFMISC_1:def_2;
reconsider a = a, b = b as LATTICE by A1, A5;
defpred S2[ set ] means P1[a,b,$1];
consider y being set such that
A7: for f being set holds
( f in y iff ( f in MonFuncs (a,b) & S2[f] ) ) from XBOOLE_0:sch_1();
take y = y; ::_thesis: S1[x,y]
thus S1[x,y] by A6, A7; ::_thesis: verum
end;
consider F being Function such that
dom F = [:F1(),F1():] and
A8: for x being set st x in [:F1(),F1():] holds
S1[x,F . x] from CLASSES1:sch_1(A4);
defpred S2[ set , set ] means for a being LATTICE st a = $1 holds
$2 = the carrier of a;
A9: now__::_thesis:_for_x_being_set_st_x_in_F1()_holds_
ex_b_being_set_st_S2[x,b]
let x be set ; ::_thesis: ( x in F1() implies ex b being set st S2[x,b] )
assume x in F1() ; ::_thesis: ex b being set st S2[x,b]
then reconsider a = x as LATTICE by A1;
reconsider b = the carrier of a as set ;
take b = b; ::_thesis: S2[x,b]
thus S2[x,b] ; ::_thesis: verum
end;
consider D being Function such that
dom D = F1() and
A10: for x being set st x in F1() holds
S2[x,D . x] from CLASSES1:sch_1(A9);
deffunc H1( set , set ) -> set = F . [$1,$2];
A11: now__::_thesis:_for_a,_b_being_LATTICE_st_a_in_F1()_&_b_in_F1()_holds_
for_f_being_set_holds_
(_(_f_in_F_._[a,b]_implies_(_P1[a,b,f]_&_f_in_MonFuncs_(a,b)_&_f_in_Funcs_(_the_carrier_of_a,_the_carrier_of_b)_&_f_is_monotone_Function_of_a,b_)_)_&_(_f_is_monotone_Function_of_a,b_&_P1[a,b,f]_implies_f_in_F_._[a,b]_)_)
let a, b be LATTICE; ::_thesis: ( a in F1() & b in F1() implies for f being set holds
( ( f in F . [a,b] implies ( P1[a,b,f] & f in MonFuncs (a,b) & f in Funcs ( the carrier of a, the carrier of b) & f is monotone Function of a,b ) ) & ( f is monotone Function of a,b & P1[a,b,f] implies f in F . [a,b] ) ) )
assume ( a in F1() & b in F1() ) ; ::_thesis: for f being set holds
( ( f in F . [a,b] implies ( P1[a,b,f] & f in MonFuncs (a,b) & f in Funcs ( the carrier of a, the carrier of b) & f is monotone Function of a,b ) ) & ( f is monotone Function of a,b & P1[a,b,f] implies f in F . [a,b] ) )
then [a,b] in [:F1(),F1():] by ZFMISC_1:87;
then consider a9, b9 being LATTICE such that
A12: [a,b] = [a9,b9] and
A13: for f being set holds
( f in F . [a,b] iff ( f in MonFuncs (a9,b9) & P1[a9,b9,f] ) ) by A8;
let f be set ; ::_thesis: ( ( f in F . [a,b] implies ( P1[a,b,f] & f in MonFuncs (a,b) & f in Funcs ( the carrier of a, the carrier of b) & f is monotone Function of a,b ) ) & ( f is monotone Function of a,b & P1[a,b,f] implies f in F . [a,b] ) )
A14: ( a = a9 & b = b9 ) by A12, XTUPLE_0:1;
hereby ::_thesis: ( f is monotone Function of a,b & P1[a,b,f] implies f in F . [a,b] )
assume A15: f in F . [a,b] ; ::_thesis: ( P1[a,b,f] & f in MonFuncs (a,b) & f in Funcs ( the carrier of a, the carrier of b) & f is monotone Function of a,b )
hence P1[a,b,f] by A13, A14; ::_thesis: ( f in MonFuncs (a,b) & f in Funcs ( the carrier of a, the carrier of b) & f is monotone Function of a,b )
thus f in MonFuncs (a,b) by A13, A14, A15; ::_thesis: ( f in Funcs ( the carrier of a, the carrier of b) & f is monotone Function of a,b )
then ex g being Function of a,b st
( f = g & g in Funcs ( the carrier of a, the carrier of b) & g is monotone ) by ORDERS_3:def_6;
hence ( f in Funcs ( the carrier of a, the carrier of b) & f is monotone Function of a,b ) ; ::_thesis: verum
end;
assume f is monotone Function of a,b ; ::_thesis: ( P1[a,b,f] implies f in F . [a,b] )
then reconsider g = f as monotone Function of a,b ;
( the carrier of b <> {} implies ( dom g = the carrier of a & rng g c= the carrier of b ) ) by FUNCT_2:def_1;
then g in Funcs ( the carrier of a, the carrier of b) by FUNCT_2:def_2;
then f in MonFuncs (a,b) by ORDERS_3:def_6;
hence ( P1[a,b,f] implies f in F . [a,b] ) by A13, A14; ::_thesis: verum
end;
A16: for a, b, c being Element of F1()
for f, g being Function st f in H1(a,b) & g in H1(b,c) holds
g * f in H1(a,c)
proof
let a, b, c be Element of F1(); ::_thesis: for f, g being Function st f in H1(a,b) & g in H1(b,c) holds
g * f in H1(a,c)
let f, g be Function; ::_thesis: ( f in H1(a,b) & g in H1(b,c) implies g * f in H1(a,c) )
assume that
A17: f in F . [a,b] and
A18: g in F . [b,c] ; ::_thesis: g * f in H1(a,c)
reconsider x = a, y = b, z = c as LATTICE by A1;
reconsider g9 = g as monotone Function of y,z by A11, A18;
reconsider f9 = f as monotone Function of x,y by A11, A17;
( P1[x,y,f9] & P1[y,z,g9] ) by A11, A17, A18;
then P1[a,c,g9 * f9] by A2;
then ( g9 * f9 is monotone Function of x,z implies g9 * f9 in F . [x,z] ) by A11;
hence g * f in H1(a,c) by YELLOW_2:12; ::_thesis: verum
end;
deffunc H2( set ) -> set = D . $1;
A19: for a, b being Element of F1() holds H1(a,b) c= Funcs (H2(a),H2(b))
proof
let a, b be Element of F1(); ::_thesis: H1(a,b) c= Funcs (H2(a),H2(b))
let f be set ; :: according to TARSKI:def_3 ::_thesis: ( not f in H1(a,b) or f in Funcs (H2(a),H2(b)) )
reconsider x = a, y = b as LATTICE by A1;
assume f in F . [a,b] ; ::_thesis: f in Funcs (H2(a),H2(b))
then f in Funcs ( the carrier of x, the carrier of y) by A11;
then f in Funcs ((D . a), the carrier of y) by A10;
hence f in Funcs (H2(a),H2(b)) by A10; ::_thesis: verum
end;
A20: now__::_thesis:_for_a_being_Element_of_F1()_holds_id_H2(a)_in_H1(a,a)
let a be Element of F1(); ::_thesis: id H2(a) in H1(a,a)
reconsider x = a as LATTICE by A1;
( id (D . a) = id x & P1[x,x, id x] ) by A3, A10;
hence id H2(a) in H1(a,a) by A11; ::_thesis: verum
end;
consider C being strict concrete category such that
A21: the carrier of C = F1() and
for a being object of C holds the_carrier_of a = H2(a) and
A22: for a, b being object of C holds <^a,b^> = H1(a,b) from YELLOW18:sch_16(A16, A19, A20);
take C ; ::_thesis: ( C is lattice-wise & the carrier of C = F1() & ( for a, b being LATTICE
for f being monotone Function of a,b holds
( f in the Arrows of C . (a,b) iff ( a in F1() & b in F1() & P1[a,b,f] ) ) ) )
thus ( C is semi-functional & C is set-id-inheriting ) ; :: according to YELLOW21:def_4 ::_thesis: ( ( for a being object of C holds a is LATTICE ) & ( for a, b being object of C
for A, B being LATTICE st A = a & B = b holds
<^a,b^> c= MonFuncs (A,B) ) & the carrier of C = F1() & ( for a, b being LATTICE
for f being monotone Function of a,b holds
( f in the Arrows of C . (a,b) iff ( a in F1() & b in F1() & P1[a,b,f] ) ) ) )
thus for a being object of C holds a is LATTICE by A1, A21; ::_thesis: ( ( for a, b being object of C
for A, B being LATTICE st A = a & B = b holds
<^a,b^> c= MonFuncs (A,B) ) & the carrier of C = F1() & ( for a, b being LATTICE
for f being monotone Function of a,b holds
( f in the Arrows of C . (a,b) iff ( a in F1() & b in F1() & P1[a,b,f] ) ) ) )
thus for a, b being object of C
for A, B being LATTICE st A = a & B = b holds
<^a,b^> c= MonFuncs (A,B) ::_thesis: ( the carrier of C = F1() & ( for a, b being LATTICE
for f being monotone Function of a,b holds
( f in the Arrows of C . (a,b) iff ( a in F1() & b in F1() & P1[a,b,f] ) ) ) )
proof
let a, b be object of C; ::_thesis: for A, B being LATTICE st A = a & B = b holds
<^a,b^> c= MonFuncs (A,B)
let A, B be LATTICE; ::_thesis: ( A = a & B = b implies <^a,b^> c= MonFuncs (A,B) )
assume A23: ( A = a & B = b ) ; ::_thesis: <^a,b^> c= MonFuncs (A,B)
let f be set ; :: according to TARSKI:def_3 ::_thesis: ( not f in <^a,b^> or f in MonFuncs (A,B) )
<^a,b^> = F . [A,B] by A22, A23;
hence ( not f in <^a,b^> or f in MonFuncs (A,B) ) by A11, A21, A23; ::_thesis: verum
end;
thus the carrier of C = F1() by A21; ::_thesis: for a, b being LATTICE
for f being monotone Function of a,b holds
( f in the Arrows of C . (a,b) iff ( a in F1() & b in F1() & P1[a,b,f] ) )
let a, b be LATTICE; ::_thesis: for f being monotone Function of a,b holds
( f in the Arrows of C . (a,b) iff ( a in F1() & b in F1() & P1[a,b,f] ) )
let f be monotone Function of a,b; ::_thesis: ( f in the Arrows of C . (a,b) iff ( a in F1() & b in F1() & P1[a,b,f] ) )
hereby ::_thesis: ( a in F1() & b in F1() & P1[a,b,f] implies f in the Arrows of C . (a,b) )
assume A24: f in the Arrows of C . (a,b) ; ::_thesis: ( a in F1() & b in F1() & P1[a,b,f] )
then [a,b] in dom the Arrows of C by FUNCT_1:def_2;
then A25: [a,b] in [:F1(),F1():] by A21;
hence ( a in F1() & b in F1() ) by ZFMISC_1:87; ::_thesis: P1[a,b,f]
reconsider x = a, y = b as object of C by A21, A25, ZFMISC_1:87;
the Arrows of C . [a,b] = <^x,y^>
.= F . [x,y] by A22 ;
hence P1[a,b,f] by A11, A21, A24; ::_thesis: verum
end;
assume A26: ( a in F1() & b in F1() ) ; ::_thesis: ( not P1[a,b,f] or f in the Arrows of C . (a,b) )
then reconsider x = a, y = b as object of C by A21;
the Arrows of C . [a,b] = <^x,y^>
.= F . [x,y] by A22 ;
hence ( not P1[a,b,f] or f in the Arrows of C . (a,b) ) by A11, A26; ::_thesis: verum
end;
registration
cluster non empty transitive strict V110() with_units reflexive with_complete_lattices for AltCatStr ;
existence
ex b1 being category st
( b1 is strict & b1 is with_complete_lattices )
proof
defpred S1[ set , set , set ] means c3 = c3;
set L = the complete LATTICE;
A1: for a, b, c being LATTICE st a in { the complete LATTICE} & b in { the complete LATTICE} & c in { the complete LATTICE} holds
for f being Function of a,b
for g being Function of b,c st S1[a,b,f] & S1[b,c,g] holds
S1[a,c,g * f] ;
A2: for a being LATTICE st a in { the complete LATTICE} holds
S1[a,a, id a] ;
A3: for a being Element of { the complete LATTICE} holds a is LATTICE by TARSKI:def_1;
consider C being strict category such that
A4: C is lattice-wise and
A5: the carrier of C = { the complete LATTICE} and
for a, b being LATTICE
for f being monotone Function of a,b holds
( f in the Arrows of C . (a,b) iff ( a in { the complete LATTICE} & b in { the complete LATTICE} & S1[a,b,f] ) ) from YELLOW21:sch_1(A3, A1, A2);
take C ; ::_thesis: ( C is strict & C is with_complete_lattices )
thus C is strict ; ::_thesis: C is with_complete_lattices
thus C is lattice-wise by A4; :: according to YELLOW21:def_5 ::_thesis: for a being object of C holds a is complete LATTICE
let a be object of C; ::_thesis: a is complete LATTICE
thus a is complete LATTICE by A5, TARSKI:def_1; ::_thesis: verum
end;
end;
theorem :: YELLOW21:1
for C being carrier-underlaid category
for a being object of C holds the_carrier_of a = the carrier of (a as_1-sorted)
proof
let C be carrier-underlaid category; ::_thesis: for a being object of C holds the_carrier_of a = the carrier of (a as_1-sorted)
let a be object of C; ::_thesis: the_carrier_of a = the carrier of (a as_1-sorted)
ex S being 1-sorted st
( a = S & the_carrier_of a = the carrier of S ) by Def3;
hence the_carrier_of a = the carrier of (a as_1-sorted) by Def1; ::_thesis: verum
end;
theorem Th2: :: YELLOW21:2
for C being set-id-inheriting carrier-underlaid category
for a being object of C holds idm a = id (a as_1-sorted)
proof
let C be set-id-inheriting carrier-underlaid category; ::_thesis: for a being object of C holds idm a = id (a as_1-sorted)
let a be object of C; ::_thesis: idm a = id (a as_1-sorted)
ex S being 1-sorted st
( a = S & the_carrier_of a = the carrier of S ) by Def3;
then the_carrier_of a = the carrier of (a as_1-sorted) by Def1;
hence idm a = id (a as_1-sorted) by YELLOW18:def_10; ::_thesis: verum
end;
notation
let C be lattice-wise category;
let a be object of C;
synonym latt a for C as_1-sorted ;
end;
definition
let C be lattice-wise category;
let a be object of C;
:: original: as_1-sorted
redefine func latt a -> LATTICE equals :: YELLOW21:def 6
a;
coherence
a as_1-sorted is LATTICE
proof
a is LATTICE by Def4;
hence a as_1-sorted is LATTICE by Def1; ::_thesis: verum
end;
compatibility
for b1 being LATTICE holds
( b1 = a as_1-sorted iff b1 = a )
proof
a is LATTICE by Def4;
hence for b1 being LATTICE holds
( b1 = a as_1-sorted iff b1 = a ) by Def1; ::_thesis: verum
end;
end;
:: deftheorem defines latt YELLOW21:def_6_:_
for C being lattice-wise category
for a being object of C holds latt a = a;
notation
let C be with_complete_lattices category;
let a be object of C;
synonym latt a for C as_1-sorted ;
end;
definition
let C be with_complete_lattices category;
let a be object of C;
:: original: as_1-sorted
redefine func latt a -> complete LATTICE;
coherence
a as_1-sorted is complete LATTICE by Def5;
end;
definition
let C be lattice-wise category;
let a, b be object of C;
assume A1: <^a,b^> <> {} ;
let f be Morphism of a,b;
func @ f -> monotone Function of (latt a),(latt b) equals :Def7: :: YELLOW21:def 7
f;
coherence
f is monotone Function of (latt a),(latt b)
proof
( f in <^a,b^> & <^a,b^> c= MonFuncs ((latt a),(latt b)) ) by A1, Def4;
then ex g being Function of (latt a),(latt b) st
( f = g & g in Funcs ( the carrier of (latt a), the carrier of (latt b)) & g is monotone ) by ORDERS_3:def_6;
hence f is monotone Function of (latt a),(latt b) ; ::_thesis: verum
end;
end;
:: deftheorem Def7 defines @ YELLOW21:def_7_:_
for C being lattice-wise category
for a, b being object of C st <^a,b^> <> {} holds
for f being Morphism of a,b holds @ f = f;
theorem Th3: :: YELLOW21:3
for C being lattice-wise category
for a, b, c being object of C st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = (@ g) * (@ f)
proof
let C be lattice-wise category; ::_thesis: for a, b, c being object of C st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = (@ g) * (@ f)
let a, b, c be object of C; ::_thesis: ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b
for g being Morphism of b,c holds g * f = (@ g) * (@ f) )
assume A1: ( <^a,b^> <> {} & <^b,c^> <> {} ) ; ::_thesis: for f being Morphism of a,b
for g being Morphism of b,c holds g * f = (@ g) * (@ f)
let f be Morphism of a,b; ::_thesis: for g being Morphism of b,c holds g * f = (@ g) * (@ f)
let g be Morphism of b,c; ::_thesis: g * f = (@ g) * (@ f)
( f = @ f & g = @ g ) by A1, Def7;
hence g * f = (@ g) * (@ f) by A1, YELLOW18:36; ::_thesis: verum
end;
scheme :: YELLOW21:sch 2
CLCatEx1{ F1() -> non empty set , P1[ set , set , set ] } :
ex C being strict lattice-wise category st
( the carrier of C = F1() & ( for a, b being object of C
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P1[ latt a, latt b,f] ) ) )
provided
A1: for a being Element of F1() holds a is LATTICE and
A2: for a, b, c being LATTICE st a in F1() & b in F1() & c in F1() holds
for f being Function of a,b
for g being Function of b,c st P1[a,b,f] & P1[b,c,g] holds
P1[a,c,g * f] and
A3: for a being LATTICE st a in F1() holds
P1[a,a, id a]
proof
A4: for a being LATTICE st a in F1() holds
P1[a,a, id a] by A3;
A5: for a, b, c being LATTICE st a in F1() & b in F1() & c in F1() holds
for f being Function of a,b
for g being Function of b,c st P1[a,b,f] & P1[b,c,g] holds
P1[a,c,g * f] by A2;
consider C being strict category such that
A6: C is lattice-wise and
A7: the carrier of C = F1() and
A8: for a, b being LATTICE
for f being monotone Function of a,b holds
( f in the Arrows of C . (a,b) iff ( a in F1() & b in F1() & P1[a,b,f] ) ) from YELLOW21:sch_1(A1, A5, A4);
reconsider C = C as strict lattice-wise category by A6;
take C ; ::_thesis: ( the carrier of C = F1() & ( for a, b being object of C
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P1[ latt a, latt b,f] ) ) )
thus the carrier of C = F1() by A7; ::_thesis: for a, b being object of C
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P1[ latt a, latt b,f] )
let a, b be object of C; ::_thesis: for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P1[ latt a, latt b,f] )
thus for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P1[ latt a, latt b,f] ) by A7, A8; ::_thesis: verum
end;
scheme :: YELLOW21:sch 3
CLCatEx2{ F1() -> non empty set , P1[ set ], P2[ set , set , set ] } :
ex C being strict lattice-wise category st
( ( for x being LATTICE holds
( x is object of C iff ( x is strict & P1[x] & the carrier of x in F1() ) ) ) & ( for a, b being object of C
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P2[ latt a, latt b,f] ) ) )
provided
A1: ex x being strict LATTICE st
( P1[x] & the carrier of x in F1() ) and
A2: for a, b, c being LATTICE st P1[a] & P1[b] & P1[c] holds
for f being Function of a,b
for g being Function of b,c st P2[a,b,f] & P2[b,c,g] holds
P2[a,c,g * f] and
A3: for a being LATTICE st P1[a] holds
P2[a,a, id a]
proof
defpred S1[ set ] means ( $1 is LATTICE & P1[$1] );
consider A being set such that
A4: for x being set holds
( x in A iff ( x in POSETS F1() & S1[x] ) ) from XBOOLE_0:sch_1();
consider x being strict LATTICE such that
A5: P1[x] and
A6: the carrier of x in F1() by A1;
x as_1-sorted = x by Def1;
then x in POSETS F1() by A6, Def2;
then reconsider A = A as non empty set by A4, A5;
A7: now__::_thesis:_for_a,_b,_c_being_LATTICE_st_a_in_A_&_b_in_A_&_c_in_A_holds_
for_f_being_Function_of_a,b
for_g_being_Function_of_b,c_st_P2[a,b,f]_&_P2[b,c,g]_holds_
P2[a,c,g_*_f]
let a, b, c be LATTICE; ::_thesis: ( a in A & b in A & c in A implies for f being Function of a,b
for g being Function of b,c st P2[a,b,f] & P2[b,c,g] holds
P2[a,c,g * f] )
assume that
A8: ( a in A & b in A ) and
A9: c in A ; ::_thesis: for f being Function of a,b
for g being Function of b,c st P2[a,b,f] & P2[b,c,g] holds
P2[a,c,g * f]
A10: P1[c] by A4, A9;
( P1[a] & P1[b] ) by A4, A8;
hence for f being Function of a,b
for g being Function of b,c st P2[a,b,f] & P2[b,c,g] holds
P2[a,c,g * f] by A2, A10; ::_thesis: verum
end;
A11: now__::_thesis:_for_a_being_LATTICE_st_a_in_A_holds_
P2[a,a,_id_a]
let a be LATTICE; ::_thesis: ( a in A implies P2[a,a, id a] )
assume a in A ; ::_thesis: P2[a,a, id a]
then P1[a] by A4;
hence P2[a,a, id a] by A3; ::_thesis: verum
end;
A12: for a being Element of A holds a is LATTICE by A4;
consider C being strict lattice-wise category such that
A13: the carrier of C = A and
A14: for a, b being object of C
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P2[ latt a, latt b,f] ) from YELLOW21:sch_2(A12, A7, A11);
take C ; ::_thesis: ( ( for x being LATTICE holds
( x is object of C iff ( x is strict & P1[x] & the carrier of x in F1() ) ) ) & ( for a, b being object of C
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P2[ latt a, latt b,f] ) ) )
hereby ::_thesis: for a, b being object of C
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P2[ latt a, latt b,f] )
let x be LATTICE; ::_thesis: ( x is object of C iff ( x is strict & P1[x] & the carrier of x in F1() ) )
x as_1-sorted = x by Def1;
then ( x in POSETS F1() iff ( x is strict Poset & the carrier of x in F1() ) ) by Def2;
hence ( x is object of C iff ( x is strict & P1[x] & the carrier of x in F1() ) ) by A4, A13; ::_thesis: verum
end;
thus for a, b being object of C
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P2[ latt a, latt b,f] ) by A14; ::_thesis: verum
end;
scheme :: YELLOW21:sch 4
CLCatUniq1{ F1() -> non empty set , P1[ set , set , set ] } :
for C1, C2 being lattice-wise category st the carrier of C1 = F1() & ( for a, b being object of C1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P1[a,b,f] ) ) & the carrier of C2 = F1() & ( for a, b being object of C2
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P1[a,b,f] ) ) holds
AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #)
proof
let A1, A2 be lattice-wise category; ::_thesis: ( the carrier of A1 = F1() & ( for a, b being object of A1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P1[a,b,f] ) ) & the carrier of A2 = F1() & ( for a, b being object of A2
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P1[a,b,f] ) ) implies AltCatStr(# the carrier of A1, the Arrows of A1, the Comp of A1 #) = AltCatStr(# the carrier of A2, the Arrows of A2, the Comp of A2 #) )
deffunc H1( set , set ) -> set = the Arrows of A1 . ($1,$2);
assume that
A1: the carrier of A1 = F1() and
A2: for a, b being object of A1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P1[a,b,f] ) and
A3: the carrier of A2 = F1() and
A4: for a, b being object of A2
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P1[a,b,f] ) ; ::_thesis: AltCatStr(# the carrier of A1, the Arrows of A1, the Comp of A1 #) = AltCatStr(# the carrier of A2, the Arrows of A2, the Comp of A2 #)
A5: now__::_thesis:_for_a,_b_being_object_of_A2_holds_<^a,b^>_=_the_Arrows_of_A1_._(a,b)
let a, b be object of A2; ::_thesis: <^a,b^> = the Arrows of A1 . (a,b)
reconsider a9 = a, b9 = b as object of A1 by A1, A3;
A6: <^a9,b9^> = the Arrows of A1 . (a9,b9) ;
thus <^a,b^> = the Arrows of A1 . (a,b) ::_thesis: verum
proof
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: the Arrows of A1 . (a,b) c= <^a,b^>
let x be set ; ::_thesis: ( x in <^a,b^> implies x in the Arrows of A1 . (a,b) )
assume A7: x in <^a,b^> ; ::_thesis: x in the Arrows of A1 . (a,b)
then reconsider f = x as Morphism of a,b ;
A8: @ f = f by A7, Def7;
then P1[ latt a9, latt b9, @ f] by A4, A7;
hence x in the Arrows of A1 . (a,b) by A2, A6, A8; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the Arrows of A1 . (a,b) or x in <^a,b^> )
assume A9: x in the Arrows of A1 . (a,b) ; ::_thesis: x in <^a,b^>
then reconsider f = x as Morphism of a9,b9 ;
A10: @ f = f by A9, Def7;
then P1[ latt a, latt b, @ f] by A2, A9;
hence x in <^a,b^> by A4, A10; ::_thesis: verum
end;
end;
A11: for a, b being object of A1 holds <^a,b^> = the Arrows of A1 . (a,b) ;
for C1, C2 being semi-functional para-functional category st the carrier of C1 = F1() & ( for a, b being object of C1 holds <^a,b^> = H1(a,b) ) & the carrier of C2 = F1() & ( for a, b being object of C2 holds <^a,b^> = H1(a,b) ) holds
AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #) from YELLOW18:sch_19();
hence AltCatStr(# the carrier of A1, the Arrows of A1, the Comp of A1 #) = AltCatStr(# the carrier of A2, the Arrows of A2, the Comp of A2 #) by A1, A3, A11, A5; ::_thesis: verum
end;
scheme :: YELLOW21:sch 5
CLCatUniq2{ F1() -> non empty set , P1[ set ], P2[ set , set , set ] } :
for C1, C2 being lattice-wise category st ( for x being LATTICE holds
( x is object of C1 iff ( x is strict & P1[x] & the carrier of x in F1() ) ) ) & ( for a, b being object of C1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P2[a,b,f] ) ) & ( for x being LATTICE holds
( x is object of C2 iff ( x is strict & P1[x] & the carrier of x in F1() ) ) ) & ( for a, b being object of C2
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P2[a,b,f] ) ) holds
AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #)
proof
let A1, A2 be lattice-wise category; ::_thesis: ( ( for x being LATTICE holds
( x is object of A1 iff ( x is strict & P1[x] & the carrier of x in F1() ) ) ) & ( for a, b being object of A1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P2[a,b,f] ) ) & ( for x being LATTICE holds
( x is object of A2 iff ( x is strict & P1[x] & the carrier of x in F1() ) ) ) & ( for a, b being object of A2
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P2[a,b,f] ) ) implies AltCatStr(# the carrier of A1, the Arrows of A1, the Comp of A1 #) = AltCatStr(# the carrier of A2, the Arrows of A2, the Comp of A2 #) )
assume that
A1: for x being LATTICE holds
( x is object of A1 iff ( x is strict & P1[x] & the carrier of x in F1() ) ) and
A2: for a, b being object of A1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P2[a,b,f] ) and
A3: for x being LATTICE holds
( x is object of A2 iff ( x is strict & P1[x] & the carrier of x in F1() ) ) ; ::_thesis: ( ex a, b being object of A2 ex f being monotone Function of (latt a),(latt b) st
( ( f in <^a,b^> implies P2[a,b,f] ) implies ( P2[a,b,f] & not f in <^a,b^> ) ) or AltCatStr(# the carrier of A1, the Arrows of A1, the Comp of A1 #) = AltCatStr(# the carrier of A2, the Arrows of A2, the Comp of A2 #) )
A4: the carrier of A2 = the carrier of A1
proof
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: the carrier of A1 c= the carrier of A2
let x be set ; ::_thesis: ( x in the carrier of A2 implies x in the carrier of A1 )
assume A5: x in the carrier of A2 ; ::_thesis: x in the carrier of A1
then A6: x is LATTICE by Def4;
then A7: ( x is strict LATTICE & P1[x] ) by A3, A5;
A8: x as_1-sorted = x by A6, Def1;
then the carrier of (x as_1-sorted) in F1() by A3, A5, A6;
then x is object of A1 by A1, A8, A7;
hence x in the carrier of A1 ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of A1 or x in the carrier of A2 )
assume A9: x in the carrier of A1 ; ::_thesis: x in the carrier of A2
then A10: x is LATTICE by Def4;
then A11: ( x is strict LATTICE & P1[x] ) by A1, A9;
A12: x as_1-sorted = x by A10, Def1;
then the carrier of (x as_1-sorted) in F1() by A1, A9, A10;
then x is object of A2 by A3, A12, A11;
hence x in the carrier of A2 ; ::_thesis: verum
end;
for C1, C2 being lattice-wise category st the carrier of C1 = the carrier of A1 & ( for a, b being object of C1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P2[a,b,f] ) ) & the carrier of C2 = the carrier of A1 & ( for a, b being object of C2
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P2[a,b,f] ) ) holds
AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #) from YELLOW21:sch_4();
hence ( ex a, b being object of A2 ex f being monotone Function of (latt a),(latt b) st
( ( f in <^a,b^> implies P2[a,b,f] ) implies ( P2[a,b,f] & not f in <^a,b^> ) ) or AltCatStr(# the carrier of A1, the Arrows of A1, the Comp of A1 #) = AltCatStr(# the carrier of A2, the Arrows of A2, the Comp of A2 #) ) by A2, A4; ::_thesis: verum
end;
scheme :: YELLOW21:sch 6
CLCovariantFunctorEx{ P1[ set , set , set ], P2[ set , set , set ], F1() -> lattice-wise category, F2() -> lattice-wise category, F3( set ) -> LATTICE, F4( set , set , set ) -> Function } :
ex F being strict covariant Functor of F1(),F2() st
( ( for a being object of F1() holds F . a = F3((latt a)) ) & ( for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F4((latt a),(latt b),(@ f)) ) )
provided
A1: for a, b being LATTICE
for f being Function of a,b holds
( f in the Arrows of F1() . (a,b) iff ( a in the carrier of F1() & b in the carrier of F1() & P1[a,b,f] ) ) and
A2: for a, b being LATTICE
for f being Function of a,b holds
( f in the Arrows of F2() . (a,b) iff ( a in the carrier of F2() & b in the carrier of F2() & P2[a,b,f] ) ) and
A3: for a being LATTICE st a in the carrier of F1() holds
F3(a) in the carrier of F2() and
A4: for a, b being LATTICE
for f being Function of a,b st P1[a,b,f] holds
( F4(a,b,f) is Function of F3(a),F3(b) & P2[F3(a),F3(b),F4(a,b,f)] ) and
A5: for a being LATTICE st a in the carrier of F1() holds
F4(a,a,(id a)) = id F3(a) and
A6: for a, b, c being LATTICE
for f being Function of a,b
for g being Function of b,c st P1[a,b,f] & P1[b,c,g] holds
F4(a,c,(g * f)) = F4(b,c,g) * F4(a,b,f)
proof
A7: for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F4(a,b,f) in the Arrows of F2() . (F3(a),F3(b))
proof
let a, b be object of F1(); ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds F4(a,b,f) in the Arrows of F2() . (F3(a),F3(b)) )
assume A8: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b holds F4(a,b,f) in the Arrows of F2() . (F3(a),F3(b))
let f be Morphism of a,b; ::_thesis: F4(a,b,f) in the Arrows of F2() . (F3(a),F3(b))
A9: f = @ f by A8, Def7;
then P1[a,b,f] by A1, A8;
then A10: ( F4(a,b,f) is Function of F3(a),F3(b) & P2[F3(a),F3(b),F4(a,b,f)] ) by A4, A9;
( F3(a) in the carrier of F2() & F3(b) in the carrier of F2() ) by A3, A9;
hence F4(a,b,f) in the Arrows of F2() . (F3(a),F3(b)) by A2, A10; ::_thesis: verum
end;
A11: now__::_thesis:_for_a,_b,_c_being_object_of_F1()_st_<^a,b^>_<>_{}_&_<^b,c^>_<>_{}_holds_
for_f_being_Morphism_of_a,b
for_g_being_Morphism_of_b,c
for_a9,_b9,_c9_being_object_of_F2()_st_a9_=_F3(a)_&_b9_=_F3(b)_&_c9_=_F3(c)_holds_
for_f9_being_Morphism_of_a9,b9
for_g9_being_Morphism_of_b9,c9_st_f9_=_F4(a,b,f)_&_g9_=_F4(b,c,g)_holds_
F4(a,c,(g_*_f))_=_g9_*_f9
let a, b, c be object of F1(); ::_thesis: ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b
for g being Morphism of b,c
for a9, b9, c9 being object of F2() st a9 = F3(a) & b9 = F3(b) & c9 = F3(c) holds
for f9 being Morphism of a9,b9
for g9 being Morphism of b9,c9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds
F4(a,c,(g * f)) = g9 * f9 )
assume that
A12: <^a,b^> <> {} and
A13: <^b,c^> <> {} ; ::_thesis: for f being Morphism of a,b
for g being Morphism of b,c
for a9, b9, c9 being object of F2() st a9 = F3(a) & b9 = F3(b) & c9 = F3(c) holds
for f9 being Morphism of a9,b9
for g9 being Morphism of b9,c9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds
F4(a,c,(g * f)) = g9 * f9
let f be Morphism of a,b; ::_thesis: for g being Morphism of b,c
for a9, b9, c9 being object of F2() st a9 = F3(a) & b9 = F3(b) & c9 = F3(c) holds
for f9 being Morphism of a9,b9
for g9 being Morphism of b9,c9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds
F4(a,c,(g * f)) = g9 * f9
let g be Morphism of b,c; ::_thesis: for a9, b9, c9 being object of F2() st a9 = F3(a) & b9 = F3(b) & c9 = F3(c) holds
for f9 being Morphism of a9,b9
for g9 being Morphism of b9,c9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds
F4(a,c,(g * f)) = g9 * f9
let a9, b9, c9 be object of F2(); ::_thesis: ( a9 = F3(a) & b9 = F3(b) & c9 = F3(c) implies for f9 being Morphism of a9,b9
for g9 being Morphism of b9,c9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds
F4(a,c,(g * f)) = g9 * f9 )
assume that
A14: a9 = F3(a) and
A15: b9 = F3(b) and
A16: c9 = F3(c) ; ::_thesis: for f9 being Morphism of a9,b9
for g9 being Morphism of b9,c9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds
F4(a,c,(g * f)) = g9 * f9
let f9 be Morphism of a9,b9; ::_thesis: for g9 being Morphism of b9,c9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds
F4(a,c,(g * f)) = g9 * f9
let g9 be Morphism of b9,c9; ::_thesis: ( f9 = F4(a,b,f) & g9 = F4(b,c,g) implies F4(a,c,(g * f)) = g9 * f9 )
assume A17: ( f9 = F4(a,b,f) & g9 = F4(b,c,g) ) ; ::_thesis: F4(a,c,(g * f)) = g9 * f9
A18: F4(a,b,f) in the Arrows of F2() . (F3(a),F3(b)) by A7, A12;
then A19: @ f9 = f9 by A14, A15, Def7;
A20: @ g = g by A13, Def7;
then A21: P1[b,c,g] by A1, A13;
A22: F4(b,c,g) in the Arrows of F2() . (F3(b),F3(c)) by A7, A13;
then A23: @ g9 = g9 by A15, A16, Def7;
A24: @ f = f by A12, Def7;
then P1[a,b,f] by A1, A12;
then F4(a,c,((@ g) * (@ f))) = F4(b,c,g) * F4(a,b,f) by A6, A24, A20, A21
.= g9 * f9 by A14, A15, A16, A17, A18, A22, A19, A23, Th3 ;
hence F4(a,c,(g * f)) = g9 * f9 by A12, A13, Th3; ::_thesis: verum
end;
A25: now__::_thesis:_for_a_being_object_of_F1()
for_a9_being_object_of_F2()_st_a9_=_F3(a)_holds_
F4(a,a,(idm_a))_=_idm_a9
let a be object of F1(); ::_thesis: for a9 being object of F2() st a9 = F3(a) holds
F4(a,a,(idm a)) = idm a9
let a9 be object of F2(); ::_thesis: ( a9 = F3(a) implies F4(a,a,(idm a)) = idm a9 )
assume A26: a9 = F3(a) ; ::_thesis: F4(a,a,(idm a)) = idm a9
idm a = id (latt a) by Th2;
hence F4(a,a,(idm a)) = id (latt a9) by A5, A26
.= idm a9 by Th2 ;
::_thesis: verum
end;
A27: for a being object of F1() holds F3(a) is object of F2()
proof
let a be object of F1(); ::_thesis: F3(a) is object of F2()
a is LATTICE by Def4;
hence F3(a) is object of F2() by A3; ::_thesis: verum
end;
consider F being strict covariant Functor of F1(),F2() such that
A28: for a being object of F1() holds F . a = F3(a) and
A29: for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F4(a,b,f) from YELLOW18:sch_8(A27, A7, A11, A25);
take F ; ::_thesis: ( ( for a being object of F1() holds F . a = F3((latt a)) ) & ( for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F4((latt a),(latt b),(@ f)) ) )
thus for a being object of F1() holds F . a = F3((latt a)) by A28; ::_thesis: for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F4((latt a),(latt b),(@ f))
let a, b be object of F1(); ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds F . f = F4((latt a),(latt b),(@ f)) )
assume A30: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b holds F . f = F4((latt a),(latt b),(@ f))
let f be Morphism of a,b; ::_thesis: F . f = F4((latt a),(latt b),(@ f))
f = @ f by A30, Def7;
hence F . f = F4((latt a),(latt b),(@ f)) by A29, A30; ::_thesis: verum
end;
scheme :: YELLOW21:sch 7
CLContravariantFunctorEx{ P1[ set , set , set ], P2[ set , set , set ], F1() -> lattice-wise category, F2() -> lattice-wise category, F3( set ) -> LATTICE, F4( set , set , set ) -> Function } :
ex F being strict contravariant Functor of F1(),F2() st
( ( for a being object of F1() holds F . a = F3((latt a)) ) & ( for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F4((latt a),(latt b),(@ f)) ) )
provided
A1: for a, b being LATTICE
for f being Function of a,b holds
( f in the Arrows of F1() . (a,b) iff ( a in the carrier of F1() & b in the carrier of F1() & P1[a,b,f] ) ) and
A2: for a, b being LATTICE
for f being Function of a,b holds
( f in the Arrows of F2() . (a,b) iff ( a in the carrier of F2() & b in the carrier of F2() & P2[a,b,f] ) ) and
A3: for a being LATTICE st a in the carrier of F1() holds
F3(a) in the carrier of F2() and
A4: for a, b being LATTICE
for f being Function of a,b st P1[a,b,f] holds
( F4(a,b,f) is Function of F3(b),F3(a) & P2[F3(b),F3(a),F4(a,b,f)] ) and
A5: for a being LATTICE st a in the carrier of F1() holds
F4(a,a,(id a)) = id F3(a) and
A6: for a, b, c being LATTICE
for f being Function of a,b
for g being Function of b,c st P1[a,b,f] & P1[b,c,g] holds
F4(a,c,(g * f)) = F4(a,b,f) * F4(b,c,g)
proof
A7: for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F4(a,b,f) in the Arrows of F2() . (F3(b),F3(a))
proof
let a, b be object of F1(); ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds F4(a,b,f) in the Arrows of F2() . (F3(b),F3(a)) )
assume A8: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b holds F4(a,b,f) in the Arrows of F2() . (F3(b),F3(a))
let f be Morphism of a,b; ::_thesis: F4(a,b,f) in the Arrows of F2() . (F3(b),F3(a))
A9: f = @ f by A8, Def7;
then P1[a,b,f] by A1, A8;
then A10: ( F4(a,b,f) is Function of F3(b),F3(a) & P2[F3(b),F3(a),F4(a,b,f)] ) by A4, A9;
( F3(a) in the carrier of F2() & F3(b) in the carrier of F2() ) by A3, A9;
hence F4(a,b,f) in the Arrows of F2() . (F3(b),F3(a)) by A2, A10; ::_thesis: verum
end;
A11: now__::_thesis:_for_a,_b,_c_being_object_of_F1()_st_<^a,b^>_<>_{}_&_<^b,c^>_<>_{}_holds_
for_f_being_Morphism_of_a,b
for_g_being_Morphism_of_b,c
for_a9,_b9,_c9_being_object_of_F2()_st_a9_=_F3(a)_&_b9_=_F3(b)_&_c9_=_F3(c)_holds_
for_f9_being_Morphism_of_b9,a9
for_g9_being_Morphism_of_c9,b9_st_f9_=_F4(a,b,f)_&_g9_=_F4(b,c,g)_holds_
F4(a,c,(g_*_f))_=_f9_*_g9
let a, b, c be object of F1(); ::_thesis: ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b
for g being Morphism of b,c
for a9, b9, c9 being object of F2() st a9 = F3(a) & b9 = F3(b) & c9 = F3(c) holds
for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds
F4(a,c,(g * f)) = f9 * g9 )
assume that
A12: <^a,b^> <> {} and
A13: <^b,c^> <> {} ; ::_thesis: for f being Morphism of a,b
for g being Morphism of b,c
for a9, b9, c9 being object of F2() st a9 = F3(a) & b9 = F3(b) & c9 = F3(c) holds
for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds
F4(a,c,(g * f)) = f9 * g9
let f be Morphism of a,b; ::_thesis: for g being Morphism of b,c
for a9, b9, c9 being object of F2() st a9 = F3(a) & b9 = F3(b) & c9 = F3(c) holds
for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds
F4(a,c,(g * f)) = f9 * g9
let g be Morphism of b,c; ::_thesis: for a9, b9, c9 being object of F2() st a9 = F3(a) & b9 = F3(b) & c9 = F3(c) holds
for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds
F4(a,c,(g * f)) = f9 * g9
let a9, b9, c9 be object of F2(); ::_thesis: ( a9 = F3(a) & b9 = F3(b) & c9 = F3(c) implies for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds
F4(a,c,(g * f)) = f9 * g9 )
assume that
A14: a9 = F3(a) and
A15: b9 = F3(b) and
A16: c9 = F3(c) ; ::_thesis: for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds
F4(a,c,(g * f)) = f9 * g9
let f9 be Morphism of b9,a9; ::_thesis: for g9 being Morphism of c9,b9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds
F4(a,c,(g * f)) = f9 * g9
let g9 be Morphism of c9,b9; ::_thesis: ( f9 = F4(a,b,f) & g9 = F4(b,c,g) implies F4(a,c,(g * f)) = f9 * g9 )
assume A17: ( f9 = F4(a,b,f) & g9 = F4(b,c,g) ) ; ::_thesis: F4(a,c,(g * f)) = f9 * g9
A18: F4(a,b,f) in the Arrows of F2() . (F3(b),F3(a)) by A7, A12;
then A19: @ f9 = f9 by A14, A15, Def7;
A20: @ g = g by A13, Def7;
then A21: P1[b,c,g] by A1, A13;
A22: F4(b,c,g) in the Arrows of F2() . (F3(c),F3(b)) by A7, A13;
then A23: @ g9 = g9 by A15, A16, Def7;
A24: @ f = f by A12, Def7;
then P1[a,b,f] by A1, A12;
then F4(a,c,((@ g) * (@ f))) = F4(a,b,f) * F4(b,c,g) by A6, A24, A20, A21
.= f9 * g9 by A14, A15, A16, A17, A18, A22, A19, A23, Th3 ;
hence F4(a,c,(g * f)) = f9 * g9 by A12, A13, Th3; ::_thesis: verum
end;
A25: now__::_thesis:_for_a_being_object_of_F1()
for_a9_being_object_of_F2()_st_a9_=_F3(a)_holds_
F4(a,a,(idm_a))_=_idm_a9
let a be object of F1(); ::_thesis: for a9 being object of F2() st a9 = F3(a) holds
F4(a,a,(idm a)) = idm a9
let a9 be object of F2(); ::_thesis: ( a9 = F3(a) implies F4(a,a,(idm a)) = idm a9 )
assume A26: a9 = F3(a) ; ::_thesis: F4(a,a,(idm a)) = idm a9
idm a = id (latt a) by Th2;
hence F4(a,a,(idm a)) = id (latt a9) by A5, A26
.= idm a9 by Th2 ;
::_thesis: verum
end;
A27: for a being object of F1() holds F3(a) is object of F2()
proof
let a be object of F1(); ::_thesis: F3(a) is object of F2()
a is LATTICE by Def4;
hence F3(a) is object of F2() by A3; ::_thesis: verum
end;
consider F being strict contravariant Functor of F1(),F2() such that
A28: for a being object of F1() holds F . a = F3(a) and
A29: for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F4(a,b,f) from YELLOW18:sch_9(A27, A7, A11, A25);
take F ; ::_thesis: ( ( for a being object of F1() holds F . a = F3((latt a)) ) & ( for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F4((latt a),(latt b),(@ f)) ) )
thus for a being object of F1() holds F . a = F3((latt a)) by A28; ::_thesis: for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F4((latt a),(latt b),(@ f))
let a, b be object of F1(); ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds F . f = F4((latt a),(latt b),(@ f)) )
assume A30: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b holds F . f = F4((latt a),(latt b),(@ f))
let f be Morphism of a,b; ::_thesis: F . f = F4((latt a),(latt b),(@ f))
f = @ f by A30, Def7;
hence F . f = F4((latt a),(latt b),(@ f)) by A29, A30; ::_thesis: verum
end;
scheme :: YELLOW21:sch 8
CLCatIsomorphism{ P1[ set , set , set ], P2[ set , set , set ], F1() -> lattice-wise category, F2() -> lattice-wise category, F3( set ) -> LATTICE, F4( set , set , set ) -> Function } :
F1(),F2() are_isomorphic
provided
A1: for a, b being LATTICE
for f being Function of a,b holds
( f in the Arrows of F1() . (a,b) iff ( a in the carrier of F1() & b in the carrier of F1() & P1[a,b,f] ) ) and
A2: for a, b being LATTICE
for f being Function of a,b holds
( f in the Arrows of F2() . (a,b) iff ( a in the carrier of F2() & b in the carrier of F2() & P2[a,b,f] ) ) and
A3: ex F being covariant Functor of F1(),F2() st
( ( for a being object of F1() holds F . a = F3(a) ) & ( for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F4(a,b,f) ) ) and
A4: for a, b being LATTICE st a in the carrier of F1() & b in the carrier of F1() & F3(a) = F3(b) holds
a = b and
A5: for a, b being LATTICE
for f, g being Function of a,b st P1[a,b,f] & P1[a,b,g] & F4(a,b,f) = F4(a,b,g) holds
f = g and
A6: for a, b being LATTICE
for f being Function of a,b st P2[a,b,f] holds
ex c, d being LATTICE ex g being Function of c,d st
( c in the carrier of F1() & d in the carrier of F1() & P1[c,d,g] & a = F3(c) & b = F3(d) & f = F4(c,d,g) )
proof
A7: for a, b being object of F1() st F3(a) = F3(b) holds
a = b
proof
let a, b be object of F1(); ::_thesis: ( F3(a) = F3(b) implies a = b )
( a = latt a & b = latt b ) ;
hence ( F3(a) = F3(b) implies a = b ) by A4; ::_thesis: verum
end;
A8: now__::_thesis:_for_a,_b_being_object_of_F2()_st_<^a,b^>_<>_{}_holds_
for_f_being_Morphism_of_a,b_ex_c,_d_being_object_of_F1()_ex_g_being_Morphism_of_c,d_st_
(_a_=_F3(c)_&_b_=_F3(d)_&_<^c,d^>_<>_{}_&_f_=_F4(c,d,g)_)
let a, b be object of F2(); ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b ex c, d being object of F1() ex g being Morphism of c,d st
( a = F3(c) & b = F3(d) & <^c,d^> <> {} & f = F4(c,d,g) ) )
assume A9: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b ex c, d being object of F1() ex g being Morphism of c,d st
( a = F3(c) & b = F3(d) & <^c,d^> <> {} & f = F4(c,d,g) )
let f be Morphism of a,b; ::_thesis: ex c, d being object of F1() ex g being Morphism of c,d st
( a = F3(c) & b = F3(d) & <^c,d^> <> {} & f = F4(c,d,g) )
A10: @ f = f by A9, Def7;
then P2[ latt a, latt b, @ f] by A2, A9;
then consider c, d being LATTICE, g being Function of c,d such that
A11: ( c in the carrier of F1() & d in the carrier of F1() ) and
A12: P1[c,d,g] and
A13: ( latt a = F3(c) & latt b = F3(d) & @ f = F4(c,d,g) ) by A6;
reconsider c9 = c, d9 = d as object of F1() by A11;
g in <^c9,d9^> by A1, A12;
hence ex c, d being object of F1() ex g being Morphism of c,d st
( a = F3(c) & b = F3(d) & <^c,d^> <> {} & f = F4(c,d,g) ) by A10, A13; ::_thesis: verum
end;
A14: for a, b being object of F1() st <^a,b^> <> {} holds
for f, g being Morphism of a,b st F4(a,b,f) = F4(a,b,g) holds
f = g
proof
let a, b be object of F1(); ::_thesis: ( <^a,b^> <> {} implies for f, g being Morphism of a,b st F4(a,b,f) = F4(a,b,g) holds
f = g )
assume A15: <^a,b^> <> {} ; ::_thesis: for f, g being Morphism of a,b st F4(a,b,f) = F4(a,b,g) holds
f = g
let f, g be Morphism of a,b; ::_thesis: ( F4(a,b,f) = F4(a,b,g) implies f = g )
A16: @ g = g by A15, Def7;
then A17: P1[ latt a, latt b, @ g] by A1, A15;
A18: @ f = f by A15, Def7;
then P1[ latt a, latt b, @ f] by A1, A15;
hence ( F4(a,b,f) = F4(a,b,g) implies f = g ) by A5, A18, A16, A17; ::_thesis: verum
end;
A19: ex F being covariant Functor of F1(),F2() st
( ( for a being object of F1() holds F . a = F3(a) ) & ( for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F4(a,b,f) ) ) by A3;
thus F1(),F2() are_isomorphic from YELLOW18:sch_11(A19, A7, A14, A8); ::_thesis: verum
end;
scheme :: YELLOW21:sch 9
CLCatAntiIsomorphism{ P1[ set , set , set ], P2[ set , set , set ], F1() -> lattice-wise category, F2() -> lattice-wise category, F3( set ) -> LATTICE, F4( set , set , set ) -> Function } :
F1(),F2() are_anti-isomorphic
provided
A1: for a, b being LATTICE
for f being Function of a,b holds
( f in the Arrows of F1() . (a,b) iff ( a in the carrier of F1() & b in the carrier of F1() & P1[a,b,f] ) ) and
A2: for a, b being LATTICE
for f being Function of a,b holds
( f in the Arrows of F2() . (a,b) iff ( a in the carrier of F2() & b in the carrier of F2() & P2[a,b,f] ) ) and
A3: ex F being contravariant Functor of F1(),F2() st
( ( for a being object of F1() holds F . a = F3(a) ) & ( for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F4(a,b,f) ) ) and
A4: for a, b being LATTICE st a in the carrier of F1() & b in the carrier of F1() & F3(a) = F3(b) holds
a = b and
A5: for a, b being LATTICE
for f, g being Function of a,b st F4(a,b,f) = F4(a,b,g) holds
f = g and
A6: for a, b being LATTICE
for f being Function of a,b st P2[a,b,f] holds
ex c, d being LATTICE ex g being Function of c,d st
( c in the carrier of F1() & d in the carrier of F1() & P1[c,d,g] & b = F3(c) & a = F3(d) & f = F4(c,d,g) )
proof
A7: for a, b being object of F1() st F3(a) = F3(b) holds
a = b
proof
let a, b be object of F1(); ::_thesis: ( F3(a) = F3(b) implies a = b )
( a = latt a & b = latt b ) ;
hence ( F3(a) = F3(b) implies a = b ) by A4; ::_thesis: verum
end;
A8: now__::_thesis:_for_a,_b_being_object_of_F2()_st_<^a,b^>_<>_{}_holds_
for_f_being_Morphism_of_a,b_ex_c,_d_being_object_of_F1()_ex_g_being_Morphism_of_c,d_st_
(_b_=_F3(c)_&_a_=_F3(d)_&_<^c,d^>_<>_{}_&_f_=_F4(c,d,g)_)
let a, b be object of F2(); ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b ex c, d being object of F1() ex g being Morphism of c,d st
( b = F3(c) & a = F3(d) & <^c,d^> <> {} & f = F4(c,d,g) ) )
assume A9: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b ex c, d being object of F1() ex g being Morphism of c,d st
( b = F3(c) & a = F3(d) & <^c,d^> <> {} & f = F4(c,d,g) )
let f be Morphism of a,b; ::_thesis: ex c, d being object of F1() ex g being Morphism of c,d st
( b = F3(c) & a = F3(d) & <^c,d^> <> {} & f = F4(c,d,g) )
A10: @ f = f by A9, Def7;
then P2[ latt a, latt b, @ f] by A2, A9;
then consider c, d being LATTICE, g being Function of c,d such that
A11: ( c in the carrier of F1() & d in the carrier of F1() ) and
A12: P1[c,d,g] and
A13: ( latt b = F3(c) & latt a = F3(d) & @ f = F4(c,d,g) ) by A6;
reconsider c9 = c, d9 = d as object of F1() by A11;
g in <^c9,d9^> by A1, A12;
hence ex c, d being object of F1() ex g being Morphism of c,d st
( b = F3(c) & a = F3(d) & <^c,d^> <> {} & f = F4(c,d,g) ) by A10, A13; ::_thesis: verum
end;
A14: for a, b being object of F1() st <^a,b^> <> {} holds
for f, g being Morphism of a,b st F4(a,b,f) = F4(a,b,g) holds
f = g
proof
let a, b be object of F1(); ::_thesis: ( <^a,b^> <> {} implies for f, g being Morphism of a,b st F4(a,b,f) = F4(a,b,g) holds
f = g )
assume A15: <^a,b^> <> {} ; ::_thesis: for f, g being Morphism of a,b st F4(a,b,f) = F4(a,b,g) holds
f = g
let f, g be Morphism of a,b; ::_thesis: ( F4(a,b,f) = F4(a,b,g) implies f = g )
( @ f = f & @ g = g ) by A15, Def7;
hence ( F4(a,b,f) = F4(a,b,g) implies f = g ) by A5; ::_thesis: verum
end;
A16: ex F being contravariant Functor of F1(),F2() st
( ( for a being object of F1() holds F . a = F3(a) ) & ( for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F4(a,b,f) ) ) by A3;
thus F1(),F2() are_anti-isomorphic from YELLOW18:sch_13(A16, A7, A14, A8); ::_thesis: verum
end;
begin
definition
let C be lattice-wise category;
attrC is with_all_isomorphisms means :Def8: :: YELLOW21:def 8
for a, b being object of C
for f being Function of (latt a),(latt b) st f is isomorphic holds
f in <^a,b^>;
end;
:: deftheorem Def8 defines with_all_isomorphisms YELLOW21:def_8_:_
for C being lattice-wise category holds
( C is with_all_isomorphisms iff for a, b being object of C
for f being Function of (latt a),(latt b) st f is isomorphic holds
f in <^a,b^> );
registration
cluster non empty transitive strict semi-functional V110() with_units reflexive para-functional set-id-inheriting concrete carrier-underlaid lattice-wise with_all_isomorphisms for AltCatStr ;
existence
ex b1 being strict lattice-wise category st b1 is with_all_isomorphisms
proof
defpred S1[ set , set , set ] means c3 = c3;
set L = the LATTICE;
A1: for a, b, c being LATTICE st a in { the LATTICE} & b in { the LATTICE} & c in { the LATTICE} holds
for f being Function of a,b
for g being Function of b,c st S1[a,b,f] & S1[b,c,g] holds
S1[a,c,g * f] ;
A2: for a being LATTICE st a in { the LATTICE} holds
S1[a,a, id a] ;
A3: for a being Element of { the LATTICE} holds a is LATTICE by TARSKI:def_1;
consider C being strict category such that
A4: C is lattice-wise and
A5: ( the carrier of C = { the LATTICE} & ( for a, b being LATTICE
for f being monotone Function of a,b holds
( f in the Arrows of C . (a,b) iff ( a in { the LATTICE} & b in { the LATTICE} & S1[a,b,f] ) ) ) ) from YELLOW21:sch_1(A3, A1, A2);
reconsider C = C as strict lattice-wise category by A4;
take C ; ::_thesis: C is with_all_isomorphisms
let a, b be object of C; :: according to YELLOW21:def_8 ::_thesis: for f being Function of (latt a),(latt b) st f is isomorphic holds
f in <^a,b^>
let f be Function of (latt a),(latt b); ::_thesis: ( f is isomorphic implies f in <^a,b^> )
thus ( f is isomorphic implies f in <^a,b^> ) by A5; ::_thesis: verum
end;
end;
theorem :: YELLOW21:4
for C being lattice-wise with_all_isomorphisms category
for a, b being object of C
for f being Morphism of a,b st @ f is isomorphic holds
f is iso
proof
let C be lattice-wise with_all_isomorphisms category; ::_thesis: for a, b being object of C
for f being Morphism of a,b st @ f is isomorphic holds
f is iso
let a, b be object of C; ::_thesis: for f being Morphism of a,b st @ f is isomorphic holds
f is iso
let f be Morphism of a,b; ::_thesis: ( @ f is isomorphic implies f is iso )
assume A1: @ f is isomorphic ; ::_thesis: f is iso
then consider g being monotone Function of (latt b),(latt a) such that
A2: (@ f) * g = id (latt b) and
A3: g * (@ f) = id (latt a) by YELLOW16:15;
A4: @ f in <^a,b^> by A1, Def8;
A5: g is isomorphic by A2, A3, YELLOW16:15;
then A6: g in <^b,a^> by Def8;
reconsider g = g as Morphism of b,a by A5, Def8;
A7: @ g = g by A6, Def7;
idm b = id (latt b) by Th2;
then A8: f * g = idm b by A2, A4, A6, A7, Th3;
then A9: g is_right_inverse_of f by ALTCAT_3:def_1;
idm a = id (latt a) by Th2;
then A10: g * f = idm a by A3, A4, A6, A7, Th3;
then A11: g is_left_inverse_of f by ALTCAT_3:def_1;
then ( f is retraction & f is coretraction ) by A9, ALTCAT_3:def_2, ALTCAT_3:def_3;
hence ( f * (f ") = idm b & (f ") * f = idm a ) by A4, A6, A8, A10, A11, A9, ALTCAT_3:def_4; :: according to ALTCAT_3:def_5 ::_thesis: verum
end;
theorem :: YELLOW21:5
for C being lattice-wise category
for a, b being object of C st <^a,b^> <> {} & <^b,a^> <> {} holds
for f being Morphism of a,b st f is iso holds
@ f is isomorphic
proof
let C be lattice-wise category; ::_thesis: for a, b being object of C st <^a,b^> <> {} & <^b,a^> <> {} holds
for f being Morphism of a,b st f is iso holds
@ f is isomorphic
let a, b be object of C; ::_thesis: ( <^a,b^> <> {} & <^b,a^> <> {} implies for f being Morphism of a,b st f is iso holds
@ f is isomorphic )
assume A1: ( <^a,b^> <> {} & <^b,a^> <> {} ) ; ::_thesis: for f being Morphism of a,b st f is iso holds
@ f is isomorphic
let f be Morphism of a,b; ::_thesis: ( f is iso implies @ f is isomorphic )
assume A2: ( f * (f ") = idm b & (f ") * f = idm a ) ; :: according to ALTCAT_3:def_5 ::_thesis: @ f is isomorphic
A3: ( idm a = id (latt a) & idm b = id (latt b) ) by Th2;
( (@ f) * (@ (f ")) = f * (f ") & (@ (f ")) * (@ f) = (f ") * f ) by A1, Th3;
hence @ f is isomorphic by A2, A3, YELLOW16:15; ::_thesis: verum
end;
scheme :: YELLOW21:sch 10
CLCatEquivalence{ P1[ set , set , set ], P2[ set , set , set ], F1() -> lattice-wise category, F2() -> lattice-wise category, F3( set ) -> LATTICE, F4( set ) -> LATTICE, F5( set , set , set ) -> Function, F6( set , set , set ) -> Function, F7( set ) -> Function, F8( set ) -> Function } :
F1(),F2() are_equivalent
provided
A1: for a, b being object of F1()
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P1[ latt a, latt b,f] ) and
A2: for a, b being object of F2()
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P2[ latt a, latt b,f] ) and
A3: ex F being covariant Functor of F1(),F2() st
( ( for a being object of F1() holds F . a = F3(a) ) & ( for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F5(a,b,f) ) ) and
A4: ex G being covariant Functor of F2(),F1() st
( ( for a being object of F2() holds G . a = F4(a) ) & ( for a, b being object of F2() st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . f = F6(a,b,f) ) ) and
A5: for a being LATTICE st a in the carrier of F1() holds
ex f being monotone Function of F4(F3(a)),a st
( f = F7(a) & f is isomorphic & P1[F4(F3(a)),a,f] & P1[a,F4(F3(a)),f " ] ) and
A6: for a being LATTICE st a in the carrier of F2() holds
ex f being monotone Function of a,F3(F4(a)) st
( f = F8(a) & f is isomorphic & P2[a,F3(F4(a)),f] & P2[F3(F4(a)),a,f " ] ) and
A7: for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F7(b) * F6(F3(a),F3(b),F5(a,b,f)) = (@ f) * F7(a) and
A8: for a, b being object of F2() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F5(F4(a),F4(b),F6(a,b,f)) * F8(a) = F8(b) * (@ f)
proof
A9: ex G being covariant Functor of F2(),F1() st
( ( for a being object of F2() holds G . a = F4(a) ) & ( for a, b being object of F2() st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . f = F6(a,b,f) ) ) by A4;
A10: for a, b being object of F2() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F5(F4(a),F4(b),F6(a,b,f)) * F8(a) = F8(b) * f
proof
let a, b be object of F2(); ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds F5(F4(a),F4(b),F6(a,b,f)) * F8(a) = F8(b) * f )
assume A11: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b holds F5(F4(a),F4(b),F6(a,b,f)) * F8(a) = F8(b) * f
let f be Morphism of a,b; ::_thesis: F5(F4(a),F4(b),F6(a,b,f)) * F8(a) = F8(b) * f
@ f = f by A11, Def7;
hence F5(F4(a),F4(b),F6(a,b,f)) * F8(a) = F8(b) * f by A8, A11; ::_thesis: verum
end;
A12: for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F7(b) * F6(F3(a),F3(b),F5(a,b,f)) = f * F7(a)
proof
let a, b be object of F1(); ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds F7(b) * F6(F3(a),F3(b),F5(a,b,f)) = f * F7(a) )
assume A13: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b holds F7(b) * F6(F3(a),F3(b),F5(a,b,f)) = f * F7(a)
let f be Morphism of a,b; ::_thesis: F7(b) * F6(F3(a),F3(b),F5(a,b,f)) = f * F7(a)
@ f = f by A13, Def7;
hence F7(b) * F6(F3(a),F3(b),F5(a,b,f)) = f * F7(a) by A7, A13; ::_thesis: verum
end;
A14: for a, b being object of F2() st b = F3(F4(a)) holds
( F8(a) in <^a,b^> & F8(a) " in <^b,a^> & F8(a) is one-to-one )
proof
let a, b be object of F2(); ::_thesis: ( b = F3(F4(a)) implies ( F8(a) in <^a,b^> & F8(a) " in <^b,a^> & F8(a) is one-to-one ) )
assume A15: b = F3(F4(a)) ; ::_thesis: ( F8(a) in <^a,b^> & F8(a) " in <^b,a^> & F8(a) is one-to-one )
consider f being monotone Function of (latt a),F3(F4(a)) such that
A16: f = F8(a) and
A17: f is isomorphic and
A18: P2[ latt a,F3(F4(a)),f] and
A19: P2[F3(F4(a)), latt a,f " ] by A6;
A20: latt b = b ;
hence F8(a) in <^a,b^> by A2, A15, A16, A18; ::_thesis: ( F8(a) " in <^b,a^> & F8(a) is one-to-one )
ex g being Function of F3(F4(a)),(latt a) st
( g = f " & g is monotone ) by A17, WAYBEL_0:def_38;
hence F8(a) " in <^b,a^> by A2, A15, A20, A16, A19; ::_thesis: F8(a) is one-to-one
thus F8(a) is one-to-one by A16, A17; ::_thesis: verum
end;
A21: for a, b being object of F1() st a = F4(F3(b)) holds
( F7(b) in <^a,b^> & F7(b) " in <^b,a^> & F7(b) is one-to-one )
proof
let a, b be object of F1(); ::_thesis: ( a = F4(F3(b)) implies ( F7(b) in <^a,b^> & F7(b) " in <^b,a^> & F7(b) is one-to-one ) )
assume A22: a = F4(F3(b)) ; ::_thesis: ( F7(b) in <^a,b^> & F7(b) " in <^b,a^> & F7(b) is one-to-one )
consider f being monotone Function of F4(F3(b)),(latt b) such that
A23: f = F7(b) and
A24: f is isomorphic and
A25: P1[F4(F3(b)), latt b,f] and
A26: P1[ latt b,F4(F3(b)),f " ] by A5;
A27: latt a = a ;
hence F7(b) in <^a,b^> by A1, A22, A23, A25; ::_thesis: ( F7(b) " in <^b,a^> & F7(b) is one-to-one )
ex g being Function of (latt b),F4(F3(b)) st
( g = f " & g is monotone ) by A24, WAYBEL_0:def_38;
hence F7(b) " in <^b,a^> by A1, A22, A27, A23, A26; ::_thesis: F7(b) is one-to-one
thus F7(b) is one-to-one by A23, A24; ::_thesis: verum
end;
A28: ex F being covariant Functor of F1(),F2() st
( ( for a being object of F1() holds F . a = F3(a) ) & ( for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F5(a,b,f) ) ) by A3;
thus F1(),F2() are_equivalent from YELLOW18:sch_22(A28, A9, A21, A14, A12, A10); ::_thesis: verum
end;
begin
definition
let R be Relation;
attrR is upper-bounded means :Def9: :: YELLOW21:def 9
ex x being set st
for y being set st y in field R holds
[y,x] in R;
end;
:: deftheorem Def9 defines upper-bounded YELLOW21:def_9_:_
for R being Relation holds
( R is upper-bounded iff ex x being set st
for y being set st y in field R holds
[y,x] in R );
Lm1: for x, X being set holds
( x in X iff X = (X \ {x}) \/ {x} )
proof
let x, X be set ; ::_thesis: ( x in X iff X = (X \ {x}) \/ {x} )
( x in X iff {x} c= X ) by ZFMISC_1:31;
hence ( x in X iff X = (X \ {x}) \/ {x} ) by XBOOLE_1:7, XBOOLE_1:45; ::_thesis: verum
end;
registration
cluster Relation-like well-ordering -> well_founded reflexive antisymmetric connected transitive for set ;
coherence
for b1 being Relation st b1 is well-ordering holds
( b1 is reflexive & b1 is transitive & b1 is antisymmetric & b1 is connected & b1 is well_founded ) ;
end;
registration
cluster Relation-like well-ordering for set ;
existence
ex b1 being Relation st b1 is well-ordering
proof
consider r being Relation such that
A1: r well_orders 5 by WELLORD2:17;
take r |_2 5 ; ::_thesis: r |_2 5 is well-ordering
thus r |_2 5 is well-ordering by A1, WELLORD2:16; ::_thesis: verum
end;
end;
theorem Th6: :: YELLOW21:6
for x, y being set
for f being one-to-one Function
for R being Relation holds
( [x,y] in (f * R) * (f ") iff ( x in dom f & y in dom f & [(f . x),(f . y)] in R ) )
proof
let x, y be set ; ::_thesis: for f being one-to-one Function
for R being Relation holds
( [x,y] in (f * R) * (f ") iff ( x in dom f & y in dom f & [(f . x),(f . y)] in R ) )
let f be one-to-one Function; ::_thesis: for R being Relation holds
( [x,y] in (f * R) * (f ") iff ( x in dom f & y in dom f & [(f . x),(f . y)] in R ) )
let R be Relation; ::_thesis: ( [x,y] in (f * R) * (f ") iff ( x in dom f & y in dom f & [(f . x),(f . y)] in R ) )
A1: rng f = dom (f ") by FUNCT_1:33;
A2: dom f = rng (f ") by FUNCT_1:33;
hereby ::_thesis: ( x in dom f & y in dom f & [(f . x),(f . y)] in R implies [x,y] in (f * R) * (f ") )
assume [x,y] in (f * R) * (f ") ; ::_thesis: ( x in dom f & y in dom f & [(f . x),(f . y)] in R )
then consider a being set such that
A3: [x,a] in f * R and
A4: [a,y] in f " by RELAT_1:def_8;
A5: ( y = (f ") . a & a in rng f ) by A1, A4, FUNCT_1:1;
consider b being set such that
A6: [x,b] in f and
A7: [b,a] in R by A3, RELAT_1:def_8;
thus ( x in dom f & y in dom f ) by A2, A4, A6, XTUPLE_0:def_12, XTUPLE_0:def_13; ::_thesis: [(f . x),(f . y)] in R
b = f . x by A6, FUNCT_1:1;
hence [(f . x),(f . y)] in R by A7, A5, FUNCT_1:35; ::_thesis: verum
end;
assume that
A8: x in dom f and
A9: y in dom f and
A10: [(f . x),(f . y)] in R ; ::_thesis: [x,y] in (f * R) * (f ")
( (f ") . (f . y) = y & f . y in rng f ) by A9, FUNCT_1:34, FUNCT_1:def_3;
then A11: [(f . y),y] in f " by A1, FUNCT_1:1;
[x,(f . x)] in f by A8, FUNCT_1:1;
then [x,(f . y)] in f * R by A10, RELAT_1:def_8;
hence [x,y] in (f * R) * (f ") by A11, RELAT_1:def_8; ::_thesis: verum
end;
registration
let f be one-to-one Function;
let R be reflexive Relation;
cluster(f * R) * (f ") -> reflexive ;
coherence
(f * R) * (f ") is reflexive
proof
let x be set ; :: according to RELAT_2:def_1,RELAT_2:def_9 ::_thesis: ( not x in field ((f * R) * (f ")) or [x,x] in (f * R) * (f ") )
A1: R is_reflexive_in field R by RELAT_2:def_9;
assume x in field ((f * R) * (f ")) ; ::_thesis: [x,x] in (f * R) * (f ")
then A2: x in (dom ((f * R) * (f "))) \/ (rng ((f * R) * (f "))) by RELAT_1:def_6;
percases ( x in dom ((f * R) * (f ")) or x in rng ((f * R) * (f ")) ) by A2, XBOOLE_0:def_3;
suppose x in dom ((f * R) * (f ")) ; ::_thesis: [x,x] in (f * R) * (f ")
then consider y being set such that
A3: [x,y] in (f * R) * (f ") by XTUPLE_0:def_12;
[(f . x),(f . y)] in R by A3, Th6;
then f . x in field R by RELAT_1:15;
then A4: [(f . x),(f . x)] in R by A1, RELAT_2:def_1;
x in dom f by A3, Th6;
hence [x,x] in (f * R) * (f ") by A4, Th6; ::_thesis: verum
end;
suppose x in rng ((f * R) * (f ")) ; ::_thesis: [x,x] in (f * R) * (f ")
then consider y being set such that
A5: [y,x] in (f * R) * (f ") by XTUPLE_0:def_13;
[(f . y),(f . x)] in R by A5, Th6;
then f . x in field R by RELAT_1:15;
then A6: [(f . x),(f . x)] in R by A1, RELAT_2:def_1;
x in dom f by A5, Th6;
hence [x,x] in (f * R) * (f ") by A6, Th6; ::_thesis: verum
end;
end;
end;
end;
registration
let f be one-to-one Function;
let R be antisymmetric Relation;
cluster(f * R) * (f ") -> antisymmetric ;
coherence
(f * R) * (f ") is antisymmetric
proof
let x, y be set ; :: according to RELAT_2:def_4,RELAT_2:def_12 ::_thesis: ( not x in field ((f * R) * (f ")) or not y in field ((f * R) * (f ")) or not [x,y] in (f * R) * (f ") or not [y,x] in (f * R) * (f ") or x = y )
assume that
x in field ((f * R) * (f ")) and
y in field ((f * R) * (f ")) ; ::_thesis: ( not [x,y] in (f * R) * (f ") or not [y,x] in (f * R) * (f ") or x = y )
assume that
A1: [x,y] in (f * R) * (f ") and
A2: [y,x] in (f * R) * (f ") ; ::_thesis: x = y
A3: ( x in dom f & y in dom f ) by A1, Th6;
A4: R is_antisymmetric_in field R by RELAT_2:def_12;
A5: [(f . y),(f . x)] in R by A2, Th6;
A6: [(f . x),(f . y)] in R by A1, Th6;
then ( f . x in field R & f . y in field R ) by RELAT_1:15;
then f . x = f . y by A6, A5, A4, RELAT_2:def_4;
hence x = y by A3, FUNCT_1:def_4; ::_thesis: verum
end;
end;
registration
let f be one-to-one Function;
let R be transitive Relation;
cluster(f * R) * (f ") -> transitive ;
coherence
(f * R) * (f ") is transitive
proof
let x, y, z be set ; :: according to RELAT_2:def_8,RELAT_2:def_16 ::_thesis: ( not x in field ((f * R) * (f ")) or not y in field ((f * R) * (f ")) or not z in field ((f * R) * (f ")) or not [x,y] in (f * R) * (f ") or not [y,z] in (f * R) * (f ") or [x,z] in (f * R) * (f ") )
assume that
x in field ((f * R) * (f ")) and
y in field ((f * R) * (f ")) and
z in field ((f * R) * (f ")) ; ::_thesis: ( not [x,y] in (f * R) * (f ") or not [y,z] in (f * R) * (f ") or [x,z] in (f * R) * (f ") )
assume that
A1: [x,y] in (f * R) * (f ") and
A2: [y,z] in (f * R) * (f ") ; ::_thesis: [x,z] in (f * R) * (f ")
A3: ( x in dom f & z in dom f ) by A1, A2, Th6;
A4: [(f . y),(f . z)] in R by A2, Th6;
then A5: f . z in field R by RELAT_1:15;
A6: R is_transitive_in field R by RELAT_2:def_16;
A7: [(f . x),(f . y)] in R by A1, Th6;
then ( f . x in field R & f . y in field R ) by RELAT_1:15;
then [(f . x),(f . z)] in R by A7, A4, A5, A6, RELAT_2:def_8;
hence [x,z] in (f * R) * (f ") by A3, Th6; ::_thesis: verum
end;
end;
theorem Th7: :: YELLOW21:7
for X being set
for A being Ordinal st X,A are_equipotent holds
ex R being Order of X st
( R well_orders X & order_type_of R = A )
proof
let X be set ; ::_thesis: for A being Ordinal st X,A are_equipotent holds
ex R being Order of X st
( R well_orders X & order_type_of R = A )
let A be Ordinal; ::_thesis: ( X,A are_equipotent implies ex R being Order of X st
( R well_orders X & order_type_of R = A ) )
given f being Function such that A1: f is one-to-one and
A2: dom f = X and
A3: rng f = A ; :: according to WELLORD2:def_4 ::_thesis: ex R being Order of X st
( R well_orders X & order_type_of R = A )
reconsider f = f as Function of X,A by A2, A3, FUNCT_2:2;
reconsider g = f " as Function of A,X by A1, A3, FUNCT_2:25;
A4: dom g = A by A1, A3, FUNCT_1:33;
reconsider f9 = f as one-to-one Function by A1;
A5: dom (RelIncl A) = A by ORDERS_1:14;
rng (RelIncl A) = A by ORDERS_1:14;
then A6: rng (f * (RelIncl A)) = A by A3, A5, RELAT_1:28;
set R = (f * (RelIncl A)) * g;
dom (f * (RelIncl A)) = X by A2, A3, A5, RELAT_1:27;
then A7: dom ((f * (RelIncl A)) * g) = X by A4, A6, RELAT_1:27;
rng g = X by A1, A2, FUNCT_1:33;
then rng ((f * (RelIncl A)) * g) = X by A4, A6, RELAT_1:28;
then A8: field ((f * (RelIncl A)) * g) = X \/ X by A7, RELAT_1:def_6
.= X ;
reconsider R = (f * (RelIncl A)) * g as Relation of X ;
(f9 * (RelIncl A)) * (f9 ") is_reflexive_in X by A8, RELAT_2:def_9;
then reconsider R = R as Order of X by A7, PARTFUN1:def_2;
A9: f is_isomorphism_of R, RelIncl A
proof
thus ( dom f = field R & rng f = field (RelIncl A) & f is one-to-one ) by A1, A2, A3, A8, WELLORD2:def_1; :: according to WELLORD1:def_7 ::_thesis: for b1, b2 being set holds
( ( not [b1,b2] in R or ( b1 in field R & b2 in field R & [(f . b1),(f . b2)] in RelIncl A ) ) & ( not b1 in field R or not b2 in field R or not [(f . b1),(f . b2)] in RelIncl A or [b1,b2] in R ) )
let a, b be set ; ::_thesis: ( ( not [a,b] in R or ( a in field R & b in field R & [(f . a),(f . b)] in RelIncl A ) ) & ( not a in field R or not b in field R or not [(f . a),(f . b)] in RelIncl A or [a,b] in R ) )
hereby ::_thesis: ( not a in field R or not b in field R or not [(f . a),(f . b)] in RelIncl A or [a,b] in R )
assume A10: [a,b] in R ; ::_thesis: ( a in field R & b in field R & [(f . a),(f . b)] in RelIncl A )
hence ( a in field R & b in field R ) by RELAT_1:15; ::_thesis: [(f . a),(f . b)] in RelIncl A
consider x being set such that
A11: [a,x] in f * (RelIncl A) and
A12: [x,b] in g by A10, RELAT_1:def_8;
A13: ( b = g . x & x in dom g ) by A12, FUNCT_1:1;
consider y being set such that
A14: [a,y] in f and
A15: [y,x] in RelIncl A by A11, RELAT_1:def_8;
y = f . a by A14, FUNCT_1:1;
hence [(f . a),(f . b)] in RelIncl A by A1, A3, A15, A13, FUNCT_1:35; ::_thesis: verum
end;
assume that
A16: a in field R and
A17: b in field R and
A18: [(f . a),(f . b)] in RelIncl A ; ::_thesis: [a,b] in R
[a,(f . a)] in f by A2, A8, A16, FUNCT_1:1;
then A19: [a,(f . b)] in f * (RelIncl A) by A18, RELAT_1:def_8;
( (f ") . (f . b) = b & f . b in A ) by A1, A2, A3, A8, A17, FUNCT_1:34, FUNCT_1:def_3;
then [(f . b),b] in g by A4, FUNCT_1:1;
hence [a,b] in R by A19, RELAT_1:def_8; ::_thesis: verum
end;
then f " is_isomorphism_of RelIncl A,R by WELLORD1:39;
then ( R is connected & R is well_founded ) by WELLORD1:43;
then A20: ( R is_connected_in X & R is_well_founded_in X ) by A8, RELAT_2:def_14, WELLORD1:3;
take R ; ::_thesis: ( R well_orders X & order_type_of R = A )
A21: R is_antisymmetric_in X by A8, RELAT_2:def_12;
( R is_reflexive_in X & R is_transitive_in X ) by A8, RELAT_2:def_9, RELAT_2:def_16;
hence R well_orders X by A21, A20, WELLORD1:def_5; ::_thesis: order_type_of R = A
then A22: R is well-ordering by A8, WELLORD1:4;
R, RelIncl A are_isomorphic by A9, WELLORD1:def_8;
hence order_type_of R = A by A22, WELLORD2:def_2; ::_thesis: verum
end;
registration
let X be non empty set ;
cluster Relation-like X -defined X -valued well-ordering V16(X) quasi_total reflexive antisymmetric transitive upper-bounded for Element of bool [:X,X:];
existence
ex b1 being Order of X st
( b1 is upper-bounded & b1 is well-ordering )
proof
set x = the Element of X;
A1: ( X \ { the Element of X}, card (X \ { the Element of X}) are_equipotent & { the Element of X},{(card (X \ { the Element of X}))} are_equipotent ) by CARD_1:28, CARD_1:def_2;
A2: succ (card (X \ { the Element of X})) = (card (X \ { the Element of X})) \/ {(card (X \ { the Element of X}))} by ORDINAL1:def_1;
not card (X \ { the Element of X}) in card (X \ { the Element of X}) ;
then A3: {(card (X \ { the Element of X}))} misses card (X \ { the Element of X}) by ZFMISC_1:50;
( { the Element of X} misses X \ { the Element of X} & X = (X \ { the Element of X}) \/ { the Element of X} ) by Lm1, XBOOLE_1:79;
then consider r being Order of X such that
A4: r well_orders X and
A5: order_type_of r = succ (card (X \ { the Element of X})) by A1, A3, A2, Th7, CARD_1:31;
take r ; ::_thesis: ( r is upper-bounded & r is well-ordering )
A6: field r = X by ORDERS_1:15;
then r is well-ordering by A4, WELLORD1:4;
then r, RelIncl (order_type_of r) are_isomorphic by WELLORD2:def_2;
then RelIncl (order_type_of r),r are_isomorphic by WELLORD1:40;
then consider f being Function such that
A7: f is_isomorphism_of RelIncl (order_type_of r),r by WELLORD1:def_8;
A8: f is one-to-one by A7, WELLORD1:def_7;
A9: rng f = X by A6, A7, WELLORD1:def_7;
field (RelIncl (order_type_of r)) = order_type_of r by WELLORD2:def_1;
then A10: dom f = order_type_of r by A7, WELLORD1:def_7;
thus r is upper-bounded ::_thesis: r is well-ordering
proof
take a = f . (card (X \ { the Element of X})); :: according to YELLOW21:def_9 ::_thesis: for y being set st y in field r holds
[y,a] in r
let y be set ; ::_thesis: ( y in field r implies [y,a] in r )
A11: card (X \ { the Element of X}) in order_type_of r by A2, A5, ZFMISC_1:136;
assume A12: y in field r ; ::_thesis: [y,a] in r
then A13: (f ") . y in order_type_of r by A6, A8, A10, A9, FUNCT_1:32;
then reconsider b = (f ") . y as Ordinal ;
( (f ") . y in card (X \ { the Element of X}) or (f ") . y = card (X \ { the Element of X}) ) by A2, A5, A13, ZFMISC_1:136;
then b c= card (X \ { the Element of X}) by ORDINAL1:def_2;
then [b,(card (X \ { the Element of X}))] in RelIncl (order_type_of r) by A13, A11, WELLORD2:def_1;
then [(f . b),a] in r by A7, WELLORD1:def_7;
hence [y,a] in r by A6, A8, A9, A12, FUNCT_1:35; ::_thesis: verum
end;
thus r is well-ordering by A4, A6, WELLORD1:4; ::_thesis: verum
end;
end;
theorem Th8: :: YELLOW21:8
for P being non empty reflexive RelStr holds
( P is upper-bounded iff the InternalRel of P is upper-bounded )
proof
let P be non empty reflexive RelStr ; ::_thesis: ( P is upper-bounded iff the InternalRel of P is upper-bounded )
the carrier of P \/ the carrier of P = the carrier of P ;
then A1: field the InternalRel of P c= the carrier of P by RELSET_1:8;
thus ( P is upper-bounded implies the InternalRel of P is upper-bounded ) ::_thesis: ( the InternalRel of P is upper-bounded implies P is upper-bounded )
proof
given x being Element of P such that A2: x is_>=_than the carrier of P ; :: according to YELLOW_0:def_5 ::_thesis: the InternalRel of P is upper-bounded
take x ; :: according to YELLOW21:def_9 ::_thesis: for y being set st y in field the InternalRel of P holds
[y,x] in the InternalRel of P
let y be set ; ::_thesis: ( y in field the InternalRel of P implies [y,x] in the InternalRel of P )
assume y in field the InternalRel of P ; ::_thesis: [y,x] in the InternalRel of P
then reconsider y = y as Element of P by A1;
x >= y by A2, LATTICE3:def_9;
hence [y,x] in the InternalRel of P by ORDERS_2:def_5; ::_thesis: verum
end;
set y = the Element of P;
given x being set such that A3: for y being set st y in field the InternalRel of P holds
[y,x] in the InternalRel of P ; :: according to YELLOW21:def_9 ::_thesis: P is upper-bounded
the Element of P <= the Element of P ;
then [ the Element of P, the Element of P] in the InternalRel of P by ORDERS_2:def_5;
then the Element of P in field the InternalRel of P by RELAT_1:15;
then [ the Element of P,x] in the InternalRel of P by A3;
then x in field the InternalRel of P by RELAT_1:15;
then reconsider x = x as Element of P by A1;
take x ; :: according to YELLOW_0:def_5 ::_thesis: the carrier of P is_<=_than x
let y be Element of P; :: according to LATTICE3:def_9 ::_thesis: ( not y in the carrier of P or y <= x )
y <= y ;
then [y,y] in the InternalRel of P by ORDERS_2:def_5;
then y in field the InternalRel of P by RELAT_1:15;
then [y,x] in the InternalRel of P by A3;
hence ( not y in the carrier of P or y <= x ) by ORDERS_2:def_5; ::_thesis: verum
end;
theorem Th9: :: YELLOW21:9
for P being non empty upper-bounded Poset st the InternalRel of P is well-ordering holds
( P is connected & P is complete & P is continuous )
proof
let P be non empty upper-bounded Poset; ::_thesis: ( the InternalRel of P is well-ordering implies ( P is connected & P is complete & P is continuous ) )
assume A1: the InternalRel of P is well-ordering ; ::_thesis: ( P is connected & P is complete & P is continuous )
A2: field the InternalRel of P = the carrier of P by ORDERS_1:15;
thus A3: P is connected ::_thesis: ( P is complete & P is continuous )
proof
let x, y be Element of P; :: according to WAYBEL_0:def_29 ::_thesis: ( x <= y or y <= x )
A4: ( x = y or x <> y ) ;
( the InternalRel of P is_connected_in the carrier of P & the InternalRel of P is_reflexive_in the carrier of P ) by A1, A2, RELAT_2:def_9, RELAT_2:def_14;
then ( [x,y] in the InternalRel of P or [y,x] in the InternalRel of P ) by A4, RELAT_2:def_1, RELAT_2:def_6;
hence ( x <= y or y <= x ) by ORDERS_2:def_5; ::_thesis: verum
end;
thus P is complete ::_thesis: P is continuous
proof
set y = the Element of P;
let X be set ; :: according to LATTICE3:def_12 ::_thesis: ex b1 being Element of the carrier of P st
( X is_<=_than b1 & ( for b2 being Element of the carrier of P holds
( not X is_<=_than b2 or b1 <= b2 ) ) )
defpred S1[ set ] means for y being Element of P st y in X holds
[y,$1] in the InternalRel of P;
consider Y being set such that
A5: for x being set holds
( x in Y iff ( x in the carrier of P & S1[x] ) ) from XBOOLE_0:sch_1();
A6: Y c= the carrier of P
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in the carrier of P )
thus ( not x in Y or x in the carrier of P ) by A5; ::_thesis: verum
end;
the InternalRel of P is upper-bounded by Th8;
then consider x being set such that
A7: for y being set st y in field the InternalRel of P holds
[y,x] in the InternalRel of P by Def9;
[ the Element of P,x] in the InternalRel of P by A2, A7;
then reconsider x = x as Element of P by A2, RELAT_1:15;
for y being Element of P st y in X holds
[y,x] in the InternalRel of P by A2, A7;
then x in Y by A5;
then consider a being set such that
A8: a in Y and
A9: for b being set st b in Y holds
[a,b] in the InternalRel of P by A1, A2, A6, WELLORD1:6;
reconsider a = a as Element of P by A6, A8;
take a ; ::_thesis: ( X is_<=_than a & ( for b1 being Element of the carrier of P holds
( not X is_<=_than b1 or a <= b1 ) ) )
hereby :: according to LATTICE3:def_9 ::_thesis: for b1 being Element of the carrier of P holds
( not X is_<=_than b1 or a <= b1 )
let y be Element of P; ::_thesis: ( y in X implies y <= a )
assume y in X ; ::_thesis: y <= a
then [y,a] in the InternalRel of P by A5, A8;
hence y <= a by ORDERS_2:def_5; ::_thesis: verum
end;
let b be Element of P; ::_thesis: ( not X is_<=_than b or a <= b )
assume A10: for c being Element of P st c in X holds
c <= b ; :: according to LATTICE3:def_9 ::_thesis: a <= b
now__::_thesis:_for_c_being_Element_of_P_st_c_in_X_holds_
[c,b]_in_the_InternalRel_of_P
let c be Element of P; ::_thesis: ( c in X implies [c,b] in the InternalRel of P )
assume c in X ; ::_thesis: [c,b] in the InternalRel of P
then c <= b by A10;
hence [c,b] in the InternalRel of P by ORDERS_2:def_5; ::_thesis: verum
end;
then b in Y by A5;
then [a,b] in the InternalRel of P by A9;
hence a <= b by ORDERS_2:def_5; ::_thesis: verum
end;
hence P is continuous by A3; ::_thesis: verum
end;
theorem Th10: :: YELLOW21:10
for P being non empty upper-bounded Poset st the InternalRel of P is well-ordering holds
for x, y being Element of P st y < x holds
ex z being Element of P st
( z is compact & y <= z & z <= x )
proof
let P be non empty upper-bounded Poset; ::_thesis: ( the InternalRel of P is well-ordering implies for x, y being Element of P st y < x holds
ex z being Element of P st
( z is compact & y <= z & z <= x ) )
set R = the InternalRel of P;
set A = order_type_of the InternalRel of P;
A1: field (RelIncl (order_type_of the InternalRel of P)) = order_type_of the InternalRel of P by WELLORD2:def_1;
assume A2: the InternalRel of P is well-ordering ; ::_thesis: for x, y being Element of P st y < x holds
ex z being Element of P st
( z is compact & y <= z & z <= x )
then reconsider L = P as complete Chain by Th9;
let x, y be Element of P; ::_thesis: ( y < x implies ex z being Element of P st
( z is compact & y <= z & z <= x ) )
the InternalRel of P, RelIncl (order_type_of the InternalRel of P) are_isomorphic by A2, WELLORD2:def_2;
then consider f being Function such that
A3: f is_isomorphism_of the InternalRel of P, RelIncl (order_type_of the InternalRel of P) by WELLORD1:def_8;
assume A4: y < x ; ::_thesis: ex z being Element of P st
( z is compact & y <= z & z <= x )
then y <= x by ORDERS_2:def_6;
then A5: [y,x] in the InternalRel of P by ORDERS_2:def_5;
then A6: [(f . y),(f . x)] in RelIncl (order_type_of the InternalRel of P) by A3, A4, WELLORD1:36;
then A7: f . x in order_type_of the InternalRel of P by A1, RELAT_1:15;
A8: f . x <> f . y by A3, A4, A5, WELLORD1:36;
A9: f . y in order_type_of the InternalRel of P by A6, A1, RELAT_1:15;
then reconsider a = f . x, b = f . y as Ordinal by A7;
b c= a by A6, A7, A9, WELLORD2:def_1;
then b c< a by A8, XBOOLE_0:def_8;
then b in a by ORDINAL1:11;
then A10: succ b c= a by ORDINAL1:21;
then A11: succ b in order_type_of the InternalRel of P by A7, ORDINAL1:12;
then A12: [(succ b),(f . x)] in RelIncl (order_type_of the InternalRel of P) by A7, A10, WELLORD2:def_1;
A13: b c= succ b by ORDINAL3:1;
rng f = order_type_of the InternalRel of P by A3, A1, WELLORD1:def_7;
then consider z being set such that
A14: z in dom f and
A15: succ b = f . z by A11, FUNCT_1:def_3;
A16: field the InternalRel of P = the carrier of P by ORDERS_1:15;
then reconsider z = z as Element of P by A3, A14, WELLORD1:def_7;
take z ; ::_thesis: ( z is compact & y <= z & z <= x )
A17: dom f = field the InternalRel of P by A3, WELLORD1:def_7;
thus z is compact ::_thesis: ( y <= z & z <= x )
proof
let D be non empty directed Subset of P; :: according to WAYBEL_3:def_1,WAYBEL_3:def_2 ::_thesis: ( not z <= sup D or ex b1 being Element of the carrier of P st
( b1 in D & z <= b1 ) )
assume that
A18: z <= sup D and
A19: for d being Element of P st d in D holds
not z <= d ; ::_thesis: contradiction
A20: L is complete ;
D is_<=_than y
proof
let c be Element of P; :: according to LATTICE3:def_9 ::_thesis: ( not c in D or c <= y )
A21: f is one-to-one by A3, WELLORD1:def_7;
assume A22: c in D ; ::_thesis: c <= y
then not z <= c by A19;
then z >= c by A20, WAYBEL_0:def_29;
then [c,z] in the InternalRel of P by ORDERS_2:def_5;
then A23: [(f . c),(succ b)] in RelIncl (order_type_of the InternalRel of P) by A3, A15, WELLORD1:def_7;
then A24: f . c in order_type_of the InternalRel of P by A1, RELAT_1:15;
then reconsider fc = f . c as Ordinal ;
A25: fc c= succ b by A11, A23, A24, WELLORD2:def_1;
c <> z by A19, A22;
then fc <> succ b by A15, A16, A17, A21, FUNCT_1:def_4;
then fc c< succ b by A25, XBOOLE_0:def_8;
then fc in succ b by ORDINAL1:11;
then fc c= b by ORDINAL1:22;
then [fc,b] in RelIncl (order_type_of the InternalRel of P) by A9, A24, WELLORD2:def_1;
hence [c,y] in the InternalRel of P by A3, A16, WELLORD1:def_7; :: according to ORDERS_2:def_5 ::_thesis: verum
end;
then sup D <= y by A20, YELLOW_0:32;
then z <= y by A18, YELLOW_0:def_2;
then [z,y] in the InternalRel of P by ORDERS_2:def_5;
then [(succ b),b] in RelIncl (order_type_of the InternalRel of P) by A3, A15, WELLORD1:def_7;
then succ b c= b by A9, A11, WELLORD2:def_1;
then b = succ b by A13, XBOOLE_0:def_10;
hence contradiction by ORDINAL1:9; ::_thesis: verum
end;
[(f . y),(succ b)] in RelIncl (order_type_of the InternalRel of P) by A9, A13, A11, WELLORD2:def_1;
hence ( [y,z] in the InternalRel of P & [z,x] in the InternalRel of P ) by A3, A15, A16, A12, WELLORD1:def_7; :: according to ORDERS_2:def_5 ::_thesis: verum
end;
theorem Th11: :: YELLOW21:11
for P being non empty upper-bounded Poset st the InternalRel of P is well-ordering holds
P is algebraic
proof
let P be non empty upper-bounded Poset; ::_thesis: ( the InternalRel of P is well-ordering implies P is algebraic )
assume A1: the InternalRel of P is well-ordering ; ::_thesis: P is algebraic
then reconsider L = P as non empty complete connected continuous Poset by Th9;
now__::_thesis:_for_x,_y_being_Element_of_L_st_x_<<_y_holds_
ex_z_being_Element_of_L_st_
(_z_in_the_carrier_of_(CompactSublatt_L)_&_x_<=_z_&_z_<=_y_)
let x, y be Element of L; ::_thesis: ( x << y implies ex z being Element of L st
( z in the carrier of (CompactSublatt L) & x <= z & z <= y ) )
assume x << y ; ::_thesis: ex z being Element of L st
( z in the carrier of (CompactSublatt L) & x <= z & z <= y )
then ( ( x is compact & x <= x & x <= y ) or x < y ) by WAYBEL_3:1, WAYBEL_3:14;
then consider z being Element of L such that
A2: z is compact and
A3: ( x <= z & z <= y ) by A1, Th10;
take z = z; ::_thesis: ( z in the carrier of (CompactSublatt L) & x <= z & z <= y )
thus z in the carrier of (CompactSublatt L) by A2, WAYBEL_8:def_1; ::_thesis: ( x <= z & z <= y )
thus ( x <= z & z <= y ) by A3; ::_thesis: verum
end;
hence P is algebraic by WAYBEL_8:7; ::_thesis: verum
end;
registration
let X be non empty set ;
let R be well-ordering upper-bounded Order of X;
cluster RelStr(# X,R #) -> algebraic complete connected continuous ;
coherence
( RelStr(# X,R #) is complete & RelStr(# X,R #) is connected & RelStr(# X,R #) is continuous & RelStr(# X,R #) is algebraic )
proof
RelStr(# X,R #) is upper-bounded by Th8;
hence ( RelStr(# X,R #) is complete & RelStr(# X,R #) is connected & RelStr(# X,R #) is continuous & RelStr(# X,R #) is algebraic ) by Th9, Th11; ::_thesis: verum
end;
end;
definition
defpred S1[ LATTICE, LATTICE, Function of $1,$2] means $3 is directed-sups-preserving ;
defpred S2[ LATTICE] means $1 is complete ;
let W be non empty set ;
given w being Element of W such that A1: not w is empty ;
funcW -UPS_category -> strict lattice-wise category means :Def10: :: YELLOW21:def 10
( ( for x being LATTICE holds
( x is object of it iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being object of it
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is directed-sups-preserving ) ) );
existence
ex b1 being strict lattice-wise category st
( ( for x being LATTICE holds
( x is object of b1 iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being object of b1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is directed-sups-preserving ) ) )
proof
reconsider w = w as non empty set by A1;
set r = the well-ordering upper-bounded Order of w;
A2: for a being LATTICE st S2[a] holds
S1[a,a, id a] ;
RelStr(# w, the well-ordering upper-bounded Order of w #) is complete ;
then A3: ex x being strict LATTICE st
( S2[x] & the carrier of x in W ) ;
A4: for a, b, c being LATTICE st S2[a] & S2[b] & S2[c] holds
for f being Function of a,b
for g being Function of b,c st S1[a,b,f] & S1[b,c,g] holds
S1[a,c,g * f] by WAYBEL20:28;
thus ex It being strict lattice-wise category st
( ( for x being LATTICE holds
( x is object of It iff ( x is strict & S2[x] & the carrier of x in W ) ) ) & ( for a, b being object of It
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff S1[ latt a, latt b,f] ) ) ) from YELLOW21:sch_3(A3, A4, A2); ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being strict lattice-wise category st ( for x being LATTICE holds
( x is object of b1 iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being object of b1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is directed-sups-preserving ) ) & ( for x being LATTICE holds
( x is object of b2 iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being object of b2
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is directed-sups-preserving ) ) holds
b1 = b2;
proof
reconsider w = w as non empty set by A1;
let C1, C2 be strict lattice-wise category; ::_thesis: ( ( for x being LATTICE holds
( x is object of C1 iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being object of C1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is directed-sups-preserving ) ) & ( for x being LATTICE holds
( x is object of C2 iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being object of C2
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is directed-sups-preserving ) ) implies C1 = C2 )
assume that
A5: for x being LATTICE holds
( x is object of C1 iff ( x is strict & S2[x] & the carrier of x in W ) ) and
A6: for a, b being object of C1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is directed-sups-preserving ) and
A7: for x being LATTICE holds
( x is object of C2 iff ( x is strict & S2[x] & the carrier of x in W ) ) and
A8: for a, b being object of C2
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is directed-sups-preserving ) ; ::_thesis: C1 = C2
defpred S3[ set , set , set ] means ex L1, L2 being LATTICE ex f being Function of L1,L2 st
( $1 = L1 & $2 = L2 & $3 = f & f is directed-sups-preserving );
A9: now__::_thesis:_for_a,_b_being_object_of_C1
for_f_being_monotone_Function_of_(latt_a),(latt_b)_holds_
(_f_in_<^a,b^>_iff_S3[a,b,f]_)
let a, b be object of C1; ::_thesis: for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff S3[a,b,f] )
let f be monotone Function of (latt a),(latt b); ::_thesis: ( f in <^a,b^> iff S3[a,b,f] )
( f in <^a,b^> iff f is directed-sups-preserving ) by A6;
hence ( f in <^a,b^> iff S3[a,b,f] ) ; ::_thesis: verum
end;
A10: now__::_thesis:_for_a,_b_being_object_of_C2
for_f_being_monotone_Function_of_(latt_a),(latt_b)_holds_
(_f_in_<^a,b^>_iff_S3[a,b,f]_)
let a, b be object of C2; ::_thesis: for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff S3[a,b,f] )
let f be monotone Function of (latt a),(latt b); ::_thesis: ( f in <^a,b^> iff S3[a,b,f] )
( f in <^a,b^> iff f is directed-sups-preserving ) by A8;
hence ( f in <^a,b^> iff S3[a,b,f] ) ; ::_thesis: verum
end;
for C1, C2 being lattice-wise category st ( for x being LATTICE holds
( x is object of C1 iff ( x is strict & S2[x] & the carrier of x in W ) ) ) & ( for a, b being object of C1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff S3[a,b,f] ) ) & ( for x being LATTICE holds
( x is object of C2 iff ( x is strict & S2[x] & the carrier of x in W ) ) ) & ( for a, b being object of C2
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff S3[a,b,f] ) ) holds
AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #) from YELLOW21:sch_5();
hence C1 = C2 by A5, A7, A9, A10; ::_thesis: verum
end;
end;
:: deftheorem Def10 defines -UPS_category YELLOW21:def_10_:_
for W being non empty set st not for w being Element of W holds w is empty holds
for b2 being strict lattice-wise category holds
( b2 = W -UPS_category iff ( ( for x being LATTICE holds
( x is object of b2 iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being object of b2
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is directed-sups-preserving ) ) ) );
registration
let W be with_non-empty_element set ;
clusterW -UPS_category -> strict lattice-wise with_complete_lattices with_all_isomorphisms ;
coherence
( W -UPS_category is with_complete_lattices & W -UPS_category is with_all_isomorphisms )
proof
set C = W -UPS_category ;
thus W -UPS_category is lattice-wise ; :: according to YELLOW21:def_5 ::_thesis: ( ( for a being object of (W -UPS_category) holds a is complete LATTICE ) & W -UPS_category is with_all_isomorphisms )
A1: ex w being non empty set st w in W by SETFAM_1:def_10;
hereby ::_thesis: W -UPS_category is with_all_isomorphisms
let a be object of (W -UPS_category); ::_thesis: a is complete LATTICE
a = latt a ;
hence a is complete LATTICE by A1, Def10; ::_thesis: verum
end;
let a, b be object of (W -UPS_category); :: according to YELLOW21:def_8 ::_thesis: for f being Function of (latt a),(latt b) st f is isomorphic holds
f in <^a,b^>
let f be Function of (latt a),(latt b); ::_thesis: ( f is isomorphic implies f in <^a,b^> )
reconsider S = latt a, T = latt b as complete LATTICE by A1, Def10;
assume f is isomorphic ; ::_thesis: f in <^a,b^>
then f is sups-preserving Function of S,T by WAYBEL13:20;
hence f in <^a,b^> by A1, Def10; ::_thesis: verum
end;
end;
theorem Th12: :: YELLOW21:12
for W being with_non-empty_element set holds the carrier of (W -UPS_category) c= POSETS W
proof
let W be with_non-empty_element set ; ::_thesis: the carrier of (W -UPS_category) c= POSETS W
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (W -UPS_category) or x in POSETS W )
assume x in the carrier of (W -UPS_category) ; ::_thesis: x in POSETS W
then reconsider x = x as object of (W -UPS_category) ;
A1: ex w being non empty set st w in W by SETFAM_1:def_10;
then A2: the carrier of (latt x) in W by Def10;
latt x = x ;
then x is strict Poset by A1, Def10;
hence x in POSETS W by A2, Def2; ::_thesis: verum
end;
theorem Th13: :: YELLOW21:13
for W being with_non-empty_element set
for x being set holds
( x is object of (W -UPS_category) iff ( x is complete LATTICE & x in POSETS W ) )
proof
let W be with_non-empty_element set ; ::_thesis: for x being set holds
( x is object of (W -UPS_category) iff ( x is complete LATTICE & x in POSETS W ) )
let x be set ; ::_thesis: ( x is object of (W -UPS_category) iff ( x is complete LATTICE & x in POSETS W ) )
hereby ::_thesis: ( x is complete LATTICE & x in POSETS W implies x is object of (W -UPS_category) )
assume x is object of (W -UPS_category) ; ::_thesis: ( x is complete LATTICE & x in POSETS W )
then reconsider a = x as object of (W -UPS_category) ;
latt a = x ;
hence x is complete LATTICE ; ::_thesis: x in POSETS W
( a in the carrier of (W -UPS_category) & the carrier of (W -UPS_category) c= POSETS W ) by Th12;
hence x in POSETS W ; ::_thesis: verum
end;
assume x is complete LATTICE ; ::_thesis: ( not x in POSETS W or x is object of (W -UPS_category) )
then reconsider L = x as complete LATTICE ;
assume x in POSETS W ; ::_thesis: x is object of (W -UPS_category)
then A1: ( the carrier of (L as_1-sorted) in W & L is strict ) by Def2;
L as_1-sorted = L by Def1;
hence x is object of (W -UPS_category) by A1, Def10; ::_thesis: verum
end;
theorem Th14: :: YELLOW21:14
for W being with_non-empty_element set
for L being LATTICE st the carrier of L in W holds
( L is object of (W -UPS_category) iff ( L is strict & L is complete ) )
proof
let W be with_non-empty_element set ; ::_thesis: for L being LATTICE st the carrier of L in W holds
( L is object of (W -UPS_category) iff ( L is strict & L is complete ) )
let L be LATTICE; ::_thesis: ( the carrier of L in W implies ( L is object of (W -UPS_category) iff ( L is strict & L is complete ) ) )
assume A1: the carrier of L in W ; ::_thesis: ( L is object of (W -UPS_category) iff ( L is strict & L is complete ) )
L as_1-sorted = L by Def1;
then ( L in POSETS W iff L is strict ) by A1, Def2;
hence ( L is object of (W -UPS_category) iff ( L is strict & L is complete ) ) by Th13; ::_thesis: verum
end;
theorem Th15: :: YELLOW21:15
for W being with_non-empty_element set
for a, b being object of (W -UPS_category)
for f being set holds
( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) )
proof
let W be with_non-empty_element set ; ::_thesis: for a, b being object of (W -UPS_category)
for f being set holds
( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) )
let a, b be object of (W -UPS_category); ::_thesis: for f being set holds
( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) )
let f be set ; ::_thesis: ( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) )
A1: ex w being non empty set st w in W by SETFAM_1:def_10;
hereby ::_thesis: ( f is directed-sups-preserving Function of (latt a),(latt b) implies f in <^a,b^> )
assume A2: f in <^a,b^> ; ::_thesis: f is directed-sups-preserving Function of (latt a),(latt b)
then reconsider g = f as Morphism of a,b ;
f = @ g by A2, Def7;
hence f is directed-sups-preserving Function of (latt a),(latt b) by A1, A2, Def10; ::_thesis: verum
end;
thus ( f is directed-sups-preserving Function of (latt a),(latt b) implies f in <^a,b^> ) by A1, Def10; ::_thesis: verum
end;
registration
let W be with_non-empty_element set ;
let a, b be object of (W -UPS_category);
cluster<^a,b^> -> non empty ;
coherence
not <^a,b^> is empty
proof
set f = the directed-sups-preserving Function of (latt a),(latt b);
the directed-sups-preserving Function of (latt a),(latt b) in <^a,b^> by Th15;
hence not <^a,b^> is empty ; ::_thesis: verum
end;
end;
begin
registration
let A be set-id-inheriting category;
cluster non empty transitive id-inheriting -> non empty set-id-inheriting for SubCatStr of A;
coherence
for b1 being non empty subcategory of A holds b1 is set-id-inheriting
proof
let B be non empty subcategory of A; ::_thesis: B is set-id-inheriting
let b be object of B; :: according to YELLOW18:def_10 ::_thesis: idm b = id (B -carrier_of b)
( b in the carrier of B & the carrier of B c= the carrier of A ) by ALTCAT_2:def_11;
then reconsider a = b as object of A ;
thus idm b = idm a by ALTCAT_2:34
.= id (the_carrier_of a) by YELLOW18:def_10
.= id (the_carrier_of b) by ALTCAT_2:34 ; ::_thesis: verum
end;
end;
registration
let A be para-functional category;
cluster non empty transitive id-inheriting -> non empty para-functional for SubCatStr of A;
coherence
for b1 being non empty subcategory of A holds b1 is para-functional
proof
let B be non empty subcategory of A; ::_thesis: B is para-functional
consider F being ManySortedSet of A such that
A1: for a1, a2 being object of A holds <^a1,a2^> c= Funcs ((F . a1),(F . a2)) by YELLOW18:def_7;
set G = F | the carrier of B;
A2: the carrier of B c= the carrier of A by ALTCAT_2:def_11;
dom F = the carrier of A by PARTFUN1:def_2;
then dom (F | the carrier of B) = the carrier of B by A2, RELAT_1:62;
then reconsider G = F | the carrier of B as ManySortedSet of B by PARTFUN1:def_2, RELAT_1:def_18;
take G ; :: according to YELLOW18:def_7 ::_thesis: for b1, b2 being Element of the carrier of B holds <^b1,b2^> c= Funcs ((G . b1),(G . b2))
let a1, a2 be object of B; ::_thesis: <^a1,a2^> c= Funcs ((G . a1),(G . a2))
( a1 in the carrier of B & a2 in the carrier of B ) ;
then reconsider b1 = a1, b2 = a2 as object of A by A2;
( F . a1 = G . a1 & F . a2 = G . a2 ) by FUNCT_1:49;
then ( <^a1,a2^> c= <^b1,b2^> & <^b1,b2^> c= Funcs ((G . a1),(G . a2)) ) by A1, ALTCAT_2:31;
hence <^a1,a2^> c= Funcs ((G . a1),(G . a2)) by XBOOLE_1:1; ::_thesis: verum
end;
end;
registration
let A be semi-functional category;
cluster non empty transitive -> non empty transitive semi-functional for SubCatStr of A;
coherence
for b1 being non empty transitive SubCatStr of A holds b1 is semi-functional
proof
let B be non empty transitive SubCatStr of A; ::_thesis: B is semi-functional
let b1, b2, b3 be object of B; :: according to ALTCAT_1:def_12 ::_thesis: ( <^b1,b2^> = {} or <^b2,b3^> = {} or <^b1,b3^> = {} or for b1 being Element of <^b1,b2^>
for b2 being Element of <^b2,b3^>
for b3, b4 being set holds
( not b1 = b3 or not b2 = b4 or b2 * b1 = b3 * b4 ) )
assume that
A1: <^b1,b2^> <> {} and
A2: <^b2,b3^> <> {} and
A3: <^b1,b3^> <> {} ; ::_thesis: for b1 being Element of <^b1,b2^>
for b2 being Element of <^b2,b3^>
for b3, b4 being set holds
( not b1 = b3 or not b2 = b4 or b2 * b1 = b3 * b4 )
reconsider a1 = b1, a2 = b2, a3 = b3 as object of A by ALTCAT_2:29;
A4: ( <^a1,a2^> <> {} & <^a2,a3^> <> {} ) by A1, A2, ALTCAT_2:31, XBOOLE_1:3;
let f1 be Morphism of b1,b2; ::_thesis: for b1 being Element of <^b2,b3^>
for b2, b3 being set holds
( not f1 = b2 or not b1 = b3 or b1 * f1 = b2 * b3 )
let f2 be Morphism of b2,b3; ::_thesis: for b1, b2 being set holds
( not f1 = b1 or not f2 = b2 or f2 * f1 = b1 * b2 )
reconsider g2 = f2 as Morphism of a2,a3 by A2, ALTCAT_2:33;
reconsider g1 = f1 as Morphism of a1,a2 by A1, ALTCAT_2:33;
A5: <^a1,a3^> <> {} by A3, ALTCAT_2:31, XBOOLE_1:3;
let f9, g9 be Function; ::_thesis: ( not f1 = f9 or not f2 = g9 or f2 * f1 = f9 * g9 )
assume ( f1 = f9 & f2 = g9 ) ; ::_thesis: f2 * f1 = f9 * g9
then g2 * g1 = g9 * f9 by A4, A5, ALTCAT_1:def_12;
hence f2 * f1 = f9 * g9 by A1, A2, ALTCAT_2:32; ::_thesis: verum
end;
end;
registration
let A be carrier-underlaid category;
cluster non empty transitive id-inheriting -> non empty carrier-underlaid for SubCatStr of A;
coherence
for b1 being non empty subcategory of A holds b1 is carrier-underlaid
proof
let B be non empty subcategory of A; ::_thesis: B is carrier-underlaid
let b be object of B; :: according to YELLOW21:def_3 ::_thesis: ex S being 1-sorted st
( b = S & the_carrier_of b = the carrier of S )
reconsider a = b as object of A by ALTCAT_2:29;
consider S being 1-sorted such that
A1: a = S and
A2: the_carrier_of a = the carrier of S by Def3;
take S ; ::_thesis: ( b = S & the_carrier_of b = the carrier of S )
thus b = S by A1; ::_thesis: the_carrier_of b = the carrier of S
thus the_carrier_of b = the carrier of S by A2, ALTCAT_2:34; ::_thesis: verum
end;
end;
registration
let A be lattice-wise category;
cluster non empty transitive id-inheriting -> non empty lattice-wise for SubCatStr of A;
coherence
for b1 being non empty subcategory of A holds b1 is lattice-wise
proof
let B be non empty subcategory of A; ::_thesis: B is lattice-wise
thus ( B is semi-functional & B is set-id-inheriting ) ; :: according to YELLOW21:def_4 ::_thesis: ( ( for a being object of B holds a is LATTICE ) & ( for a, b being object of B
for A, B being LATTICE st A = a & B = b holds
<^a,b^> c= MonFuncs (A,B) ) )
hereby ::_thesis: for a, b being object of B
for A, B being LATTICE st A = a & B = b holds
<^a,b^> c= MonFuncs (A,B)
let b be object of B; ::_thesis: b is LATTICE
reconsider a = b as object of A by ALTCAT_2:29;
a is LATTICE by Def4;
hence b is LATTICE ; ::_thesis: verum
end;
let a, b be object of B; ::_thesis: for A, B being LATTICE st A = a & B = b holds
<^a,b^> c= MonFuncs (A,B)
reconsider a9 = a, b9 = b as object of A by ALTCAT_2:29;
let A, B be LATTICE; ::_thesis: ( A = a & B = b implies <^a,b^> c= MonFuncs (A,B) )
assume ( A = a & B = b ) ; ::_thesis: <^a,b^> c= MonFuncs (A,B)
then ( <^a,b^> c= <^a9,b9^> & <^a9,b9^> c= MonFuncs (A,B) ) by Def4, ALTCAT_2:31;
hence <^a,b^> c= MonFuncs (A,B) by XBOOLE_1:1; ::_thesis: verum
end;
end;
registration
let A be lattice-wise with_all_isomorphisms category;
cluster non empty transitive full id-inheriting -> non empty with_all_isomorphisms for SubCatStr of A;
coherence
for b1 being non empty subcategory of A st b1 is full holds
b1 is with_all_isomorphisms
proof
let B be non empty subcategory of A; ::_thesis: ( B is full implies B is with_all_isomorphisms )
assume A1: B is full ; ::_thesis: B is with_all_isomorphisms
let a, b be object of B; :: according to YELLOW21:def_8 ::_thesis: for f being Function of (latt a),(latt b) st f is isomorphic holds
f in <^a,b^>
let f be Function of (latt a),(latt b); ::_thesis: ( f is isomorphic implies f in <^a,b^> )
reconsider a9 = a, b9 = b as object of A by ALTCAT_2:29;
assume f is isomorphic ; ::_thesis: f in <^a,b^>
then f in <^a9,b9^> by Def8;
hence f in <^a,b^> by A1, ALTCAT_2:28; ::_thesis: verum
end;
end;
registration
let A be with_complete_lattices category;
cluster non empty transitive id-inheriting -> non empty with_complete_lattices for SubCatStr of A;
coherence
for b1 being non empty subcategory of A holds b1 is with_complete_lattices
proof
let B be non empty subcategory of A; ::_thesis: B is with_complete_lattices
thus B is lattice-wise ; :: according to YELLOW21:def_5 ::_thesis: for a being object of B holds a is complete LATTICE
let b be object of B; ::_thesis: b is complete LATTICE
reconsider a = b as object of A by ALTCAT_2:29;
a is complete LATTICE by Def5;
hence b is complete LATTICE ; ::_thesis: verum
end;
end;
definition
let W be with_non-empty_element set ;
defpred S1[ object of (W -UPS_category)] means latt $1 is continuous ;
consider a being non empty set such that
A1: a in W by SETFAM_1:def_10;
set r = the well-ordering upper-bounded Order of a;
set b = RelStr(# a, the well-ordering upper-bounded Order of a #);
funcW -CONT_category -> non empty strict full subcategory of W -UPS_category means :Def11: :: YELLOW21:def 11
for a being object of (W -UPS_category) holds
( a is object of it iff latt a is continuous );
existence
ex b1 being non empty strict full subcategory of W -UPS_category st
for a being object of (W -UPS_category) holds
( a is object of b1 iff latt a is continuous )
proof
reconsider b = RelStr(# a, the well-ordering upper-bounded Order of a #) as object of (W -UPS_category) by A1, Def10;
b = latt b ;
then A2: ex b being object of (W -UPS_category) st S1[b] ;
thus ex C being non empty strict full subcategory of W -UPS_category st
for a being object of (W -UPS_category) holds
( a is object of C iff S1[a] ) from YELLOW20:sch_2(A2); ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being non empty strict full subcategory of W -UPS_category st ( for a being object of (W -UPS_category) holds
( a is object of b1 iff latt a is continuous ) ) & ( for a being object of (W -UPS_category) holds
( a is object of b2 iff latt a is continuous ) ) holds
b1 = b2;
proof
let B1, B2 be non empty strict full subcategory of W -UPS_category ; ::_thesis: ( ( for a being object of (W -UPS_category) holds
( a is object of B1 iff latt a is continuous ) ) & ( for a being object of (W -UPS_category) holds
( a is object of B2 iff latt a is continuous ) ) implies B1 = B2 )
assume that
A3: for a being object of (W -UPS_category) holds
( a is object of B1 iff S1[a] ) and
A4: for a being object of (W -UPS_category) holds
( a is object of B2 iff S1[a] ) ; ::_thesis: B1 = B2
AltCatStr(# the carrier of B1, the Arrows of B1, the Comp of B1 #) = AltCatStr(# the carrier of B2, the Arrows of B2, the Comp of B2 #) from YELLOW20:sch_3(A3, A4);
hence B1 = B2 ; ::_thesis: verum
end;
end;
:: deftheorem Def11 defines -CONT_category YELLOW21:def_11_:_
for W being with_non-empty_element set
for b2 being non empty strict full subcategory of W -UPS_category holds
( b2 = W -CONT_category iff for a being object of (W -UPS_category) holds
( a is object of b2 iff latt a is continuous ) );
definition
let W be with_non-empty_element set ;
defpred S1[ object of (W -CONT_category)] means latt $1 is algebraic ;
consider a being non empty set such that
A1: a in W by SETFAM_1:def_10;
set r = the well-ordering upper-bounded Order of a;
set b = RelStr(# a, the well-ordering upper-bounded Order of a #);
funcW -ALG_category -> non empty strict full subcategory of W -CONT_category means :Def12: :: YELLOW21:def 12
for a being object of (W -CONT_category) holds
( a is object of it iff latt a is algebraic );
existence
ex b1 being non empty strict full subcategory of W -CONT_category st
for a being object of (W -CONT_category) holds
( a is object of b1 iff latt a is algebraic )
proof
reconsider b = RelStr(# a, the well-ordering upper-bounded Order of a #) as object of (W -UPS_category) by A1, Def10;
b = latt b ;
then reconsider b = b as object of (W -CONT_category) by Def11;
b = latt b ;
then A2: ex b being object of (W -CONT_category) st S1[b] ;
thus ex C being non empty strict full subcategory of W -CONT_category st
for a being object of (W -CONT_category) holds
( a is object of C iff S1[a] ) from YELLOW20:sch_2(A2); ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being non empty strict full subcategory of W -CONT_category st ( for a being object of (W -CONT_category) holds
( a is object of b1 iff latt a is algebraic ) ) & ( for a being object of (W -CONT_category) holds
( a is object of b2 iff latt a is algebraic ) ) holds
b1 = b2;
proof
let B1, B2 be non empty strict full subcategory of W -CONT_category ; ::_thesis: ( ( for a being object of (W -CONT_category) holds
( a is object of B1 iff latt a is algebraic ) ) & ( for a being object of (W -CONT_category) holds
( a is object of B2 iff latt a is algebraic ) ) implies B1 = B2 )
assume that
A3: for a being object of (W -CONT_category) holds
( a is object of B1 iff S1[a] ) and
A4: for a being object of (W -CONT_category) holds
( a is object of B2 iff S1[a] ) ; ::_thesis: B1 = B2
AltCatStr(# the carrier of B1, the Arrows of B1, the Comp of B1 #) = AltCatStr(# the carrier of B2, the Arrows of B2, the Comp of B2 #) from YELLOW20:sch_3(A3, A4);
hence B1 = B2 ; ::_thesis: verum
end;
end;
:: deftheorem Def12 defines -ALG_category YELLOW21:def_12_:_
for W being with_non-empty_element set
for b2 being non empty strict full subcategory of W -CONT_category holds
( b2 = W -ALG_category iff for a being object of (W -CONT_category) holds
( a is object of b2 iff latt a is algebraic ) );
theorem Th16: :: YELLOW21:16
for W being with_non-empty_element set
for L being LATTICE st the carrier of L in W holds
( L is object of (W -CONT_category) iff ( L is strict & L is complete & L is continuous ) )
proof
let W be with_non-empty_element set ; ::_thesis: for L being LATTICE st the carrier of L in W holds
( L is object of (W -CONT_category) iff ( L is strict & L is complete & L is continuous ) )
let L be LATTICE; ::_thesis: ( the carrier of L in W implies ( L is object of (W -CONT_category) iff ( L is strict & L is complete & L is continuous ) ) )
assume A1: the carrier of L in W ; ::_thesis: ( L is object of (W -CONT_category) iff ( L is strict & L is complete & L is continuous ) )
hereby ::_thesis: ( L is strict & L is complete & L is continuous implies L is object of (W -CONT_category) )
assume L is object of (W -CONT_category) ; ::_thesis: ( L is strict & L is complete & L is continuous )
then reconsider a = L as object of (W -CONT_category) ;
( L = latt a & a is object of (W -UPS_category) ) by ALTCAT_2:29;
hence ( L is strict & L is complete & L is continuous ) by A1, Def11, Th14; ::_thesis: verum
end;
assume A2: ( L is strict & L is complete & L is continuous ) ; ::_thesis: L is object of (W -CONT_category)
then reconsider a = L as object of (W -UPS_category) by A1, Th14;
latt a = L ;
hence L is object of (W -CONT_category) by A2, Def11; ::_thesis: verum
end;
theorem :: YELLOW21:17
for W being with_non-empty_element set
for L being LATTICE st the carrier of L in W holds
( L is object of (W -ALG_category) iff ( L is strict & L is complete & L is algebraic ) )
proof
let W be with_non-empty_element set ; ::_thesis: for L being LATTICE st the carrier of L in W holds
( L is object of (W -ALG_category) iff ( L is strict & L is complete & L is algebraic ) )
let L be LATTICE; ::_thesis: ( the carrier of L in W implies ( L is object of (W -ALG_category) iff ( L is strict & L is complete & L is algebraic ) ) )
assume A1: the carrier of L in W ; ::_thesis: ( L is object of (W -ALG_category) iff ( L is strict & L is complete & L is algebraic ) )
hereby ::_thesis: ( L is strict & L is complete & L is algebraic implies L is object of (W -ALG_category) )
assume L is object of (W -ALG_category) ; ::_thesis: ( L is strict & L is complete & L is algebraic )
then reconsider a = L as object of (W -ALG_category) ;
( L = latt a & a is object of (W -CONT_category) ) by ALTCAT_2:29;
hence ( L is strict & L is complete & L is algebraic ) by A1, Def12, Th16; ::_thesis: verum
end;
assume A2: ( L is strict & L is complete & L is algebraic ) ; ::_thesis: L is object of (W -ALG_category)
then reconsider a = L as object of (W -CONT_category) by A1, Th16;
latt a = L ;
hence L is object of (W -ALG_category) by A2, Def12; ::_thesis: verum
end;
theorem Th18: :: YELLOW21:18
for W being with_non-empty_element set
for a, b being object of (W -CONT_category)
for f being set holds
( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) )
proof
let W be with_non-empty_element set ; ::_thesis: for a, b being object of (W -CONT_category)
for f being set holds
( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) )
let a, b be object of (W -CONT_category); ::_thesis: for f being set holds
( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) )
let f be set ; ::_thesis: ( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) )
reconsider a1 = a, b1 = b as object of (W -UPS_category) by ALTCAT_2:29;
<^a,b^> = <^a1,b1^> by ALTCAT_2:28;
hence ( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) ) by Th15; ::_thesis: verum
end;
theorem Th19: :: YELLOW21:19
for W being with_non-empty_element set
for a, b being object of (W -ALG_category)
for f being set holds
( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) )
proof
let W be with_non-empty_element set ; ::_thesis: for a, b being object of (W -ALG_category)
for f being set holds
( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) )
let a, b be object of (W -ALG_category); ::_thesis: for f being set holds
( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) )
let f be set ; ::_thesis: ( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) )
reconsider a1 = a, b1 = b as object of (W -CONT_category) by ALTCAT_2:29;
<^a,b^> = <^a1,b1^> by ALTCAT_2:28;
hence ( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) ) by Th18; ::_thesis: verum
end;
registration
let W be with_non-empty_element set ;
let a, b be object of (W -CONT_category);
cluster<^a,b^> -> non empty ;
coherence
not <^a,b^> is empty
proof
set f = the directed-sups-preserving Function of (latt a),(latt b);
the directed-sups-preserving Function of (latt a),(latt b) in <^a,b^> by Th18;
hence not <^a,b^> is empty ; ::_thesis: verum
end;
end;
registration
let W be with_non-empty_element set ;
let a, b be object of (W -ALG_category);
cluster<^a,b^> -> non empty ;
coherence
not <^a,b^> is empty
proof
set f = the directed-sups-preserving Function of (latt a),(latt b);
the directed-sups-preserving Function of (latt a),(latt b) in <^a,b^> by Th19;
hence not <^a,b^> is empty ; ::_thesis: verum
end;
end;