:: Duality Based on Galois Connection. Part I :: by Grzegorz Bancerek :: :: Received August 8, 2001 :: Copyright (c) 2001-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies REWRITE1, WAYBEL_0, WAYBEL_1, FUNCT_1, XBOOLE_0, ORDERS_2, SEQM_3, SUBSET_1, XXREAL_0, RELAT_1, LATTICES, EQREL_1, ORDINAL2, STRUCT_0, ARYTM_0, ALTCAT_1, CAT_1, ZFMISC_1, YELLOW21, FILTER_0, WELLORD1, ORDERS_1, SETFAM_1, QC_LANG1, TARSKI, FUNCTOR0, FUNCT_2, WAYBEL11, YELLOW_9, RCOMP_1, CARD_FIL, YELLOW_0, RELAT_2, WAYBEL_3, LATTICE3, PRE_TOPC, GROUP_6, ALTCAT_2, FUNCOP_1, YELLOW20, YELLOW18, WAYBEL_8, FINSET_1, WAYBEL34; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FINSET_1, ORDERS_1, DOMAIN_1, FUNCOP_1, STRUCT_0, ORDERS_2, LATTICE3, WELLORD1, ALTCAT_1, FUNCTOR0, ALTCAT_2, YELLOW_0, WAYBEL_0, YELLOW_2, WAYBEL_1, PRE_TOPC, T_0TOPSP, WAYBEL_3, WAYBEL_8, YELLOW_7, WAYBEL11, YELLOW_9, WAYBEL18, YELLOW18, YELLOW20, YELLOW21; constructors WELLORD1, BORSUK_1, T_0TOPSP, WAYBEL_8, WAYBEL11, YELLOW_9, WAYBEL18, YELLOW18, YELLOW20, YELLOW21, WAYBEL20; registrations XBOOLE_0, SUBSET_1, SETFAM_1, RELSET_1, FUNCT_2, FINSET_1, STRUCT_0, PRE_TOPC, ORDERS_2, LATTICE3, YELLOW_0, ALTCAT_2, FUNCTOR0, WAYBEL_0, YELLOW_2, WAYBEL_1, WAYBEL_2, WAYBEL_3, YELLOW_7, WAYBEL_8, WAYBEL10, WAYBEL11, FUNCTOR2, ALTCAT_4, LATTICE5, WAYBEL17, YELLOW_9, WAYBEL21, YELLOW18, YELLOW21, RELAT_1; requirements SUBSET, BOOLE; begin ::Infs-preserving and sups-preserving maps registration let S,T be complete LATTICE; cluster Galois for Connection of S,T; end; theorem :: WAYBEL34:1 for S,T, S9,T9 being non empty RelStr st the RelStr of S = the RelStr of S9 & the RelStr of T = the RelStr of T9 for c being Connection of S,T, c9 being Connection of S9,T9 st c = c9 holds c is Galois implies c9 is Galois; definition let S,T be LATTICE; let g be Function of S,T; assume that S is complete and g is infs-preserving; func LowerAdj g -> Function of T,S means :: WAYBEL34:def 1 [g, it] is Galois; end; definition let S,T be LATTICE; let d be Function of T,S; assume that T is complete and d is sups-preserving; func UpperAdj d -> Function of S,T means :: WAYBEL34:def 2 [it, d] is Galois; end; registration let S,T be complete LATTICE; let g be infs-preserving Function of S,T; cluster LowerAdj g -> lower_adjoint; end; registration let S,T be complete LATTICE; let d be sups-preserving Function of T,S; cluster UpperAdj d -> upper_adjoint; 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); 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); definition let S,T be RelStr; let f be Function of the carrier of S, the carrier of T; func f opp -> Function of S opp, T opp equals :: WAYBEL34:def 3 f; end; registration let S,T be complete LATTICE; let g be infs-preserving Function of S,T; cluster g opp -> lower_adjoint; end; registration let S,T be complete LATTICE; let d be sups-preserving Function of S,T; cluster d opp -> upper_adjoint; 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); theorem :: WAYBEL34:5 for S,T being complete LATTICE for d being sups-preserving Function of S, T holds LowerAdj (d opp) = UpperAdj d; theorem :: WAYBEL34:6 for L be non empty RelStr holds [id L, id L] is Galois; theorem :: WAYBEL34:7 :: 1.2. LEMMA, p. 179 :: LowerAdj and UpperAdj preserve identities for L being complete LATTICE holds LowerAdj id L = id L & UpperAdj id L = id L; theorem :: WAYBEL34:8 :: 1.2. LEMMA, p. 179 :: LowerAdj preserves contravariantly composition 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); theorem :: WAYBEL34:9 :: 1.2. LEMMA, p. 179 :: UpperAdj preserves contravariantly composition 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); theorem :: WAYBEL34:10 :: 1.3. THEOREM, p. 179 for S,T being complete LATTICE for g being infs-preserving Function of S,T holds UpperAdj LowerAdj g = g; theorem :: WAYBEL34:11 :: 1.3. THEOREM, p. 179 for S,T being complete LATTICE for d being sups-preserving Function of S,T holds LowerAdj UpperAdj d = d; theorem :: WAYBEL34:12 for C being non empty AltCatStr for a,b,f being object st f in (the Arrows of C).(a,b) ex o1,o2 being Object of C st o1 = a & o2 = b & f in <^o1,o2^> & f is Morphism of o1,o2; definition :: 1.1 DEFINITION, p. 179 let W be non empty set; given w being Element of W such that w is non empty; func W-INF_category -> lattice-wise strict category means :: WAYBEL34:def 4 (for x being LATTICE holds x is Object of it iff x is strict complete & the carrier of x in W) & for a,b being Object of it, f being monotone Function of latt a, latt b holds f in <^a,b^> iff f is infs-preserving; end; definition :: 1.1 DEFINITION, p. 179 let W be non empty set; given w being Element of W such that w is non empty; func W-SUP_category -> lattice-wise strict category means :: WAYBEL34:def 5 (for x being LATTICE holds x is Object of it iff x is strict complete & the carrier of x in W) & for a,b being Object of it, f being monotone Function of latt a, latt b holds f in <^a,b^> iff f is sups-preserving; end; registration let W be with_non-empty_element set; cluster W-INF_category -> with_complete_lattices; cluster W-SUP_category -> with_complete_lattices; end; theorem :: 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 complete & the carrier of L in W; theorem :: 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; theorem :: 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 complete & the carrier of L in W; theorem :: 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; theorem :: WAYBEL34:17 for W being with_non-empty_element set holds the carrier of W-INF_category = the carrier of W-SUP_category; definition :: 1.2 LEMMA, p. 179 let W be with_non-empty_element set; func W LowerAdj -> contravariant strict Functor of W-INF_category, W-SUP_category means :: WAYBEL34:def 6 (for a being Object of W-INF_category holds it.a = latt a) & for a,b being Object of W-INF_category st <^a,b^> <> {} for f being Morphism of a,b holds it.f = LowerAdj @f; func W UpperAdj -> contravariant strict Functor of W-SUP_category, W-INF_category means :: WAYBEL34:def 7 (for a being Object of W-SUP_category holds it.a = latt a) & for a,b being Object of W-SUP_category st <^a,b^> <> {} for f being Morphism of a,b holds it.f = UpperAdj @f; end; registration let W be with_non-empty_element set; cluster W LowerAdj -> bijective; cluster W UpperAdj -> bijective; end; theorem :: WAYBEL34:18 for W being with_non-empty_element set holds W LowerAdj" = W UpperAdj & W UpperAdj" = W LowerAdj; theorem :: WAYBEL34:19 :: 1.3 THEOREM, p. 179 for W being with_non-empty_element set holds (W LowerAdj)*(W UpperAdj) = id (W-SUP_category) & (W UpperAdj)*(W LowerAdj) = id (W-INF_category); theorem :: WAYBEL34:20 :: 1.3 THEOREM, p. 179 for W being with_non-empty_element set holds W-INF_category, W-SUP_category are_anti-isomorphic; begin ::Scott continuous maps and continuous lattices theorem :: WAYBEL34:21 :: 1.4. THEOREM, (1) <=> (2), p. 180 for S,T being complete LATTICE, 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; definition let S,T be non empty reflexive RelStr; let f be Function of S,T; attr f is waybelow-preserving means :: WAYBEL34:def 8 for x,y being Element of S st x << y holds f.x << f.y; end; theorem :: WAYBEL34:22 :: 1.4. THEOREM, (1) => (3), p. 180 for S,T being complete LATTICE, g being infs-preserving Function of S,T holds g is directed-sups-preserving implies LowerAdj g is waybelow-preserving; theorem :: WAYBEL34:23 :: 1.4. THEOREM, (3+) => (1), p. 180 for S being complete LATTICE for T being complete continuous LATTICE for g being infs-preserving Function of S,T st LowerAdj g is waybelow-preserving holds g is directed-sups-preserving; definition let S,T be TopSpace; let f be Function of S,T; attr f is relatively_open means :: WAYBEL34:def 9 for V being open Subset of S holds f.:V is open Subset of T|rng f; end; 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; theorem :: WAYBEL34:25 :: requirement of 1.5. REMARK, p. 181 for S,T being complete LATTICE, 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); theorem :: WAYBEL34:26 :: 1.5. REMARK, (2) => (2'), p. 181 for S,T being complete LATTICE, 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; registration let X,Y be complete LATTICE; let f be sups-preserving Function of X,Y; cluster Image f -> complete; end; theorem :: WAYBEL34:27 :: 1.5. REMARK, (2') => (2''), p. 181 for S,T being complete LATTICE, 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, d9 being Function of X, Z st d = LowerAdj g & d9 = d holds d is relatively_open implies d9 is open; theorem :: WAYBEL34:28 :: 1.6. COROLLARY, p. 181 for S,T being complete LATTICE, g being infs-preserving Function of S,T st g is one-to-one 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; registration let X be complete LATTICE; let f be projection Function of X,X; cluster Image f -> complete; end; theorem :: WAYBEL34:29 for L being complete LATTICE, k being kernel Function of L,L holds corestr k is infs-preserving & inclusion k is sups-preserving & LowerAdj corestr k = inclusion k & UpperAdj inclusion k = corestr k; theorem :: WAYBEL34:30 for L being complete LATTICE, k being kernel Function of L,L holds k is directed-sups-preserving iff corestr k is directed-sups-preserving; theorem :: WAYBEL34:31 :: 1.7. COROLLARY, (1) <=> (2), p. 181 for L being complete LATTICE, 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; theorem :: WAYBEL34:32 for L being complete LATTICE for S being sups-inheriting non empty full SubRelStr of L for x,y being Element of L, a,b being Element of S st a = x & b = y holds x << y implies a << b; theorem :: WAYBEL34:33 :: 1.7. COROLLARY, (1) => (3), p. 181 for L being complete LATTICE, k being kernel Function of L,L st k is directed-sups-preserving for x,y being Element of L, a,b being Element of Image k st a = x & b = y holds x << y iff a << b; theorem :: WAYBEL34:34 :: 1.7. COROLLARY, (3) => (1), p. 181 for L being complete LATTICE, k being kernel Function of L,L st Image k is continuous & for x,y being Element of L, a,b being Element of Image k st a = x & b = y holds x << y iff a << b holds k is directed-sups-preserving; theorem :: WAYBEL34:35 for L being complete LATTICE, c being closure Function of L,L holds corestr c is sups-preserving & inclusion c is infs-preserving & UpperAdj corestr c = inclusion c & LowerAdj inclusion c = corestr c; theorem :: WAYBEL34:36 for L being complete LATTICE, c being closure Function of L,L holds Image c is directed-sups-inheriting iff inclusion c is directed-sups-preserving; theorem :: WAYBEL34:37 :: 1.8. COROLLARY, (1) <=> (2), p. 182 for L being complete LATTICE, 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; theorem :: WAYBEL34:38 :: 1.8. COROLLARY, (1) => (3), p. 182 for L being complete LATTICE, c being closure Function of L,L holds Image c is directed-sups-inheriting implies corestr c is waybelow-preserving; theorem :: WAYBEL34:39 :: 1.8. COROLLARY, (3) => (1), p. 182 :: SHOULD BE: :: for L being complete LATTICE, c being closure map of L,L :: st :: Image c is continuous & corestr c is waybelow-preserving :: holds Image c is directed-sups-inheriting :: ------------------------ a bug ??? for L being continuous complete LATTICE, c being closure Function of L,L st corestr c is waybelow-preserving holds Image c is directed-sups-inheriting; begin ::Duality of subcategories of {\it INF} and {\it SUP} definition :: 1.9. DEFINITION, p. 182 let W be non empty set; func W-INF(SC)_category -> strict non empty subcategory of W-INF_category means :: WAYBEL34:def 10 (for a being Object of W-INF_category holds a is Object of it) & for a,b being Object of W-INF_category for a9,b9 being Object of it st a9 = a & b9 = b & <^a,b^> <> {} for f being Morphism of a,b holds f in <^a9,b9^> iff @f is directed-sups-preserving; end; definition :: 1.9. DEFINITION, p. 182 let W be with_non-empty_element set; func W-SUP(SO)_category -> strict non empty subcategory of W-SUP_category means :: WAYBEL34:def 11 (for a being Object of W-SUP_category holds a is Object of it) & for a,b being Object of W-SUP_category for a9,b9 being Object of it st a9 = a & b9 = b & <^a,b^> <> {} for f being Morphism of a,b holds f in <^a9,b9^> iff UpperAdj @f is directed-sups-preserving; end; theorem :: WAYBEL34:40 for S being non empty RelStr, 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 & S --> t preserves_inf_of X; theorem :: WAYBEL34:41 for S being non empty RelStr for T being lower-bounded non empty reflexive antisymmetric RelStr holds S --> Bottom T is sups-preserving; theorem :: WAYBEL34:42 for S being non empty RelStr for T being upper-bounded non empty reflexive antisymmetric RelStr holds S --> Top T is infs-preserving; registration :: WAYBEL24 let S be non empty RelStr; let T be upper-bounded non empty reflexive antisymmetric RelStr; cluster S --> Top T -> directed-sups-preserving infs-preserving; end; registration let S be non empty RelStr; let T be lower-bounded non empty reflexive antisymmetric RelStr; cluster S --> Bottom T -> filtered-infs-preserving sups-preserving; end; registration let S be non empty RelStr; let T be upper-bounded non empty reflexive antisymmetric RelStr; cluster directed-sups-preserving infs-preserving for Function of S, T; end; registration let S be non empty RelStr; let T be lower-bounded non empty reflexive antisymmetric RelStr; cluster filtered-infs-preserving sups-preserving for Function of S, T; end; theorem :: 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 complete & the carrier of L in W; theorem :: 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 directed-sups-preserving infs-preserving Function of latt a, latt b; 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 complete & the carrier of L in W; theorem :: 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 & UpperAdj g is directed-sups-preserving; theorem :: WAYBEL34:47 :: Remark after 1.9. DEFINITION, p. 182 for W being with_non-empty_element set holds W-INF(SC)_category = Intersect(W-INF_category, W-UPS_category); definition :: 1.9. DEFINITION, p. 182 let W be with_non-empty_element set; func W-CL_category -> strict full non empty subcategory of W-INF(SC)_category means :: WAYBEL34:def 12 for a being Object of W-INF(SC)_category holds a is Object of it iff latt a is continuous; end; registration let W be with_non-empty_element set; cluster W-CL_category -> with_complete_lattices; end; theorem :: 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 complete continuous; theorem :: 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; definition :: 1.9. DEFINITION, p. 182 let W be with_non-empty_element set; func W-CL-opp_category -> strict full non empty subcategory of W-SUP(SO)_category means :: WAYBEL34:def 13 for a being Object of W-SUP(SO)_category holds a is Object of it iff latt a is continuous; end; theorem :: 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 complete continuous; theorem :: 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 & UpperAdj g is directed-sups-preserving; :: 1.10. THEOREM, p. 182 theorem :: 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; 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; theorem :: WAYBEL34:54 for W being with_non-empty_element set holds W-CL_category, W-CL-opp_category are_anti-isomorphic_under W LowerAdj; 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; begin ::Compact preserving maps and sup-semilattices morphisms definition let S,T be non empty reflexive RelStr; let f be Function of S,T; attr f is compact-preserving means :: WAYBEL34:def 14 for s being Element of S st s is compact holds f.s is compact; end; theorem :: WAYBEL34:56 :: 1.11. PROPOSITION, (1) => (2) p.183 for S,T being complete LATTICE, d being sups-preserving Function of T,S st d is waybelow-preserving holds d is compact-preserving; theorem :: WAYBEL34:57 :: 1.11. PROPOSITION, (2) => (1) p.183 for S,T being complete LATTICE, d being sups-preserving Function of T,S st T is algebraic & d is compact-preserving holds d is waybelow-preserving; theorem :: WAYBEL34:58 for R,S,T being non empty RelStr, 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 & g preserves_sup_of f.:X holds g*f preserves_sup_of X; definition let S,T be non empty RelStr; let f be Function of S,T; attr f is finite-sups-preserving means :: WAYBEL34:def 15 for X being finite Subset of S holds f preserves_sup_of X; attr f is bottom-preserving means :: WAYBEL34:def 16 f preserves_sup_of {}S; end; 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 & g is finite-sups-preserving holds g*f is finite-sups-preserving; 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 :: WAYBEL34:def 17 f.Bottom S = Bottom T; end; definition let L be non empty RelStr; let S be SubRelStr of L; attr S is finite-sups-inheriting means :: WAYBEL34:def 18 for X being finite Subset of S st ex_sup_of X,L holds "\/"(X,L) in the carrier of S; attr S is bottom-inheriting means :: WAYBEL34:def 19 Bottom L in the carrier of S; end; registration let S,T be non empty RelStr; cluster sups-preserving -> bottom-preserving for Function of S,T; end; registration let L be lower-bounded antisymmetric non empty RelStr; cluster finite-sups-inheriting -> bottom-inheriting join-inheriting for SubRelStr of L; end; registration let L be non empty RelStr; cluster sups-inheriting -> finite-sups-inheriting for SubRelStr of L; end; registration let S,T be lower-bounded non empty Poset; cluster sups-preserving for Function of S,T; end; registration let L be lower-bounded antisymmetric non empty RelStr; cluster bottom-inheriting -> non empty lower-bounded for full SubRelStr of L; end; registration let L be lower-bounded antisymmetric non empty RelStr; cluster non empty sups-inheriting finite-sups-inheriting bottom-inheriting full for SubRelStr of L; end; theorem :: WAYBEL34:60 for L being lower-bounded antisymmetric non empty RelStr for S being non empty bottom-inheriting full SubRelStr of L holds Bottom S = Bottom L; registration let L be with_suprema lower-bounded non empty Poset; cluster bottom-inheriting join-inheriting -> finite-sups-inheriting for full SubRelStr of L; end; theorem :: WAYBEL34:61 for S,T being non empty RelStr, f being Function of S,T st f is finite-sups-preserving holds f is join-preserving bottom-preserving; theorem :: WAYBEL34:62 for S,T being lower-bounded with_suprema Poset, f being Function of S,T st f is join-preserving bottom-preserving holds f is finite-sups-preserving; registration let S,T be non empty RelStr; cluster sups-preserving -> finite-sups-preserving for Function of S,T; cluster finite-sups-preserving -> join-preserving bottom-preserving for Function of S,T; end; registration let S be non empty RelStr; let T be lower-bounded non empty reflexive antisymmetric RelStr; cluster sups-preserving finite-sups-preserving for Function of S,T; end; registration :: WAYBEL13:15 let L be lower-bounded non empty Poset; cluster CompactSublatt L -> lower-bounded; end; theorem :: WAYBEL34:63 for S being RelStr, T being non empty RelStr, 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; theorem :: WAYBEL34:64 for S,T being LATTICE, f being join-preserving Function of S,T for S9 being non empty join-inheriting full SubRelStr of S for T9 being non empty join-inheriting full SubRelStr of T for g being Function of S9, T9 st g = f|the carrier of S9 holds g is join-preserving; theorem :: WAYBEL34:65 for S,T being lower-bounded LATTICE for f being finite-sups-preserving Function of S,T for S9 being non empty finite-sups-inheriting full SubRelStr of S for T9 being non empty finite-sups-inheriting full SubRelStr of T for g being Function of S9, T9 st g = f|the carrier of S9 holds g is finite-sups-preserving; registration let L be complete LATTICE; cluster CompactSublatt L -> finite-sups-inheriting; end; theorem :: 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; theorem :: WAYBEL34:67 :: 1.12. COROLLARY, p. 183 for S,T being complete LATTICE st T is algebraic 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;