Journal of Formalized Mathematics
Volume 13, 2001
University of Bialystok
Copyright (c) 2001
Association of Mizar Users
The abstract of the Mizar article:
-
- by
- Grzegorz Bancerek
- Received August 8, 2001
- MML identifier: WAYBEL34
- [
Mizar article,
MML identifier index
]
environ
vocabulary BHSP_3, WAYBEL_0, WAYBEL_1, PRE_TOPC, ORDERS_1, SEQM_3, FUNCT_1,
RELAT_1, LATTICES, ORDINAL2, OPPCAT_1, ALTCAT_1, CAT_1, WELLORD1,
YELLOW21, FILTER_0, TRIANG_1, QC_LANG1, FUNCTOR0, BOOLE, SGRAPH1,
WAYBEL11, YELLOW_9, QUANTAL1, YELLOW_0, SUBSET_1, RELAT_2, WAYBEL_3,
LATTICE3, GROUP_6, ALTCAT_2, FUNCOP_1, CANTOR_1, YELLOW20, YELLOW18,
COMPTS_1, WAYBEL_8, FINSET_1, WAYBEL34;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELSET_1, FUNCT_1,
FUNCT_2, BINOP_1, FINSET_1, STRUCT_0, ORDERS_1, LATTICE3, GRCAT_1,
BORSUK_1, TRIANG_1, 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 RELAT_2, GRCAT_1, TOPS_2, T_0TOPSP, WAYBEL_1, WAYBEL_8, WAYBEL11,
YELLOW_9, QUANTAL1, WAYBEL18, YELLOW18, YELLOW20, YELLOW21, BORSUK_1,
MEMBERED;
clusters RELSET_1, FUNCT_1, PRE_TOPC, FINSET_1, RLVECT_2, STRUCT_0, LATTICE3,
YELLOW_0, WAYBEL_0, LATTICE5, YELLOW_2, WAYBEL_1, WAYBEL_2, TRIANG_1,
WAYBEL_8, YELLOW_7, WAYBEL11, YELLOW_9, WAYBEL_3, TOPS_1, WAYBEL10,
WAYBEL17, WAYBEL21, YELLOW21, ALTCAT_4, FUNCTOR0, FUNCTOR2, MEMBERED,
ZFMISC_1;
requirements SUBSET, BOOLE;
begin
::<section1>Infs-preserving and sups-preserving maps</section1>
definition
let S,T be complete LATTICE;
cluster Galois Connection of S,T;
end;
theorem :: WAYBEL34:1
for S,T, S',T' being non empty RelStr
st the RelStr of S = the RelStr of S' & the RelStr of T = the RelStr of T'
for c being Connection of S,T, c' being Connection of S',T' st c = c'
holds c is Galois implies c' is Galois;
definition
let S,T be LATTICE;
let g be map of S,T;
assume S is complete & T is complete & g is infs-preserving;
func LowerAdj g -> map of T,S means
:: WAYBEL34:def 1
[g, it] is Galois;
end;
definition
let S,T be LATTICE;
let d be map of T,S;
assume S is complete & T is complete & d is sups-preserving;
func UpperAdj d -> map of S,T means
:: WAYBEL34:def 2
[it, d] is Galois;
end;
definition
let S,T be complete LATTICE;
let g be infs-preserving map of S,T;
cluster LowerAdj g -> lower_adjoint;
end;
definition
let S,T be complete LATTICE;
let d be sups-preserving map of T,S;
cluster UpperAdj d -> upper_adjoint;
end;
theorem :: WAYBEL34:2
for S,T being complete LATTICE
for g being infs-preserving map 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 map 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 -> map of S opp, T opp equals
:: WAYBEL34:def 3
f;
end;
definition
let S,T be complete LATTICE;
let g be infs-preserving map of S,T;
cluster g opp -> lower_adjoint;
end;
definition
let S,T be complete LATTICE;
let d be sups-preserving map of S,T;
cluster d opp -> upper_adjoint;
end;
theorem :: WAYBEL34:4
for S,T being complete LATTICE
for g being infs-preserving map of S, T
holds LowerAdj g = UpperAdj (g opp);
theorem :: WAYBEL34:5
for S,T being complete LATTICE
for d being sups-preserving map 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 map of L1,L2
for g2 being infs-preserving map 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 map of L1,L2
for d2 being sups-preserving map 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 map 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 map of S,T
holds LowerAdj UpperAdj d = d;
theorem :: WAYBEL34:12
for C being non empty AltCatStr
for a,b,f being set 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 map 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 map of latt a, latt b
holds f in <^a,b^> iff f is sups-preserving;
end;
definition
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 map 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 map 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;
definition
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
::<section2>Scott continuous maps and continuous lattices</section2>
canceled 2;
theorem :: WAYBEL34:23 :: 1.4. THEOREM, (1) <=> (2), p. 180
for S,T being complete LATTICE, g being infs-preserving map 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 map 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:24 :: 1.4. THEOREM, (1) => (3), p. 180
for S,T being complete LATTICE, g being infs-preserving map of S,T
holds
g is directed-sups-preserving implies LowerAdj g is waybelow-preserving;
theorem :: WAYBEL34:25 :: 1.4. THEOREM, (3+) => (1), p. 180
for S being complete LATTICE
for T being complete continuous LATTICE
for g being infs-preserving map of S,T
st LowerAdj g is waybelow-preserving
holds g is directed-sups-preserving;
definition
let S,T be TopSpace;
let f be map 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:26
for X,Y being non empty TopSpace
for d being map of X, Y holds
d is relatively_open iff corestr d is open;
theorem :: WAYBEL34:27 :: requirement of 1.5. REMARK, p. 181
for S,T being complete LATTICE, g being infs-preserving map 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:28 :: 1.5. REMARK, (2) => (2'), p. 181
for S,T being complete LATTICE, g being infs-preserving map 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 map of X, Y st d = LowerAdj g
holds d is relatively_open;
definition
let X,Y be complete LATTICE;
let f be sups-preserving map of X,Y;
cluster Image f -> complete;
end;
theorem :: WAYBEL34:29 :: 1.5. REMARK, (2') => (2''), p. 181
for S,T being complete LATTICE, g being infs-preserving map 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 map of X, Y, d' being map of X, Z st d = LowerAdj g & d' = d
holds d is relatively_open implies d' is open;
theorem :: WAYBEL34:30
for T1, T2, S1, S2 being TopStruct
st the TopStruct of T1 = the TopStruct of T2 &
the TopStruct of S1 = the TopStruct of S2
holds S1 is SubSpace of T1 implies S2 is SubSpace of T2;
theorem :: WAYBEL34:31
for T being TopStruct holds T|[#]T = the TopStruct of T;
theorem :: WAYBEL34:32 :: 1.6. COROLLARY, p. 181
for S,T being complete LATTICE, g being infs-preserving map 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 map of X,Y st d = LowerAdj g holds
g is directed-sups-preserving iff d is open;
definition
let X be complete LATTICE;
let f be projection map of X,X;
cluster Image f -> complete;
end;
theorem :: WAYBEL34:33
for L being complete LATTICE, k being kernel map 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:34
for L being complete LATTICE, k being kernel map of L,L holds
k is directed-sups-preserving
iff
corestr k is directed-sups-preserving;
theorem :: WAYBEL34:35 :: 1.7. COROLLARY, (1) <=> (2), p. 181
for L being complete LATTICE, k being kernel map 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:36
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:37 :: 1.7. COROLLARY, (1) => (3), p. 181
for L being complete LATTICE, k being kernel map 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:38 :: 1.7. COROLLARY, (3) => (1), p. 181
for L being complete LATTICE, k being kernel map 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:39
for L being complete LATTICE, c being closure map 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:40
for L being complete LATTICE, c being closure map of L,L holds
Image c is directed-sups-inheriting
iff
inclusion c is directed-sups-preserving;
theorem :: WAYBEL34:41 :: 1.8. COROLLARY, (1) <=> (2), p. 182
for L being complete LATTICE, c being closure map 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 map of Y,X st f = c holds f is open;
theorem :: WAYBEL34:42 :: 1.8. COROLLARY, (1) => (3), p. 182
for L being complete LATTICE, c being closure map of L,L holds
Image c is directed-sups-inheriting
implies
corestr c is waybelow-preserving;
theorem :: WAYBEL34:43 :: 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 map of L,L
st
corestr c is waybelow-preserving
holds
Image c is directed-sups-inheriting;
begin
::<section3>Duality of subcategories of {\it INF} and {\it SUP}</section3>
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 a',b' being object of it st a' = a & b' = b & <^a,b^> <> {}
for f being Morphism of a,b holds
f in <^a',b'^> 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 a',b' being object of it st a' = a & b' = b & <^a,b^> <> {}
for f being Morphism of a,b holds
f in <^a',b'^> iff UpperAdj @f is directed-sups-preserving);
end;
theorem :: WAYBEL34:44
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:45
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:46
for S being non empty RelStr
for T being upper-bounded non empty reflexive antisymmetric RelStr
holds S --> Top T is infs-preserving;
definition :: 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;
definition
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;
definition
let S be non empty RelStr;
let T be upper-bounded non empty reflexive antisymmetric RelStr;
cluster directed-sups-preserving infs-preserving map of S, T;
end;
definition
let S be non empty RelStr;
let T be lower-bounded non empty reflexive antisymmetric RelStr;
cluster filtered-infs-preserving sups-preserving map of S, T;
end;
theorem :: WAYBEL34:47
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:48
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 map of latt a, latt b;
theorem :: WAYBEL34:49
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:50
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 map of latt a, latt b st g = f &
UpperAdj g is directed-sups-preserving;
theorem :: WAYBEL34:51 :: 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;
definition
let W be with_non-empty_element set;
:: COS ZLE!!! To jest wniosek z rejestracji warunkowej YELLOW21:condreg 9,
:: a jest potrzebna rejstracja aby zadzialalo nizej
cluster W-CL_category -> with_complete_lattices;
end;
theorem :: WAYBEL34:52
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:53
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 map 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:54
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:55
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 map of latt a, latt b st g = f &
UpperAdj g is directed-sups-preserving;
:: 1.10. THEOREM, p. 182
::::::::::::::::::::::::::::::::::::::
theorem :: WAYBEL34:56
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:57
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:58
for W being with_non-empty_element set holds
W-CL_category, W-CL-opp_category are_anti-isomorphic_under W LowerAdj;
theorem :: WAYBEL34:59
for W being with_non-empty_element set holds
W-CL-opp_category, W-CL_category are_anti-isomorphic_under W UpperAdj;
begin
::<section4>Compact preserving maps and sup-semilattices morphisms</section4>
definition
let S,T be non empty reflexive RelStr;
let f be map 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:60 :: 1.11. PROPOSITION, (1) => (2) p.183
for S,T being complete LATTICE, d being sups-preserving map of T,S
st d is waybelow-preserving
holds d is compact-preserving;
theorem :: WAYBEL34:61 :: 1.11. PROPOSITION, (2) => (1) p.183
for S,T being complete LATTICE, d being sups-preserving map of T,S
st T is algebraic & d is compact-preserving
holds d is waybelow-preserving;
theorem :: WAYBEL34:62
for R,S,T being non empty RelStr, X being Subset of R
for f being map of R,S for g being map 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 map 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:63
for R,S,T being non empty RelStr
for f being map of R,S for g being map 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 map 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;
definition
let S,T be non empty RelStr;
cluster sups-preserving -> bottom-preserving map of S,T;
end;
definition
let L be lower-bounded antisymmetric non empty RelStr;
cluster finite-sups-inheriting ->
bottom-inheriting join-inheriting SubRelStr of L;
end;
definition
let L be non empty RelStr;
cluster sups-inheriting -> finite-sups-inheriting SubRelStr of L;
end;
definition
let S,T be lower-bounded non empty Poset;
cluster sups-preserving map of S,T;
end;
definition
let L be lower-bounded antisymmetric non empty RelStr;
cluster bottom-inheriting -> non empty lower-bounded (full SubRelStr of L);
end;
definition
let L be lower-bounded antisymmetric non empty RelStr;
cluster non empty sups-inheriting finite-sups-inheriting bottom-inheriting
full SubRelStr of L;
end;
theorem :: WAYBEL34:64
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;
definition
let L be with_suprema lower-bounded non empty Poset;
cluster bottom-inheriting join-inheriting -> finite-sups-inheriting
(full SubRelStr of L);
end;
theorem :: WAYBEL34:65
for S,T being non empty RelStr, f being map of S,T
st f is finite-sups-preserving
holds f is join-preserving bottom-preserving;
theorem :: WAYBEL34:66
for S,T being lower-bounded with_suprema Poset, f being map of S,T
st f is join-preserving bottom-preserving
holds f is finite-sups-preserving;
definition
let S,T be non empty RelStr;
cluster sups-preserving -> finite-sups-preserving map of S,T;
cluster finite-sups-preserving ->
join-preserving bottom-preserving map of S,T;
end;
definition
let S be non empty RelStr;
let T be lower-bounded non empty reflexive antisymmetric RelStr;
cluster sups-preserving finite-sups-preserving map of S,T;
end;
definition :: WAYBEL13:15
let L be lower-bounded non empty Poset;
cluster CompactSublatt L -> lower-bounded;
end;
theorem :: WAYBEL34:67
for S being RelStr, T being non empty RelStr, f being map of S,T
for S' being SubRelStr of S
for T' being SubRelStr of T
st f.:the carrier of S' c= the carrier of T'
holds f|the carrier of S' is map of S', T';
theorem :: WAYBEL34:68
for S,T being LATTICE, f being join-preserving map of S,T
for S' being non empty join-inheriting full SubRelStr of S
for T' being non empty join-inheriting full SubRelStr of T
for g being map of S', T' st g = f|the carrier of S'
holds g is join-preserving;
theorem :: WAYBEL34:69
for S,T being lower-bounded LATTICE
for f being finite-sups-preserving map of S,T
for S' being non empty finite-sups-inheriting full SubRelStr of S
for T' being non empty finite-sups-inheriting full SubRelStr of T
for g being map of S', T' st g = f|the carrier of S'
holds g is finite-sups-preserving;
definition
let L be complete LATTICE;
cluster CompactSublatt L -> finite-sups-inheriting;
end;
theorem :: WAYBEL34:70
for S,T being complete LATTICE
for d being sups-preserving map of T,S holds
d is compact-preserving
iff
d|the carrier of CompactSublatt T is
finite-sups-preserving map of CompactSublatt T, CompactSublatt S;
theorem :: WAYBEL34:71 :: 1.12. COROLLARY, p. 183
for S,T being complete LATTICE st T is algebraic
for g being infs-preserving map of S,T holds
g is directed-sups-preserving
iff
(LowerAdj g)|the carrier of CompactSublatt T is
finite-sups-preserving map of CompactSublatt T, CompactSublatt S;
Back to top