:: Duality Based on Galois Connection. Part I
:: by Grzegorz Bancerek
::
:: Received August 8, 2001
:: Copyright (c) 2001-2012 Association of Mizar Users


begin

::<section1>Infs-preserving and sups-preserving maps</section1>
registration
let S, T be complete LATTICE;
cluster Galois for Connection of S,T;
existence
 ex b1 being Connection of S,T st b1 is Galois
proofend;
end;

theorem Th1: :: WAYBEL34:1
for S, T, S9, T9 being non empty RelStr st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of S9, the InternalRel of S9 #) &amp; RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of T9, the InternalRel of T9 #) holds
for c being Connection of S,T
for c9 being Connection of S9,T9 st c = c9 &amp; c is Galois holds
c9 is Galois
proofend;

definition
let S, T be LATTICE;
let g be Function of S,T;
assume that
A1: S is complete and
A2: g is infs-preserving ;
A3: g is upper_adjoint by A1, A2, WAYBEL_1:16;
func LowerAdj g ->  Function of T,S means :Def1: :: WAYBEL34:def 1
[g,it] is Galois ;
uniqueness
 for b1, b2 being Function of T,S st [g,b1] is Galois &amp; [g,b2] is Galois holds
b1 = b2
proofend;
existence
 ex b1 being Function of T,S st [g,b1] is Galois by A3, WAYBEL_1:def_11;
end;

:: deftheorem Def1 defines LowerAdj WAYBEL34:def_1_:_
 for S, T being LATTICE
for g being Function of S,T st S is complete &amp; g is infs-preserving holds
for b4 being Function of T,S holds
( b4 = LowerAdj g iff [g,b4] is Galois );

definition
let S, T be LATTICE;
let d be Function of T,S;
assume that
A1: T is complete and
A2: d is sups-preserving ;
A3: d is lower_adjoint by A1, A2, WAYBEL_1:17;
func UpperAdj d ->  Function of S,T means :Def2: :: WAYBEL34:def 2
[it,d] is Galois ;
existence
 ex b1 being Function of S,T st [b1,d] is Galois by A3, WAYBEL_1:def_12;
correctness
uniqueness
for b1, b2 being Function of S,T st [b1,d] is Galois &amp; [b2,d] is Galois holds
b1 = b2;
proofend;
end;

:: deftheorem Def2 defines UpperAdj WAYBEL34:def_2_:_
 for S, T being LATTICE
for d being Function of T,S st T is complete &amp; d is sups-preserving holds
for b4 being Function of S,T holds
( b4 = UpperAdj d iff [b4,d] is Galois );

Lm1: now__::_thesis:_for_S,_T_being_LATTICE_st_S_is_complete_&amp;_T_is_complete_holds_
for_g_being_Function_of_S,T_st_g_is_infs-preserving_holds_
(_LowerAdj_g_is_monotone_&amp;_LowerAdj_g_is_lower_adjoint_&amp;_LowerAdj_g_is_sups-preserving_)
let S, T be LATTICE; ::_thesis: ( S is complete &amp; T is complete implies for g being Function of S,T st g is infs-preserving holds
( LowerAdj g is monotone &amp; LowerAdj g is lower_adjoint &amp; LowerAdj g is sups-preserving ) )
assume that
A1: S is complete and
A2: T is complete ; ::_thesis: for g being Function of S,T st g is infs-preserving holds
( LowerAdj g is monotone &amp; LowerAdj g is lower_adjoint &amp; LowerAdj g is sups-preserving )
reconsider S9 = S, T9 = T as complete LATTICE by A1, A2;
let g be Function of S,T; ::_thesis: ( g is infs-preserving implies ( LowerAdj g is monotone &amp; LowerAdj g is lower_adjoint &amp; LowerAdj g is sups-preserving ) )
assume  g is infs-preserving ; ::_thesis: ( LowerAdj g is monotone &amp; LowerAdj g is lower_adjoint &amp; LowerAdj g is sups-preserving )
then reconsider g9 = g as infs-preserving Function of S9,T9 ;
 [g9,(LowerAdj g9)] is Galois by Def1;
then  ( LowerAdj g9 is lower_adjoint &amp; LowerAdj g9 is monotone ) by WAYBEL_1:8, WAYBEL_1:def_12;
hence  ( LowerAdj g is monotone &amp; LowerAdj g is lower_adjoint &amp; LowerAdj g is sups-preserving ) ; ::_thesis: verum
end;

Lm2: now__::_thesis:_for_S,_T_being_LATTICE_st_S_is_complete_&amp;_T_is_complete_holds_
for_g_being_Function_of_S,T_st_g_is_sups-preserving_holds_
(_UpperAdj_g_is_monotone_&amp;_UpperAdj_g_is_upper_adjoint_&amp;_UpperAdj_g_is_infs-preserving_)
let S, T be LATTICE; ::_thesis: ( S is complete &amp; T is complete implies for g being Function of S,T st g is sups-preserving holds
( UpperAdj g is monotone &amp; UpperAdj g is upper_adjoint &amp; UpperAdj g is infs-preserving ) )
assume that
A1: S is complete and
A2: T is complete ; ::_thesis: for g being Function of S,T st g is sups-preserving holds
( UpperAdj g is monotone &amp; UpperAdj g is upper_adjoint &amp; UpperAdj g is infs-preserving )
reconsider S9 = S, T9 = T as complete LATTICE by A1, A2;
let g be Function of S,T; ::_thesis: ( g is sups-preserving implies ( UpperAdj g is monotone &amp; UpperAdj g is upper_adjoint &amp; UpperAdj g is infs-preserving ) )
assume  g is sups-preserving ; ::_thesis: ( UpperAdj g is monotone &amp; UpperAdj g is upper_adjoint &amp; UpperAdj g is infs-preserving )
then reconsider g9 = g as sups-preserving Function of S9,T9 ;
 [(UpperAdj g9),g9] is Galois by Def2;
then  ( UpperAdj g9 is upper_adjoint &amp; UpperAdj g9 is monotone ) by WAYBEL_1:8, WAYBEL_1:def_11;
hence  ( UpperAdj g is monotone &amp; UpperAdj g is upper_adjoint &amp; UpperAdj g is infs-preserving ) ; ::_thesis: verum
end;

registration
let S, T be complete LATTICE;
let g be infs-preserving Function of S,T;
cluster LowerAdj g ->  lower_adjoint ;
coherence
 LowerAdj g is lower_adjoint by Lm1;
