Journal of Formalized Mathematics
Volume 10, 1998
University of Bialystok
Copyright (c) 1998
Association of Mizar Users
The abstract of the Mizar article:
-
- by
- Robert Milewski
- Received November 28, 1998
- MML identifier: WAYBEL23
- [
Mizar article,
MML identifier index
]
environ
vocabulary ORDERS_1, WAYBEL_8, WAYBEL_3, BOOLE, WAYBEL_0, COMPTS_1, RELAT_2,
YELLOW_1, TARSKI, FILTER_2, YELLOW_0, ORDINAL2, LATTICE3, LATTICES,
FINSET_1, CAT_1, BHSP_3, QUANTAL1, FILTER_0, PRE_TOPC, CARD_1, SETFAM_1,
ORDINAL1, SUBSET_1, REALSET1, FUNCT_1, WELLORD2, RELAT_1, SEQM_3,
YELLOW_2, WAYBEL_1, WELLORD1, SGRAPH1, WAYBEL23, RLVECT_3;
notation TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, REALSET1, FUNCT_1,
STRUCT_0, FUNCT_2, FINSET_1, ORDINAL1, ORDINAL2, CARD_1, PRE_TOPC,
ORDERS_1, CANTOR_1, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_0,
WAYBEL_1, WAYBEL_3, WAYBEL_8;
constructors TOPS_2, CANTOR_1, LATTICE3, ORDERS_3, YELLOW_3, WAYBEL_1,
WAYBEL_3, WAYBEL_8;
clusters STRUCT_0, FINSET_1, CARD_1, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2,
WAYBEL_0, WAYBEL_3, WAYBEL_7, WAYBEL_8, WAYBEL14, RELSET_1, SUBSET_1,
XBOOLE_0;
requirements SUBSET, BOOLE;
begin :: Preliminaries
theorem :: WAYBEL23:1
for L be non empty Poset
for x be Element of L holds
compactbelow x = waybelow x /\ the carrier of CompactSublatt L;
definition
let L be non empty reflexive transitive RelStr;
let X be Subset of InclPoset Ids L;
redefine func union X -> Subset of L;
end;
theorem :: WAYBEL23:2
for L be non empty RelStr
for X,Y be Subset of L st X c= Y holds
finsups X c= finsups Y;
theorem :: WAYBEL23:3
for L be non empty transitive RelStr
for S be sups-inheriting non empty full SubRelStr of L
for X be Subset of L
for Y be Subset of S st X = Y holds
finsups X c= finsups Y;
theorem :: WAYBEL23:4
for L be complete transitive antisymmetric (non empty RelStr)
for S be sups-inheriting non empty full SubRelStr of L
for X be Subset of L
for Y be Subset of S st X = Y holds
finsups X = finsups Y;
theorem :: WAYBEL23:5
for L be complete sup-Semilattice
for S be join-inheriting non empty full SubRelStr of L
st Bottom L in the carrier of S
for X be Subset of L
for Y be Subset of S st X = Y holds
finsups Y c= finsups X;
theorem :: WAYBEL23:6
for L be lower-bounded sup-Semilattice
for X be Subset of InclPoset Ids L holds
sup X = downarrow finsups union X;
theorem :: WAYBEL23:7
for L be reflexive transitive RelStr
for X be Subset of L holds
downarrow downarrow X = downarrow X;
theorem :: WAYBEL23:8
for L be reflexive transitive RelStr
for X be Subset of L holds
uparrow uparrow X = uparrow X;
theorem :: WAYBEL23:9
for L be non empty reflexive transitive RelStr
for x be Element of L holds
downarrow downarrow x = downarrow x;
theorem :: WAYBEL23:10
for L be non empty reflexive transitive RelStr
for x be Element of L holds
uparrow uparrow x = uparrow x;
theorem :: WAYBEL23:11
for L be non empty RelStr
for S be non empty SubRelStr of L
for X be Subset of L
for Y be Subset of S st X = Y holds
downarrow Y c= downarrow X;
theorem :: WAYBEL23:12
for L be non empty RelStr
for S be non empty SubRelStr of L
for X be Subset of L
for Y be Subset of S st X = Y holds
uparrow Y c= uparrow X;
theorem :: WAYBEL23:13
for L be non empty RelStr
for S be non empty SubRelStr of L
for x be Element of L
for y be Element of S st x = y holds
downarrow y c= downarrow x;
theorem :: WAYBEL23:14
for L be non empty RelStr
for S be non empty SubRelStr of L
for x be Element of L
for y be Element of S st x = y holds
uparrow y c= uparrow x;
begin :: Relational Subsets
definition
let L be non empty RelStr;
let S be Subset of L;
attr S is meet-closed means
:: WAYBEL23:def 1
subrelstr S is meet-inheriting;
end;
definition
let L be non empty RelStr;
let S be Subset of L;
attr S is join-closed means
:: WAYBEL23:def 2
subrelstr S is join-inheriting;
end;
definition
let L be non empty RelStr;
let S be Subset of L;
attr S is infs-closed means
:: WAYBEL23:def 3
subrelstr S is infs-inheriting;
end;
definition
let L be non empty RelStr;
let S be Subset of L;
attr S is sups-closed means
:: WAYBEL23:def 4
subrelstr S is sups-inheriting;
end;
definition
let L be non empty RelStr;
cluster infs-closed -> meet-closed Subset of L;
cluster sups-closed -> join-closed Subset of L;
end;
definition
let L be non empty RelStr;
cluster infs-closed sups-closed non empty Subset of L;
end;
theorem :: WAYBEL23:15
for L be non empty RelStr
for S be Subset of L holds
S is meet-closed iff
for x,y be Element of L st x in S & y in S & ex_inf_of {x,y},L
holds inf {x,y} in S;
theorem :: WAYBEL23:16
for L be non empty RelStr
for S be Subset of L holds
S is join-closed iff
for x,y be Element of L st x in S & y in S & ex_sup_of {x,y},L
holds sup {x,y} in S;
theorem :: WAYBEL23:17
for L be antisymmetric with_infima RelStr
for S be Subset of L holds
S is meet-closed iff
for x,y be Element of L st x in S & y in S holds inf {x,y} in S;
theorem :: WAYBEL23:18
for L be antisymmetric with_suprema RelStr
for S be Subset of L holds
S is join-closed iff
for x,y be Element of L st x in S & y in S holds sup {x,y} in S;
theorem :: WAYBEL23:19
for L be non empty RelStr
for S be Subset of L holds
S is infs-closed iff
for X be Subset of S st ex_inf_of X,L holds "/\"(X,L) in S;
theorem :: WAYBEL23:20
for L be non empty RelStr
for S be Subset of L holds
S is sups-closed iff
for X be Subset of S st ex_sup_of X,L holds "\/"(X,L) in S;
theorem :: WAYBEL23:21
for L be non empty transitive RelStr
for S be infs-closed non empty Subset of L
for X be Subset of S st ex_inf_of X,L holds
ex_inf_of X,subrelstr S & "/\"(X,subrelstr S) = "/\"(X,L);
theorem :: WAYBEL23:22
for L be non empty transitive RelStr
for S be sups-closed non empty Subset of L
for X be Subset of S st ex_sup_of X,L holds
ex_sup_of X,subrelstr S & "\/"(X,subrelstr S) = "\/"(X,L);
theorem :: WAYBEL23:23
for L be non empty transitive RelStr
for S be meet-closed non empty Subset of L
for x,y be Element of S st ex_inf_of {x,y},L holds
ex_inf_of {x,y},subrelstr S & "/\"({x,y},subrelstr S) = "/\"({x,y},L);
theorem :: WAYBEL23:24
for L be non empty transitive RelStr
for S be join-closed non empty Subset of L
for x,y be Element of S st ex_sup_of {x,y},L holds
ex_sup_of {x,y},subrelstr S & "\/"({x,y},subrelstr S) = "\/"({x,y},L);
theorem :: WAYBEL23:25
for L be with_infima antisymmetric transitive RelStr
for S be non empty meet-closed Subset of L holds
subrelstr S is with_infima;
theorem :: WAYBEL23:26
for L be with_suprema antisymmetric transitive RelStr
for S be non empty join-closed Subset of L holds
subrelstr S is with_suprema;
definition
let L be with_infima antisymmetric transitive RelStr;
let S be non empty meet-closed Subset of L;
cluster subrelstr S -> with_infima;
end;
definition
let L be with_suprema antisymmetric transitive RelStr;
let S be non empty join-closed Subset of L;
cluster subrelstr S -> with_suprema;
end;
theorem :: WAYBEL23:27
for L be complete transitive antisymmetric (non empty RelStr)
for S be infs-closed non empty Subset of L
for X be Subset of S holds
"/\"(X,subrelstr S) = "/\"(X,L);
theorem :: WAYBEL23:28
for L be complete transitive antisymmetric (non empty RelStr)
for S be sups-closed non empty Subset of L
for X be Subset of S holds
"\/"(X,subrelstr S) = "\/"(X,L);
theorem :: WAYBEL23:29
for L be Semilattice
for S be meet-closed Subset of L holds
S is filtered;
theorem :: WAYBEL23:30
for L be sup-Semilattice
for S be join-closed Subset of L holds
S is directed;
definition
let L be Semilattice;
cluster meet-closed -> filtered Subset of L;
end;
definition
let L be sup-Semilattice;
cluster join-closed -> directed Subset of L;
end;
theorem :: WAYBEL23:31
for L be Semilattice
for S be upper non empty Subset of L holds
S is Filter of L iff S is meet-closed;
theorem :: WAYBEL23:32
for L be sup-Semilattice
for S be lower non empty Subset of L holds
S is Ideal of L iff S is join-closed;
theorem :: WAYBEL23:33
for L be non empty RelStr
for S1,S2 be join-closed Subset of L holds
S1 /\ S2 is join-closed;
theorem :: WAYBEL23:34
for L be non empty RelStr
for S1,S2 be meet-closed Subset of L holds
S1 /\ S2 is meet-closed;
theorem :: WAYBEL23:35
for L be sup-Semilattice
for x be Element of L holds
downarrow x is join-closed;
theorem :: WAYBEL23:36
for L be Semilattice
for x be Element of L holds
downarrow x is meet-closed;
theorem :: WAYBEL23:37
for L be sup-Semilattice
for x be Element of L holds
uparrow x is join-closed;
theorem :: WAYBEL23:38
for L be Semilattice
for x be Element of L holds
uparrow x is meet-closed;
definition
let L be sup-Semilattice;
let x be Element of L;
cluster downarrow x -> join-closed;
cluster uparrow x -> join-closed;
end;
definition
let L be Semilattice;
let x be Element of L;
cluster downarrow x -> meet-closed;
cluster uparrow x -> meet-closed;
end;
theorem :: WAYBEL23:39
for L be sup-Semilattice
for x be Element of L holds
waybelow x is join-closed;
theorem :: WAYBEL23:40
for L be Semilattice
for x be Element of L holds
waybelow x is meet-closed;
theorem :: WAYBEL23:41
for L be sup-Semilattice
for x be Element of L holds
wayabove x is join-closed;
definition
let L be sup-Semilattice;
let x be Element of L;
cluster waybelow x -> join-closed;
cluster wayabove x -> join-closed;
end;
definition
let L be Semilattice;
let x be Element of L;
cluster waybelow x -> meet-closed;
end;
begin :: About Bases of Continuous Lattices
definition
let T be TopStruct;
func weight T -> Cardinal equals
:: WAYBEL23:def 5
meet {Card B where B is Basis of T : not contradiction};
end;
definition
let T be TopStruct;
attr T is second-countable means
:: WAYBEL23:def 6
weight T c= omega;
end;
definition :: DEFINITION 4.1
let L be continuous sup-Semilattice;
mode CLbasis of L -> Subset of L means
:: WAYBEL23:def 7
it is join-closed &
for x be Element of L holds x = sup (waybelow x /\ it);
end;
definition
let L be non empty RelStr;
let S be Subset of L;
attr S is with_bottom means
:: WAYBEL23:def 8
Bottom L in S;
end;
definition
let L be non empty RelStr;
let S be Subset of L;
attr S is with_top means
:: WAYBEL23:def 9
Top L in S;
end;
definition
let L be non empty RelStr;
cluster with_bottom -> non empty Subset of L;
end;
definition
let L be non empty RelStr;
cluster with_top -> non empty Subset of L;
end;
definition
let L be non empty RelStr;
cluster with_bottom Subset of L;
cluster with_top Subset of L;
end;
definition
let L be continuous sup-Semilattice;
cluster with_bottom CLbasis of L;
cluster with_top CLbasis of L;
end;
theorem :: WAYBEL23:42
for L be lower-bounded antisymmetric non empty RelStr
for S be with_bottom Subset of L holds
subrelstr S is lower-bounded;
definition
let L be lower-bounded antisymmetric non empty RelStr;
let S be with_bottom Subset of L;
cluster subrelstr S -> lower-bounded;
end;
definition
let L be continuous sup-Semilattice;
cluster -> join-closed CLbasis of L;
end;
definition
cluster bounded non trivial (continuous LATTICE);
end;
definition
let L be lower-bounded non trivial (continuous sup-Semilattice);
cluster -> non empty CLbasis of L;
end;
theorem :: WAYBEL23:43
for L be sup-Semilattice holds
the carrier of CompactSublatt L is join-closed Subset of L;
theorem :: WAYBEL23:44 :: Under 4.1 (i)
for L be algebraic lower-bounded LATTICE holds
the carrier of CompactSublatt L is with_bottom CLbasis of L;
theorem :: WAYBEL23:45 :: Under 4.1 (ii)
for L be continuous lower-bounded sup-Semilattice
st the carrier of CompactSublatt L is CLbasis of L holds
L is algebraic;
theorem :: WAYBEL23:46 :: PROPOSITION 4.2. (1) iff (2)
for L be continuous lower-bounded LATTICE
for B be join-closed Subset of L holds
B is CLbasis of L iff
for x,y be Element of L st not y <= x
ex b be Element of L st b in B & not b <= x & b << y;
theorem :: WAYBEL23:47 :: PROPOSITION 4.2. (1) iff (3)
for L be continuous lower-bounded LATTICE
for B be join-closed Subset of L st Bottom L in B holds
B is CLbasis of L iff
for x,y be Element of L st x << y
ex b be Element of L st b in B & x <= b & b << y;
theorem :: WAYBEL23:48 :: PROPOSITION 4.2. (1) iff (4)
for L be continuous lower-bounded LATTICE
for B be join-closed Subset of L st Bottom L in B holds
B is CLbasis of L iff
(the carrier of CompactSublatt L c= B &
for x,y be Element of L st not y <= x
ex b be Element of L st b in B & not b <= x & b <= y);
theorem :: WAYBEL23:49 :: PROPOSITION 4.2. (1) iff (5)
for L be continuous lower-bounded LATTICE
for B be join-closed Subset of L st Bottom L in B holds
B is CLbasis of L iff
for x,y be Element of L st not y <= x
ex b be Element of L st b in B & not b <= x & b <= y;
theorem :: WAYBEL23:50
for L be lower-bounded sup-Semilattice
for S be non empty full SubRelStr of L
st Bottom
L in the carrier of S & the carrier of S is join-closed Subset of L
for x be Element of L holds
waybelow x /\ (the carrier of S) is Ideal of S;
definition
let L be non empty reflexive transitive RelStr;
let S be non empty full SubRelStr of L;
func supMap S -> map of InclPoset(Ids S), L means
:: WAYBEL23:def 10
for I be Ideal of S holds it.I = "\/"(I,L);
end;
definition
let L be non empty reflexive transitive RelStr;
let S be non empty full SubRelStr of L;
func idsMap S -> map of InclPoset(Ids S), InclPoset(Ids L) means
:: WAYBEL23:def 11
for I be Ideal of S
ex J be Subset of L st
I = J & it.I = downarrow J;
end;
definition
let L be reflexive RelStr;
let B be Subset of L;
cluster subrelstr B -> reflexive;
end;
definition
let L be transitive RelStr;
let B be Subset of L;
cluster subrelstr B -> transitive;
end;
definition
let L be antisymmetric RelStr;
let B be Subset of L;
cluster subrelstr B -> antisymmetric;
end;
definition
let L be lower-bounded continuous sup-Semilattice;
let B be with_bottom CLbasis of L;
func baseMap B -> map of L, InclPoset(Ids subrelstr B) means
:: WAYBEL23:def 12
for x be Element of L holds it.x = waybelow x /\ B;
end;
theorem :: WAYBEL23:51
for L be non empty reflexive transitive RelStr
for S be non empty full SubRelStr of L holds
dom supMap S = Ids S & rng supMap S is Subset of L;
theorem :: WAYBEL23:52
for L be non empty reflexive transitive RelStr
for S be non empty full SubRelStr of L
for x be set holds
x in dom supMap S iff x is Ideal of S;
theorem :: WAYBEL23:53
for L be non empty reflexive transitive RelStr
for S be non empty full SubRelStr of L holds
dom idsMap S = Ids S & rng idsMap S is Subset of Ids L;
theorem :: WAYBEL23:54
for L be non empty reflexive transitive RelStr
for S be non empty full SubRelStr of L
for x be set holds
x in dom idsMap S iff x is Ideal of S;
theorem :: WAYBEL23:55
for L be non empty reflexive transitive RelStr
for S be non empty full SubRelStr of L
for x be set holds
x in rng idsMap S implies x is Ideal of L;
theorem :: WAYBEL23:56
for L be lower-bounded continuous sup-Semilattice
for B be with_bottom CLbasis of L holds
dom baseMap B = the carrier of L &
rng baseMap B is Subset of Ids subrelstr B;
theorem :: WAYBEL23:57
for L be lower-bounded continuous sup-Semilattice
for B be with_bottom CLbasis of L
for x be set holds
x in rng baseMap B implies x is Ideal of subrelstr B;
theorem :: WAYBEL23:58
for L be up-complete (non empty Poset)
for S be non empty full SubRelStr of L holds
supMap S is monotone;
theorem :: WAYBEL23:59
for L be non empty reflexive transitive RelStr
for S be non empty full SubRelStr of L holds
idsMap S is monotone;
theorem :: WAYBEL23:60
for L be lower-bounded continuous sup-Semilattice
for B be with_bottom CLbasis of L holds
baseMap B is monotone;
definition
let L be up-complete (non empty Poset);
let S be non empty full SubRelStr of L;
cluster supMap S -> monotone;
end;
definition
let L be non empty reflexive transitive RelStr;
let S be non empty full SubRelStr of L;
cluster idsMap S -> monotone;
end;
definition
let L be lower-bounded continuous sup-Semilattice;
let B be with_bottom CLbasis of L;
cluster baseMap B -> monotone;
end;
theorem :: WAYBEL23:61
for L be lower-bounded (continuous sup-Semilattice)
for B be with_bottom CLbasis of L holds
idsMap (subrelstr B) is sups-preserving;
theorem :: WAYBEL23:62
for L be up-complete (non empty Poset)
for S be non empty full SubRelStr of L holds
supMap S = (SupMap L)*(idsMap S);
theorem :: WAYBEL23:63 :: PROPOSITION 4.3.(i)
for L be lower-bounded continuous sup-Semilattice
for B be with_bottom CLbasis of L holds
[supMap subrelstr B,baseMap B] is Galois;
theorem :: WAYBEL23:64 :: PROPOSITION 4.3.(ii)
for L be lower-bounded continuous sup-Semilattice
for B be with_bottom CLbasis of L holds
supMap subrelstr B is upper_adjoint & baseMap B is lower_adjoint;
theorem :: WAYBEL23:65 :: PROPOSITION 4.3.(iii)
for L be lower-bounded (continuous sup-Semilattice)
for B be with_bottom CLbasis of L holds
rng supMap subrelstr B = the carrier of L;
theorem :: WAYBEL23:66 :: PROPOSITION 4.3.(iv)
for L be lower-bounded (continuous sup-Semilattice)
for B be with_bottom CLbasis of L holds
supMap (subrelstr B) is infs-preserving sups-preserving;
theorem :: WAYBEL23:67
for L be lower-bounded continuous sup-Semilattice
for B be with_bottom CLbasis of L holds
baseMap B is sups-preserving;
definition
let L be lower-bounded continuous sup-Semilattice;
let B be with_bottom CLbasis of L;
cluster supMap subrelstr B -> infs-preserving sups-preserving;
cluster baseMap B -> sups-preserving;
end;
canceled;
theorem :: WAYBEL23:69 :: PROPOSITION 4.3.(vi)
for L be lower-bounded (continuous sup-Semilattice)
for B be with_bottom CLbasis of L holds
the carrier of CompactSublatt InclPoset(Ids subrelstr B) =
{ downarrow b where b is Element of subrelstr B : not contradiction };
theorem :: WAYBEL23:70 :: PROPOSITION 4.3.(vii)
for L be lower-bounded (continuous sup-Semilattice)
for B be with_bottom CLbasis of L holds
CompactSublatt InclPoset(Ids subrelstr B),subrelstr B are_isomorphic;
theorem :: WAYBEL23:71
for L be continuous lower-bounded LATTICE
for B be with_bottom CLbasis of L st
for B1 be with_bottom CLbasis of L holds B c= B1
for J be Element of InclPoset Ids subrelstr B holds
J = waybelow "\/"(J,L) /\ B;
theorem :: WAYBEL23:72 :: PROPOSITION 4.4. (1) iff (2)
for L be continuous lower-bounded LATTICE holds
L is algebraic iff
the carrier of CompactSublatt L is with_bottom CLbasis of L &
for B be with_bottom CLbasis of L holds
the carrier of CompactSublatt L c= B;
theorem :: WAYBEL23:73 :: PROPOSITION 4.4. (1) iff (3)
for L be continuous lower-bounded LATTICE holds
L is algebraic iff
ex B be with_bottom CLbasis of L st
for B1 be with_bottom CLbasis of L holds B c= B1;
Back to top