:: Bases of Continuous Lattices
:: by Robert Milewski
::
:: Received November 28, 1998
:: Copyright (c) 1998-2016 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 XBOOLE_0, ORDERS_2, SUBSET_1, WAYBEL_8, WAYBEL_3, STRUCT_0,
TARSKI, WAYBEL_0, XXREAL_0, RCOMP_1, RELAT_2, YELLOW_1, CARD_FIL,
YELLOW_0, ORDINAL2, LATTICE3, EQREL_1, FINSET_1, CAT_1, REWRITE1,
LATTICES, PRE_TOPC, CARD_1, SETFAM_1, RLVECT_3, ORDINAL1, XXREAL_2,
ZFMISC_1, FUNCT_1, WELLORD2, RELAT_1, SEQM_3, YELLOW_2, WAYBEL_1,
WELLORD1, FUNCT_2, WAYBEL23;
notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, FUNCT_1, RELSET_1, PARTFUN1,
FUNCT_2, DOMAIN_1, ORDERS_1, STRUCT_0, FINSET_1, ORDINAL1, CARD_1,
PRE_TOPC, ORDERS_2, CANTOR_1, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2,
WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL_8;
constructors DOMAIN_1, CANTOR_1, ORDERS_3, WAYBEL_8, RELSET_1, WAYBEL20,
TOPS_2;
registrations RELSET_1, FINSET_1, CARD_1, STRUCT_0, LATTICE3, YELLOW_0,
WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_3, WAYBEL_7, WAYBEL_8, WAYBEL14,
SUBSET_1;
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;
registration
let L be non empty RelStr;
cluster infs-closed -> meet-closed for Subset of L;
cluster sups-closed -> join-closed for Subset of L;
end;
registration
let L be non empty RelStr;
cluster infs-closed sups-closed non empty for 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;
registration
let L be with_infima antisymmetric transitive RelStr;
let S be non empty meet-closed Subset of L;
cluster subrelstr S -> with_infima;
end;
registration
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
;
registration
let L be Semilattice;
cluster meet-closed -> filtered for Subset of L;
end;
registration
let L be sup-Semilattice;
cluster join-closed -> directed for 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;
registration
let L be sup-Semilattice;
let x be Element of L;
cluster downarrow x -> join-closed;
cluster uparrow x -> join-closed;
end;
registration
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;
registration
let L be sup-Semilattice;
let x be Element of L;
cluster waybelow x -> join-closed;
cluster wayabove x -> join-closed;
end;
registration
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 the set of all card B where B is Basis of T ;
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;
registration
let L be non empty RelStr;
cluster with_bottom -> non empty for Subset of L;
end;
registration
let L be non empty RelStr;
cluster with_top -> non empty for Subset of L;
end;
registration
let L be non empty RelStr;
cluster with_bottom for Subset of L;
cluster with_top for Subset of L;
end;
registration
let L be continuous sup-Semilattice;
cluster with_bottom for CLbasis of L;
cluster with_top for 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;
registration
let L be lower-bounded antisymmetric non empty RelStr;
let S be with_bottom Subset of L;
cluster subrelstr S -> lower-bounded;
end;
registration
let L be continuous sup-Semilattice;
cluster -> join-closed for CLbasis of L;
end;
registration
cluster bounded non trivial for continuous LATTICE;
end;
registration
let L be lower-bounded non trivial continuous sup-Semilattice;
cluster -> non empty for 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 -> Function 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 -> Function 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;
registration
let L be reflexive RelStr;
let B be Subset of L;
cluster subrelstr B -> reflexive;
end;
registration
let L be transitive RelStr;
let B be Subset of L;
cluster subrelstr B -> transitive;
end;
registration
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 -> Function 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;
registration
let L be up-complete non empty Poset;
let S be non empty full SubRelStr of L;
cluster supMap S -> monotone;
end;
registration
let L be non empty reflexive transitive RelStr;
let S be non empty full SubRelStr of L;
cluster idsMap S -> monotone;
end;
registration
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;
registration
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;
theorem :: WAYBEL23:68 :: 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) = the set of all downarrow b where b is Element of subrelstr B;
theorem :: WAYBEL23:69 :: 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:70
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:71 :: 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:72 :: 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;
theorem :: WAYBEL23:73 :: WAYBEL31:1, AK, 21.02.2006
for T be TopStruct for b be Basis of T holds weight T c= card b;
theorem :: WAYBEL23:74 :: WAYBEL31:1, AK, 21.02.2006
for T be TopStruct ex b be Basis of T st card b = weight T;