end;

registration
let S, T be complete LATTICE;
let d be sups-preserving Function of T,S;
cluster UpperAdj d ->  upper_adjoint ;
coherence
 UpperAdj d is upper_adjoint by Lm2;
end;

theorem :: WAYBEL34:2
for S, T being complete LATTICE
for g being infs-preserving Function of S,T
for t being Element of T holds (LowerAdj g) . t = inf (g " (uparrow t))
proofend;

theorem :: WAYBEL34:3
for S, T being complete LATTICE
for d being sups-preserving Function of T,S
for s being Element of S holds (UpperAdj d) . s = sup (d " (downarrow s))
proofend;

definition
let S, T be RelStr ;
let f be Function of the carrier of S, the carrier of T;
funcf opp  ->  Function of (S opp),(T opp) equals :: WAYBEL34:def 3
f;
coherence
 f is Function of (S opp),(T opp) ;
end;

:: deftheorem  defines opp WAYBEL34:def_3_:_
 for S, T being RelStr
for f being Function of the carrier of S, the carrier of T holds f opp = f;

registration
let S, T be complete LATTICE;
let g be infs-preserving Function of S,T;
clusterg opp  ->  lower_adjoint ;
coherence
 g opp is lower_adjoint
proofend;
end;

registration
let S, T be complete LATTICE;
let d be sups-preserving Function of S,T;
clusterd opp  ->  upper_adjoint ;
coherence
 d opp is upper_adjoint
proofend;
end;

theorem :: WAYBEL34:4
for S, T being complete LATTICE
for g being infs-preserving Function of S,T holds LowerAdj g = UpperAdj (g opp)
proofend;

theorem :: WAYBEL34:5
for S, T being complete LATTICE
for d being sups-preserving Function of S,T holds LowerAdj (d opp) = UpperAdj d
proofend;

theorem Th6: :: WAYBEL34:6
for L being non empty RelStr holds [(id L),(id L)] is Galois
proofend;

theorem Th7: :: WAYBEL34:7
for L being complete LATTICE holds
( LowerAdj (id L) = id L &amp; UpperAdj (id L) = id L )
proofend;

theorem Th8: :: WAYBEL34:8
for L1, L2, L3 being complete LATTICE
for g1 being infs-preserving Function of L1,L2
for g2 being infs-preserving Function of L2,L3 holds LowerAdj (g2 * g1) = (LowerAdj g1) * (LowerAdj g2)
proofend;

theorem Th9: :: WAYBEL34:9
for L1, L2, L3 being complete LATTICE
for d1 being sups-preserving Function of L1,L2
for d2 being sups-preserving Function of L2,L3 holds UpperAdj (d2 * d1) = (UpperAdj d1) * (UpperAdj d2)
proofend;

theorem Th10: :: WAYBEL34:10
for S, T being complete LATTICE
for g being infs-preserving Function of S,T holds UpperAdj (LowerAdj g) = g
proofend;

theorem Th11: :: WAYBEL34:11
for S, T being complete LATTICE
for d being sups-preserving Function of S,T holds LowerAdj (UpperAdj d) = d
proofend;

theorem Th12: :: WAYBEL34:12
for C being non empty AltCatStr
for a, b, f being set st f in the Arrows of C . (a,b) holds
ex o1, o2 being object of C st
( o1 = a &amp; o2 = b &amp; f in <^o1,o2^> &amp; f is Morphism of o1,o2 )
proofend;

definition
let W be non empty set ;
defpred S1[ LATTICE] means $1 is complete ;
defpred S2[ LATTICE, LATTICE, Function of $1,$2] means $3 is infs-preserving ;
given w being Element of W such that A1: not w is empty ;
funcW -INF_category  ->  strict lattice-wise category means :Def4: :: WAYBEL34:def 4
( ( for x being LATTICE holds
( x is object of it iff ( x is strict &amp; x is complete &amp; the carrier of x in W ) ) ) &amp; ( 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 infs-preserving ) ) );
existence
 ex b1 being strict lattice-wise category st
( ( for x being LATTICE holds
( x is object of b1 iff ( x is strict &amp; x is complete &amp; the carrier of x in W ) ) ) &amp; ( 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 infs-preserving ) ) )
proofend;
uniqueness
 for b1, b2 being strict lattice-wise category st ( for x being LATTICE holds
( x is object of b1 iff ( x is strict &amp; x is complete &amp; the carrier of x in W ) ) ) &amp; ( 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 infs-preserving ) ) &amp; ( for x being LATTICE holds
( x is object of b2 iff ( x is strict &amp; x is complete &amp; the carrier of x in W ) ) ) &amp; ( 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 infs-preserving ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines -INF_category WAYBEL34:def_4_:_
 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 -INF_category iff ( ( for x being LATTICE holds
( x is object of b2 iff ( x is strict &amp; x is complete &amp; the carrier of x in W ) ) ) &amp; ( 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 infs-preserving ) ) ) );

Lm3:  for W being with_non-empty_element set
for a, b being LATTICE
for f being Function of a,b holds
( f in the Arrows of (W -INF_category) . (a,b) iff ( a in the carrier of (W -INF_category) &amp; b in the carrier of (W -INF_category) &amp; a is complete &amp; b is complete &amp; f is infs-preserving ) )
proofend;

definition
let W be non empty set ;
defpred S1[ LATTICE] means $1 is complete ;
defpred S2[ LATTICE, LATTICE, Function of $1,$2] means $3 is sups-preserving ;
given w being Element of W such that A1: not w is empty ;
funcW -SUP_category  ->  strict lattice-wise category means :Def5: :: WAYBEL34:def 5
( ( for x being LATTICE holds
( x is object of it iff ( x is strict &amp; x is complete &amp; the carrier of x in W ) ) ) &amp; ( 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 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 &amp; x is complete &amp; the carrier of x in W ) ) ) &amp; ( 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 sups-preserving ) ) )
proofend;
uniqueness
 for b1, b2 being strict lattice-wise category st ( for x being LATTICE holds
( x is object of b1 iff ( x is strict &amp; x is complete &amp; the carrier of x in W ) ) ) &amp; ( 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 sups-preserving ) ) &amp; ( for x being LATTICE holds
( x is object of b2 iff ( x is strict &amp; x is complete &amp; the carrier of x in W ) ) ) &amp; ( 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 sups-preserving ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines -SUP_category WAYBEL34:def_5_:_
 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 -SUP_category iff ( ( for x being LATTICE holds
( x is object of b2 iff ( x is strict &amp; x is complete &amp; the carrier of x in W ) ) ) &amp; ( 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 sups-preserving ) ) ) );

Lm4:  for W being with_non-empty_element set
for a, b being LATTICE
for f being Function of a,b holds
( f in the Arrows of (W -SUP_category) . (a,b) iff ( a in the carrier of (W -SUP_category) &amp; b in the carrier of (W -SUP_category) &amp; a is complete &amp; b is complete &amp; f is sups-preserving ) )
proofend;

registration
let W be with_non-empty_element set ;
clusterW -INF_category  ->  strict lattice-wise with_complete_lattices ;
coherence
 W -INF_category is with_complete_lattices
proofend;
clusterW -SUP_category  ->  strict lattice-wise with_complete_lattices ;
coherence
 W -SUP_category is with_complete_lattices
proofend;
end;

theorem Th13: :: WAYBEL34:13
for W being with_non-empty_element set
for L being LATTICE holds
( L is object of (W -INF_category) iff ( L is strict &amp; L is complete &amp; the carrier of L in W ) )
proofend;

theorem Th14: :: WAYBEL34:14
for W being with_non-empty_element set
for a, b being object of (W -INF_category)
for f being set holds
( f in <^a,b^> iff f is infs-preserving Function of (latt a),(latt b) )
proofend;

theorem Th15: :: WAYBEL34:15
for W being with_non-empty_element set
for L being LATTICE holds
( L is object of (W -SUP_category) iff ( L is strict &amp; L is complete &amp; the carrier of L in W ) )
proofend;

theorem Th16: :: WAYBEL34:16
for W being with_non-empty_element set
for a, b being object of (W -SUP_category)
for f being set holds
( f in <^a,b^> iff f is sups-preserving Function of (latt a),(latt b) )
proofend;

theorem Th17: :: WAYBEL34:17
for W being with_non-empty_element set holds the carrier of (W -INF_category) = the carrier of (W -SUP_category)
proofend;

definition
let W be with_non-empty_element set ;
set A = W -INF_category ;
set B = W -SUP_category ;
deffunc H1( LATTICE) ->  LATTICE = $1;
deffunc H2( LATTICE, LATTICE, Function of $1,$2) ->  Function of $2,$1 = LowerAdj $3;
defpred S1[ LATTICE, LATTICE, Function of $1,$2] means ( $1 is complete &amp; $2 is complete &amp; $3 is infs-preserving );
defpred S2[ LATTICE, LATTICE, Function of $1,$2] means ( $1 is complete &amp; $2 is complete &amp; $3 is sups-preserving );
A1: for a, b being LATTICE
for f being Function of a,b holds
( f in the Arrows of (W -INF_category) . (a,b) iff ( a in the carrier of (W -INF_category) &amp; b in the carrier of (W -INF_category) &amp; S1[a,b,f] ) ) by Lm3;
A2: for a, b being LATTICE
for f being Function of a,b holds
( f in the Arrows of (W -SUP_category) . (a,b) iff ( a in the carrier of (W -SUP_category) &amp; b in the carrier of (W -SUP_category) &amp; S2[a,b,f] ) ) by Lm4;
A3: for a being LATTICE st a in the carrier of (W -INF_category) holds
H1(a) in the carrier of (W -SUP_category) by Th17;
A4: for a, b being LATTICE
for f being Function of a,b st S1[a,b,f] holds
( H2(a,b,f) is Function of H1(b),H1(a) &amp; S2[H1(b),H1(a),H2(a,b,f)] ) ;
A5: now__::_thesis:_for_a_being_LATTICE_st_a_in_the_carrier_of_(W_-INF_category)_holds_
H2(a,a,_id_a)_=_id_H1(a)
let a be LATTICE; ::_thesis: ( a in the carrier of (W -INF_category) implies H2(a,a, id a) = id H1(a) )
assume  a in the carrier of (W -INF_category) ; ::_thesis: H2(a,a, id a) = id H1(a)
then  a is complete by YELLOW21:def_5;
hence  H2(a,a, id a) = id H1(a) by Th7; ::_thesis: verum
end;
A6: for a, b, c being LATTICE
for f being Function of a,b
for g being Function of b,c st S1[a,b,f] &amp; S1[b,c,g] holds
H2(a,c,g * f) = H2(a,b,f) * H2(b,c,g) by Th8;
funcW LowerAdj  ->  strict contravariant Functor of W -INF_category ,W -SUP_category  means :Def6: :: WAYBEL34:def 6
( ( for a being object of (W -INF_category) holds it . a = latt a ) &amp; ( for a, b being object of (W -INF_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds it . f = LowerAdj (@ f) ) );
existence
 ex b1 being strict contravariant Functor of W -INF_category ,W -SUP_category st
( ( for a being object of (W -INF_category) holds b1 . a = latt a ) &amp; ( for a, b being object of (W -INF_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds b1 . f = LowerAdj (@ f) ) )
proofend;
uniqueness
 for b1, b2 being strict contravariant Functor of W -INF_category ,W -SUP_category st ( for a being object of (W -INF_category) holds b1 . a = latt a ) &amp; ( for a, b being object of (W -INF_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds b1 . f = LowerAdj (@ f) ) &amp; ( for a being object of (W -INF_category) holds b2 . a = latt a ) &amp; ( for a, b being object of (W -INF_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds b2 . f = LowerAdj (@ f) ) holds
b1 = b2
proofend;
deffunc H3( LATTICE, LATTICE, Function of $1,$2) ->  Function of $2,$1 = UpperAdj $3;
A13: for a being LATTICE st a in the carrier of (W -SUP_category) holds
H1(a) in the carrier of (W -INF_category) by Th17;
A14: for a, b being LATTICE
for f being Function of a,b st S2[a,b,f] holds
( H3(a,b,f) is Function of H1(b),H1(a) &amp; S1[H1(b),H1(a),H3(a,b,f)] ) ;
A15: now__::_thesis:_for_a_being_LATTICE_st_a_in_the_carrier_of_(W_-SUP_category)_holds_
H3(a,a,_id_a)_=_id_H1(a)
let a be LATTICE; ::_thesis: ( a in the carrier of (W -SUP_category) implies H3(a,a, id a) = id H1(a) )
assume  a in the carrier of (W -SUP_category) ; ::_thesis: H3(a,a, id a) = id H1(a)
then  a is complete by YELLOW21:def_5;
hence  H3(a,a, id a) = id H1(a) by Th7; ::_thesis: verum
end;
A16: for a, b, c being LATTICE
for f being Function of a,b
for g being Function of b,c st S2[a,b,f] &amp; S2[b,c,g] holds
H3(a,c,g * f) = H3(a,b,f) * H3(b,c,g) by Th9;
funcW UpperAdj  ->  strict contravariant Functor of W -SUP_category ,W -INF_category  means :Def7: :: WAYBEL34:def 7
( ( for a being object of (W -SUP_category) holds it . a = latt a ) &amp; ( for a, b being object of (W -SUP_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds it . f = UpperAdj (@ f) ) );
existence
 ex b1 being strict contravariant Functor of W -SUP_category ,W -INF_category st
( ( for a being object of (W -SUP_category) holds b1 . a = latt a ) &amp; ( for a, b being object of (W -SUP_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds b1 . f = UpperAdj (@ f) ) )
proofend;
uniqueness
 for b1, b2 being strict contravariant Functor of W -SUP_category ,W -INF_category st ( for a being object of (W -SUP_category) holds b1 . a = latt a ) &amp; ( for a, b being object of (W -SUP_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds b1 . f = UpperAdj (@ f) ) &amp; ( for a being object of (W -SUP_category) holds b2 . a = latt a ) &amp; ( for a, b being object of (W -SUP_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds b2 . f = UpperAdj (@ f) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines LowerAdj WAYBEL34:def_6_:_
 for W being with_non-empty_element set
for b2 being strict contravariant Functor of W -INF_category ,W -SUP_category holds
( b2 = W LowerAdj iff ( ( for a being object of (W -INF_category) holds b2 . a = latt a ) &amp; ( for a, b being object of (W -INF_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds b2 . f = LowerAdj (@ f) ) ) );

:: deftheorem Def7 defines UpperAdj WAYBEL34:def_7_:_
 for W being with_non-empty_element set
for b2 being strict contravariant Functor of W -SUP_category ,W -INF_category holds
( b2 = W UpperAdj iff ( ( for a being object of (W -SUP_category) holds b2 . a = latt a ) &amp; ( for a, b being object of (W -SUP_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds b2 . f = UpperAdj (@ f) ) ) );

registration
let W be with_non-empty_element set ;
clusterW LowerAdj  ->  strict contravariant bijective ;
coherence
 W LowerAdj is bijective
proofend;
clusterW UpperAdj  ->  strict contravariant bijective ;
coherence
 W UpperAdj is bijective
proofend;
end;

theorem Th18: :: WAYBEL34:18
for W being with_non-empty_element set holds
( (W LowerAdj) " = W UpperAdj &amp; (W UpperAdj) " = W LowerAdj )
proofend;

theorem :: WAYBEL34:19
for W being with_non-empty_element set holds
( (W LowerAdj) * (W UpperAdj) = id (W -SUP_category) &amp; (W UpperAdj) * (W LowerAdj) = id (W -INF_category) )
proofend;

theorem :: WAYBEL34:20
for W being with_non-empty_element set holds W -INF_category ,W -SUP_category are_anti-isomorphic
proofend;

begin

::<section2>Scott continuous maps and continuous lattices</section2>
theorem Th21: :: WAYBEL34:21
for S, T being complete LATTICE
for g being infs-preserving Function of S,T holds
( g is directed-sups-preserving iff for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S
for V being open Subset of X holds uparrow ((LowerAdj g) .: V) is open Subset of Y )
proofend;

definition
let S, T be non empty reflexive RelStr ;
let f be Function of S,T;
attrf is waybelow-preserving  means :Def8: :: WAYBEL34:def 8
 for x, y being Element of S st x << y holds
f . x << f . y;
end;

:: deftheorem Def8 defines waybelow-preserving WAYBEL34:def_8_:_
 for S, T being non empty reflexive RelStr
for f being Function of S,T holds
( f is waybelow-preserving iff for x, y being Element of S st x << y holds
f . x << f . y );

theorem Th22: :: WAYBEL34:22
for S, T being complete LATTICE
for g being infs-preserving Function of S,T st g is directed-sups-preserving holds
LowerAdj g is waybelow-preserving
proofend;

theorem Th23: :: WAYBEL34:23
for S being complete LATTICE
for T being continuous complete LATTICE
for g being infs-preserving Function of S,T st LowerAdj g is waybelow-preserving holds
g is directed-sups-preserving
proofend;

definition
let S, T be TopSpace;
let f be Function of S,T;
attrf is relatively_open  means :Def9: :: WAYBEL34:def 9
 for V being open Subset of S holds f .: V is open Subset of (T | (rng f));
end;

:: deftheorem Def9 defines relatively_open WAYBEL34:def_9_:_
 for S, T being TopSpace
for f being Function of S,T holds
( f is relatively_open iff for V being open Subset of S holds f .: V is open Subset of (T | (rng f)) );

theorem :: WAYBEL34:24
for X, Y being non empty TopSpace
for d being Function of X,Y holds
( d is relatively_open iff corestr d is open )
proofend;

theorem Th25: :: WAYBEL34:25
for S, T being complete LATTICE
for g being infs-preserving Function of S,T
for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S
for V being open Subset of X holds (LowerAdj g) .: V = (rng (LowerAdj g)) /\ (uparrow ((LowerAdj g) .: V))
proofend;

theorem Th26: :: WAYBEL34:26
for S, T being complete LATTICE
for g being infs-preserving Function of S,T
for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S st ( for V being open Subset of X holds uparrow ((LowerAdj g) .: V) is open Subset of Y ) holds
for d being Function of X,Y st d = LowerAdj g holds
d is relatively_open
proofend;

registration
let X, Y be complete LATTICE;
let f be sups-preserving Function of X,Y;
cluster Image f ->  complete ;
coherence
 Image f is complete by YELLOW_2:34;
end;

theorem :: WAYBEL34:27
for S, T being complete LATTICE
for g being infs-preserving Function of S,T
for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S
for Z being Scott TopAugmentation of Image (LowerAdj g)
for d being Function of X,Y
for d9 being Function of X,Z st d = LowerAdj g &amp; d9 = d &amp; d is relatively_open holds
d9 is open
proofend;

theorem Th28: :: WAYBEL34:28
for S, T being complete LATTICE
for g being infs-preserving Function of S,T st g is V7() holds
for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S
for d being Function of X,Y st d = LowerAdj g holds
( g is directed-sups-preserving iff d is open )
proofend;

registration
let X be complete LATTICE;
let f be projection Function of X,X;
cluster Image f ->  complete ;
coherence
 Image f is complete by WAYBEL_1:54;
end;

theorem Th29: :: WAYBEL34:29
for L being complete LATTICE
for k being kernel Function of L,L holds
( corestr k is infs-preserving &amp; inclusion k is sups-preserving &amp; LowerAdj (corestr k) = inclusion k &amp; UpperAdj (inclusion k) = corestr k )
proofend;

theorem Th30: :: WAYBEL34:30
for L being complete LATTICE
for k being kernel Function of L,L holds
( k is directed-sups-preserving iff corestr k is directed-sups-preserving )
proofend;

theorem :: WAYBEL34:31
for L being complete LATTICE
for k being kernel Function of L,L holds
( k is directed-sups-preserving iff for X being Scott TopAugmentation of Image k
for Y being Scott TopAugmentation of L
for V being Subset of L st V is open Subset of X holds
uparrow V is open Subset of Y )
proofend;

theorem Th32: :: WAYBEL34:32
for L being complete LATTICE
for S being non empty full sups-inheriting SubRelStr of L
for x, y being Element of L
for a, b being Element of S st a = x &amp; b = y &amp; x << y holds
a << b
proofend;

theorem :: WAYBEL34:33
for L being complete LATTICE
for k being kernel Function of L,L st k is directed-sups-preserving holds
for x, y being Element of L
for a, b being Element of (Image k) st a = x &amp; b = y holds
( x << y iff a << b )
proofend;

theorem :: WAYBEL34:34
for L being complete LATTICE
for k being kernel Function of L,L st Image k is continuous &amp; ( for x, y being Element of L
for a, b being Element of (Image k) st a = x &amp; b = y holds
( x << y iff a << b ) ) holds
k is directed-sups-preserving
proofend;

theorem Th35: :: WAYBEL34:35
for L being complete LATTICE
for c being closure Function of L,L holds
( corestr c is sups-preserving &amp; inclusion c is infs-preserving &amp; UpperAdj (corestr c) = inclusion c &amp; LowerAdj (inclusion c) = corestr c )
proofend;

theorem Th36: :: WAYBEL34:36
for L being complete LATTICE
for c being closure Function of L,L holds
( Image c is directed-sups-inheriting iff inclusion c is directed-sups-preserving )
proofend;

theorem :: WAYBEL34:37
for L being complete LATTICE
for c being closure Function of L,L holds
( Image c is directed-sups-inheriting iff for X being Scott TopAugmentation of Image c
for Y being Scott TopAugmentation of L
for f being Function of Y,X st f = c holds
f is open )
proofend;

theorem :: WAYBEL34:38
for L being complete LATTICE
for c being closure Function of L,L st Image c is directed-sups-inheriting holds
corestr c is waybelow-preserving
proofend;

theorem :: WAYBEL34:39
for L being continuous complete LATTICE
for c being closure Function of L,L st corestr c is waybelow-preserving holds
Image c is directed-sups-inheriting
proofend;

begin

::<section3>Duality of subcategories of {\it INF} and {\it SUP}</section3>
definition
let W be non empty set ;
set A = W -INF_category ;
defpred S1[ set ] means verum;
defpred S2[ object of (W -INF_category), object of (W -INF_category), Morphism of $1,$2] means  @ $3 is directed-sups-preserving ;
A1: ex a being object of (W -INF_category) st S1[a] ;
A2: for a, b, c being object of (W -INF_category) st S1[a] &amp; S1[b] &amp; S1[c] &amp; <^a,b^> <> {} &amp; <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c st S2[a,b,f] &amp; S2[b,c,g] holds
S2[a,c,g * f]
proofend;
A8: for a being object of (W -INF_category) st S1[a] holds
S2[a,a, idm a]
proofend;
funcW -INF(SC)_category  ->  non empty strict subcategory of W -INF_category  means :Def10: :: WAYBEL34:def 10
( ( for a being object of (W -INF_category) holds a is object of it ) &amp; ( for a, b being object of (W -INF_category)
for a9, b9 being object of it st a9 = a &amp; b9 = b &amp; <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff @ f is directed-sups-preserving ) ) );
existence
 ex b1 being non empty strict subcategory of W -INF_category st
( ( for a being object of (W -INF_category) holds a is object of b1 ) &amp; ( for a, b being object of (W -INF_category)
for a9, b9 being object of b1 st a9 = a &amp; b9 = b &amp; <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff @ f is directed-sups-preserving ) ) )
proofend;
correctness
uniqueness
for b1, b2 being non empty strict subcategory of W -INF_category st ( for a being object of (W -INF_category) holds a is object of b1 ) &amp; ( for a, b being object of (W -INF_category)
for a9, b9 being object of b1 st a9 = a &amp; b9 = b &amp; <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff @ f is directed-sups-preserving ) ) &amp; ( for a being object of (W -INF_category) holds a is object of b2 ) &amp; ( for a, b being object of (W -INF_category)
for a9, b9 being object of b2 st a9 = a &amp; b9 = b &amp; <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff @ f is directed-sups-preserving ) ) holds
b1 = b2;
proofend;
end;

:: deftheorem Def10 defines -INF(SC)_category WAYBEL34:def_10_:_
 for W being non empty set
for b2 being non empty strict subcategory of W -INF_category holds
( b2 = W -INF(SC)_category iff ( ( for a being object of (W -INF_category) holds a is object of b2 ) &amp; ( for a, b being object of (W -INF_category)
for a9, b9 being object of b2 st a9 = a &amp; b9 = b &amp; <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff @ f is directed-sups-preserving ) ) ) );

definition
let W be with_non-empty_element set ;
A1: ex w being non empty set st w in W by SETFAM_1:def_10;
set A = W -SUP_category ;
defpred S1[ set ] means verum;
defpred S2[ object of (W -SUP_category), object of (W -SUP_category), Morphism of $1,$2] means  UpperAdj (@ $3) is directed-sups-preserving ;
A2: ex a being object of (W -SUP_category) st S1[a] ;
A3: for a, b, c being object of (W -SUP_category) st S1[a] &amp; S1[b] &amp; S1[c] &amp; <^a,b^> <> {} &amp; <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c st S2[a,b,f] &amp; S2[b,c,g] holds
S2[a,c,g * f]
proofend;
A12: for a being object of (W -SUP_category) st S1[a] holds
S2[a,a, idm a]
proofend;
funcW -SUP(SO)_category  ->  non empty strict subcategory of W -SUP_category  means :Def11: :: WAYBEL34:def 11
( ( for a being object of (W -SUP_category) holds a is object of it ) &amp; ( for a, b being object of (W -SUP_category)
for a9, b9 being object of it st a9 = a &amp; b9 = b &amp; <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff UpperAdj (@ f) is directed-sups-preserving ) ) );
existence
 ex b1 being non empty strict subcategory of W -SUP_category st
( ( for a being object of (W -SUP_category) holds a is object of b1 ) &amp; ( for a, b being object of (W -SUP_category)
for a9, b9 being object of b1 st a9 = a &amp; b9 = b &amp; <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff UpperAdj (@ f) is directed-sups-preserving ) ) )
proofend;
correctness
uniqueness
for b1, b2 being non empty strict subcategory of W -SUP_category st ( for a being object of (W -SUP_category) holds a is object of b1 ) &amp; ( for a, b being object of (W -SUP_category)
for a9, b9 being object of b1 st a9 = a &amp; b9 = b &amp; <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff UpperAdj (@ f) is directed-sups-preserving ) ) &amp; ( for a being object of (W -SUP_category) holds a is object of b2 ) &amp; ( for a, b being object of (W -SUP_category)
for a9, b9 being object of b2 st a9 = a &amp; b9 = b &amp; <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff UpperAdj (@ f) is directed-sups-preserving ) ) holds
b1 = b2;
proofend;
end;

:: deftheorem Def11 defines -SUP(SO)_category WAYBEL34:def_11_:_
 for W being with_non-empty_element set
for b2 being non empty strict subcategory of W -SUP_category holds
( b2 = W -SUP(SO)_category iff ( ( for a being object of (W -SUP_category) holds a is object of b2 ) &amp; ( for a, b being object of (W -SUP_category)
for a9, b9 being object of b2 st a9 = a &amp; b9 = b &amp; <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff UpperAdj (@ f) is directed-sups-preserving ) ) ) );

theorem Th40: :: WAYBEL34:40
for S being non empty RelStr
for T being non empty reflexive antisymmetric RelStr
for t being Element of T
for X being non empty Subset of S holds
( S --> t preserves_sup_of X &amp; S --> t preserves_inf_of X )
proofend;

theorem Th41: :: WAYBEL34:41
for S being non empty RelStr
for T being non empty reflexive antisymmetric lower-bounded RelStr holds S --> (Bottom T) is sups-preserving
proofend;

theorem Th42: :: WAYBEL34:42
for S being non empty RelStr
for T being non empty reflexive antisymmetric upper-bounded RelStr holds S --> (Top T) is infs-preserving
proofend;

registration
let S be non empty RelStr ;
let T be non empty reflexive antisymmetric upper-bounded RelStr ;
clusterS --> (Top T) ->  infs-preserving directed-sups-preserving ;
coherence
 ( S --> (Top T) is directed-sups-preserving &amp; S --> (Top T) is infs-preserving )
proofend;
end;

registration
let S be non empty RelStr ;
let T be non empty reflexive antisymmetric lower-bounded RelStr ;
clusterS --> (Bottom T) ->  sups-preserving filtered-infs-preserving ;
coherence
 ( S --> (Bottom T) is filtered-infs-preserving &amp; S --> (Bottom T) is sups-preserving )
proofend;
end;

registration
let S be non empty RelStr ;
let T be non empty reflexive antisymmetric upper-bounded RelStr ;
cluster Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total infs-preserving directed-sups-preserving for Element of bool [: the carrier of S, the carrier of T:];
existence
 ex b1 being Function of S,T st
( b1 is directed-sups-preserving &amp; b1 is infs-preserving )
proofend;
end;

registration
let S be non empty RelStr ;
let T be non empty reflexive antisymmetric lower-bounded RelStr ;
cluster Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total sups-preserving filtered-infs-preserving for Element of bool [: the carrier of S, the carrier of T:];
existence
 ex b1 being Function of S,T st
( b1 is filtered-infs-preserving &amp; b1 is sups-preserving )
proofend;
end;

theorem Th43: :: WAYBEL34:43
for W being with_non-empty_element set
for L being LATTICE holds
( L is object of (W -INF(SC)_category) iff ( L is strict &amp; L is complete &amp; the carrier of L in W ) )
proofend;

theorem Th44: :: WAYBEL34:44
for W being with_non-empty_element set
for a, b being object of (W -INF(SC)_category)
for f being set holds
( f in <^a,b^> iff f is infs-preserving directed-sups-preserving Function of (latt a),(latt b) )
proofend;

theorem :: WAYBEL34:45
for W being with_non-empty_element set
for L being LATTICE holds
( L is object of (W -SUP(SO)_category) iff ( L is strict &amp; L is complete &amp; the carrier of L in W ) )
proofend;

theorem Th46: :: WAYBEL34:46
for W being with_non-empty_element set
for a, b being object of (W -SUP(SO)_category)
for f being set holds
( f in <^a,b^> iff ex g being sups-preserving Function of (latt a),(latt b) st
( g = f &amp; UpperAdj g is directed-sups-preserving ) )
proofend;

theorem :: WAYBEL34:47
for W being with_non-empty_element set holds W -INF(SC)_category = Intersect ((W -INF_category),(W -UPS_category))
proofend;

definition
let W be with_non-empty_element set ;
defpred S1[ object of (W -INF(SC)_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 -CL_category  ->  non empty strict full subcategory of W -INF(SC)_category  means :Def12: :: WAYBEL34:def 12
 for a being object of (W -INF(SC)_category) holds
( a is object of it iff latt a is continuous );
existence
 ex b1 being non empty strict full subcategory of W -INF(SC)_category st
for a being object of (W -INF(SC)_category) holds
( a is object of b1 iff latt a is continuous )
proofend;
correctness
uniqueness
for b1, b2 being non empty strict full subcategory of W -INF(SC)_category st ( for a being object of (W -INF(SC)_category) holds
( a is object of b1 iff latt a is continuous ) ) &amp; ( for a being object of (W -INF(SC)_category) holds
( a is object of b2 iff latt a is continuous ) ) holds
b1 = b2;
proofend;
end;

:: deftheorem Def12 defines -CL_category WAYBEL34:def_12_:_
 for W being with_non-empty_element set
for b2 being non empty strict full subcategory of W -INF(SC)_category holds
( b2 = W -CL_category iff for a being object of (W -INF(SC)_category) holds
( a is object of b2 iff latt a is continuous ) );

registration
let W be with_non-empty_element set ;
clusterW -CL_category  ->  non empty strict full with_complete_lattices ;
coherence
 W -CL_category is with_complete_lattices ;
end;

theorem Th48: :: WAYBEL34:48
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 -CL_category) iff ( L is strict &amp; L is complete &amp; L is continuous ) )
proofend;

theorem Th49: :: WAYBEL34:49
for W being with_non-empty_element set
for a, b being object of (W -CL_category)
for f being set holds
( f in <^a,b^> iff f is infs-preserving directed-sups-preserving Function of (latt a),(latt b) )
proofend;

definition
let W be with_non-empty_element set ;
defpred S1[ object of (W -SUP(SO)_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 -CL-opp_category  ->  non empty strict full subcategory of W -SUP(SO)_category  means :Def13: :: WAYBEL34:def 13
 for a being object of (W -SUP(SO)_category) holds
( a is object of it iff latt a is continuous );
existence
 ex b1 being non empty strict full subcategory of W -SUP(SO)_category st
for a being object of (W -SUP(SO)_category) holds
( a is object of b1 iff latt a is continuous )
proofend;
correctness
uniqueness
for b1, b2 being non empty strict full subcategory of W -SUP(SO)_category st ( for a being object of (W -SUP(SO)_category) holds
( a is object of b1 iff latt a is continuous ) ) &amp; ( for a being object of (W -SUP(SO)_category) holds
( a is object of b2 iff latt a is continuous ) ) holds
b1 = b2;
proofend;
end;

:: deftheorem Def13 defines -CL-opp_category WAYBEL34:def_13_:_
 for W being with_non-empty_element set
for b2 being non empty strict full subcategory of W -SUP(SO)_category holds
( b2 = W -CL-opp_category iff for a being object of (W -SUP(SO)_category) holds
( a is object of b2 iff latt a is continuous ) );

theorem Th50: :: WAYBEL34:50
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 -CL-opp_category) iff ( L is strict &amp; L is complete &amp; L is continuous ) )
proofend;

theorem Th51: :: WAYBEL34:51
for W being with_non-empty_element set
for a, b being object of (W -CL-opp_category)
for f being set holds
( f in <^a,b^> iff ex g being sups-preserving Function of (latt a),(latt b) st
( g = f &amp; UpperAdj g is directed-sups-preserving ) )
proofend;

:: 1.10. THEOREM, p. 182
theorem Th52: :: WAYBEL34:52
for W being with_non-empty_element set holds W -INF(SC)_category ,W -SUP(SO)_category are_anti-isomorphic_under W LowerAdj
proofend;

theorem :: WAYBEL34:53
for W being with_non-empty_element set holds W -SUP(SO)_category ,W -INF(SC)_category are_anti-isomorphic_under W UpperAdj
proofend;

theorem Th54: :: WAYBEL34:54
for W being with_non-empty_element set holds W -CL_category ,W -CL-opp_category are_anti-isomorphic_under W LowerAdj
proofend;

theorem :: WAYBEL34:55
for W being with_non-empty_element set holds W -CL-opp_category ,W -CL_category are_anti-isomorphic_under W UpperAdj
proofend;

begin

::<section4>Compact preserving maps and sup-semilattices morphisms</section4>
definition
let S, T be non empty reflexive RelStr ;
let f be Function of S,T;
attrf is compact-preserving  means :: WAYBEL34:def 14
 for s being Element of S st s is compact holds
f . s is compact ;
end;

:: deftheorem  defines compact-preserving WAYBEL34:def_14_:_
 for S, T being non empty reflexive RelStr
for f being Function of S,T holds
( f is compact-preserving iff for s being Element of S st s is compact holds
f . s is compact );

theorem Th56: :: WAYBEL34:56
for S, T being complete LATTICE
for d being sups-preserving Function of T,S st d is waybelow-preserving holds
d is compact-preserving
proofend;

theorem Th57: :: WAYBEL34:57
for S, T being complete LATTICE
for d being sups-preserving Function of T,S st T is algebraic &amp; d is compact-preserving holds
d is waybelow-preserving
proofend;

theorem Th58: :: WAYBEL34:58
for R, S, T being non empty RelStr
for X being Subset of R
for f being Function of R,S
for g being Function of S,T st f preserves_sup_of X &amp; g preserves_sup_of f .: X holds
g * f preserves_sup_of X
proofend;

definition
let S, T be non empty RelStr ;
let f be Function of S,T;
attrf is finite-sups-preserving  means :: WAYBEL34:def 15
 for X being finite Subset of S holds f preserves_sup_of X;
attrf is bottom-preserving  means :Def16: :: WAYBEL34:def 16
f preserves_sup_of {} S;
end;

:: deftheorem  defines finite-sups-preserving WAYBEL34:def_15_:_
 for S, T being non empty RelStr
for f being Function of S,T holds
( f is finite-sups-preserving iff for X being finite Subset of S holds f preserves_sup_of X );

:: deftheorem Def16 defines bottom-preserving WAYBEL34:def_16_:_
 for S, T being non empty RelStr
for f being Function of S,T holds
( f is bottom-preserving iff f preserves_sup_of {} S );

theorem :: WAYBEL34:59
for R, S, T being non empty RelStr
for f being Function of R,S
for g being Function of S,T st f is finite-sups-preserving &amp; g is finite-sups-preserving holds
g * f is finite-sups-preserving
proofend;

definition
let S, T be non empty antisymmetric lower-bounded RelStr ;
let f be Function of S,T;
redefine attr f is bottom-preserving  means :Def17: :: WAYBEL34:def 17
f . (Bottom S) = Bottom T;
compatibility
 ( f is bottom-preserving iff f . (Bottom S) = Bottom T )
proofend;
end;

:: deftheorem Def17 defines bottom-preserving WAYBEL34:def_17_:_
 for S, T being non empty antisymmetric lower-bounded RelStr
for f being Function of S,T holds
( f is bottom-preserving iff f . (Bottom S) = Bottom T );

definition
let L be non empty RelStr ;
let S be SubRelStr of L;
attrS is finite-sups-inheriting  means :Def18: :: WAYBEL34:def 18
 for X being finite Subset of S st ex_sup_of X,L holds
"\/" (X,L) in the carrier of S;
attrS is bottom-inheriting  means :Def19: :: WAYBEL34:def 19
 Bottom L in the carrier of S;
end;

:: deftheorem Def18 defines finite-sups-inheriting WAYBEL34:def_18_:_
 for L being non empty RelStr
for S being SubRelStr of L holds
( S is finite-sups-inheriting iff for X being finite Subset of S st ex_sup_of X,L holds
"\/" (X,L) in the carrier of S );

:: deftheorem Def19 defines bottom-inheriting WAYBEL34:def_19_:_
 for L being non empty RelStr
for S being SubRelStr of L holds
( S is bottom-inheriting iff Bottom L in the carrier of S );

registration
let S, T be non empty RelStr ;
cluster Function-like quasi_total sups-preserving  ->  bottom-preserving for Element of bool [: the carrier of S, the carrier of T:];
coherence
 for b1 being Function of S,T st b1 is sups-preserving holds
b1 is bottom-preserving
proofend;
end;

registration
let L be non empty antisymmetric lower-bounded RelStr ;
cluster finite-sups-inheriting  ->  join-inheriting bottom-inheriting for SubRelStr of L;
coherence
 for b1 being SubRelStr of L st b1 is finite-sups-inheriting holds
( b1 is bottom-inheriting &amp; b1 is join-inheriting )
proofend;
end;

registration
let L be non empty RelStr ;
cluster sups-inheriting  ->  finite-sups-inheriting for SubRelStr of L;
coherence
 for b1 being SubRelStr of L st b1 is sups-inheriting holds
b1 is finite-sups-inheriting
proofend;
end;

registration
let S, T be non empty lower-bounded Poset;
cluster Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total sups-preserving for Element of bool [: the carrier of S, the carrier of T:];
existence
 ex b1 being Function of S,T st b1 is sups-preserving
proofend;
end;

registration
let L be non empty antisymmetric lower-bounded RelStr ;
cluster full bottom-inheriting  ->  non empty lower-bounded full for SubRelStr of L;
coherence
 for b1 being full SubRelStr of L st b1 is bottom-inheriting holds
( not b1 is empty &amp; b1 is lower-bounded )
proofend;
end;

registration
let L be non empty antisymmetric lower-bounded RelStr ;
cluster non empty full sups-inheriting finite-sups-inheriting bottom-inheriting for SubRelStr of L;
existence
 ex b1 being SubRelStr of L st
( not b1 is empty &amp; b1 is sups-inheriting &amp; b1 is finite-sups-inheriting &amp; b1 is bottom-inheriting &amp; b1 is full )
proofend;
end;

theorem Th60: :: WAYBEL34:60
for L being non empty antisymmetric lower-bounded RelStr
for S being non empty full bottom-inheriting SubRelStr of L holds Bottom S = Bottom L
proofend;

registration
let L be non empty lower-bounded with_suprema Poset;
cluster full join-inheriting bottom-inheriting  ->  full finite-sups-inheriting for SubRelStr of L;
coherence
 for b1 being full SubRelStr of L st b1 is bottom-inheriting &amp; b1 is join-inheriting holds
b1 is finite-sups-inheriting
proofend;
end;

theorem Th61: :: WAYBEL34:61
for S, T being non empty RelStr
for f being Function of S,T st f is finite-sups-preserving holds
( f is join-preserving &amp; f is bottom-preserving )
proofend;

theorem Th62: :: WAYBEL34:62
for S, T being lower-bounded with_suprema Poset
for f being Function of S,T st f is join-preserving &amp; f is bottom-preserving holds
f is finite-sups-preserving
proofend;

registration
let S, T be non empty RelStr ;
cluster Function-like quasi_total sups-preserving  ->  finite-sups-preserving for Element of bool [: the carrier of S, the carrier of T:];
coherence
 for b1 being Function of S,T st b1 is sups-preserving holds
b1 is finite-sups-preserving
proofend;
cluster Function-like quasi_total finite-sups-preserving  ->  join-preserving bottom-preserving for Element of bool [: the carrier of S, the carrier of T:];
coherence
 for b1 being Function of S,T st b1 is finite-sups-preserving holds
( b1 is join-preserving &amp; b1 is bottom-preserving ) by Th61;
end;

registration
let S be non empty RelStr ;
let T be non empty reflexive antisymmetric lower-bounded RelStr ;
cluster Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total sups-preserving finite-sups-preserving for Element of bool [: the carrier of S, the carrier of T:];
existence
 ex b1 being Function of S,T st
( b1 is sups-preserving &amp; b1 is finite-sups-preserving )
proofend;
end;

registration
let L be non empty lower-bounded Poset;
cluster CompactSublatt L ->  lower-bounded ;
coherence
 CompactSublatt L is lower-bounded
proofend;
end;

theorem Th63: :: WAYBEL34:63
for S being RelStr
for T being non empty RelStr
for f being Function of S,T
for S9 being SubRelStr of S
for T9 being SubRelStr of T st f .: the carrier of S9 c= the carrier of T9 holds
f | the carrier of S9 is Function of S9,T9
proofend;

theorem Th64: :: WAYBEL34:64
for S, T being LATTICE
for f being join-preserving Function of S,T
for S9 being non empty full join-inheriting SubRelStr of S
for T9 being non empty full join-inheriting SubRelStr of T
for g being Function of S9,T9 st g = f | the carrier of S9 holds
g is join-preserving
proofend;

theorem Th65: :: WAYBEL34:65
for S, T being lower-bounded LATTICE
for f being finite-sups-preserving Function of S,T
for S9 being non empty full finite-sups-inheriting SubRelStr of S
for T9 being non empty full finite-sups-inheriting SubRelStr of T
for g being Function of S9,T9 st g = f | the carrier of S9 holds
g is finite-sups-preserving
proofend;

registration
let L be complete LATTICE;
cluster CompactSublatt L ->  finite-sups-inheriting ;
coherence
 CompactSublatt L is finite-sups-inheriting
proofend;
end;

theorem Th66: :: WAYBEL34:66
for S, T being complete LATTICE
for d being sups-preserving Function of T,S holds
( d is compact-preserving iff d | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S) )
proofend;

theorem :: WAYBEL34:67
for S, T being complete LATTICE st T is algebraic holds
for g being infs-preserving Function of S,T holds
( g is directed-sups-preserving iff (LowerAdj g) | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S) )
proofend;