:: Bases of Continuous Lattices
:: by Robert Milewski
::
:: Received November 28, 1998
:: Copyright (c) 1998-2026 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;
requirements SUBSET, BOOLE;
definitions TARSKI, LATTICE3, YELLOW_0, XBOOLE_0;
equalities YELLOW_0, XBOOLE_0, STRUCT_0;
expansions TARSKI, LATTICE3, YELLOW_0, XBOOLE_0;
theorems TARSKI, SETFAM_1, ZFMISC_1, FUNCT_1, FUNCT_2, CANTOR_1, YELLOW_0,
YELLOW_1, YELLOW_2, YELLOW_3, YELLOW_5, YELLOW12, WAYBEL_0, WAYBEL_1,
WAYBEL_3, WAYBEL_7, WAYBEL_8, WAYBEL10, WAYBEL13, WAYBEL20, WAYBEL21,
XBOOLE_0, XBOOLE_1;
schemes ORDINAL1, FUNCT_2, MONOID_1;
begin :: Preliminaries
theorem Th1:
for L be non empty Poset for x be Element of L holds compactbelow
x = waybelow x /\ the carrier of CompactSublatt L
proof
let L be non empty Poset;
let x be Element of L;
A1: compactbelow x c= waybelow x /\ the carrier of CompactSublatt L
proof
let y be object;
assume
A2: y in compactbelow x;
then reconsider y1 = y as Element of L;
A3: y in downarrow x /\ the carrier of CompactSublatt L by A2,WAYBEL_8:5;
then y in downarrow x by XBOOLE_0:def 4;
then
A4: y1 <= x by WAYBEL_0:17;
A5: y in the carrier of CompactSublatt L by A3,XBOOLE_0:def 4;
then y1 is compact by WAYBEL_8:def 1;
then y1 << y1 by WAYBEL_3:def 2;
then y1 << x by A4,WAYBEL_3:2;
then y1 in waybelow x by WAYBEL_3:7;
hence thesis by A5,XBOOLE_0:def 4;
end;
waybelow x /\ the carrier of CompactSublatt L c= compactbelow x
proof
let y be object;
assume
A6: y in waybelow x /\ the carrier of CompactSublatt L;
then reconsider y1 = y as Element of L;
y in waybelow x by A6,XBOOLE_0:def 4;
then y1 << x by WAYBEL_3:7;
then y1 <= x by WAYBEL_3:1;
then
A7: y in downarrow x by WAYBEL_0:17;
y in the carrier of CompactSublatt L by A6,XBOOLE_0:def 4;
then y in downarrow x /\ the carrier of CompactSublatt L by A7,
XBOOLE_0:def 4;
hence thesis by WAYBEL_8:5;
end;
hence thesis by A1;
end;
definition
let L be non empty reflexive transitive RelStr;
let X be Subset of InclPoset Ids L;
redefine func union X -> Subset of L; :: redefines union (TARSKI, definition)
coherence
proof
union X c= the carrier of L
proof
let x be object;
assume x in union X;
then consider Y be set such that
A1: x in Y and
A2: Y in X by TARSKI:def 4;
reconsider Y as Ideal of L by A2,YELLOW_2:41;
x in Y by A1;
hence thesis;
end;
hence thesis;
end;
end;
Lm1: for X be non empty set for Y be Subset of InclPoset X st ex_sup_of Y,
InclPoset X holds union Y c= sup Y
proof
let X be non empty set;
let Y be Subset of InclPoset X;
assume
A1: ex_sup_of Y,InclPoset X;
now
let x be set;
assume
A2: x in Y;
then reconsider x1 = x as Element of InclPoset X;
sup Y is_>=_than Y by A1,YELLOW_0:30;
then sup Y >= x1 by A2;
hence x c= sup Y by YELLOW_1:3;
end;
hence thesis by ZFMISC_1:76;
end;
theorem Th2:
for L be non empty RelStr for X,Y be Subset of L st X c= Y holds
finsups X c= finsups Y
proof
let L be non empty RelStr;
let X,Y be Subset of L;
assume
A1: X c= Y;
let x be object;
assume x in finsups X;
then x in {"\/"(V,L) where V is finite Subset of X: ex_sup_of V,L} by
WAYBEL_0:def 27;
then consider Z be finite Subset of X such that
A2: x = "\/"(Z,L) and
A3: ex_sup_of Z,L;
reconsider Z as finite Subset of Y by A1,XBOOLE_1:1;
ex_sup_of Z,L by A3;
then x in {"\/"(V,L) where V is finite Subset of Y: ex_sup_of V,L} by A2;
hence thesis by WAYBEL_0:def 27;
end;
theorem Th3:
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
proof
let L be non empty transitive RelStr;
let S be sups-inheriting non empty full SubRelStr of L;
let X be Subset of L;
let Y be Subset of S;
assume
A1: X = Y;
let x be object;
assume x in finsups X;
then x in {"\/"(V,L) where V is finite Subset of X: ex_sup_of V,L} by
WAYBEL_0:def 27;
then consider Z be finite Subset of X such that
A2: x = "\/"(Z,L) and
A3: ex_sup_of Z,L;
reconsider Z as finite Subset of Y by A1;
reconsider Z1 = Z as Subset of S by XBOOLE_1:1;
A4: "\/"(Z1,L) in the carrier of S by A3,YELLOW_0:def 19;
then
A5: ex_sup_of Z1,S by A3,YELLOW_0:64;
x = "\/"(Z1,S) by A2,A3,A4,YELLOW_0:64;
then x in {"\/"(V,S) where V is finite Subset of Y: ex_sup_of V,S} by A5;
hence thesis by WAYBEL_0:def 27;
end;
theorem
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
proof
let L be complete transitive antisymmetric non empty RelStr;
let S be sups-inheriting non empty full SubRelStr of L;
let X be Subset of L;
let Y be Subset of S;
assume
A1: X = Y;
hence finsups X c= finsups Y by Th3;
let x be object;
assume x in finsups Y;
then x in {"\/"(V,S) where V is finite Subset of Y: ex_sup_of V,S} by
WAYBEL_0:def 27;
then consider Z be finite Subset of Y such that
A2: x = "\/"(Z,S) and
ex_sup_of Z,S;
reconsider Z as finite Subset of X by A1;
reconsider Z1 = Z as Subset of S by XBOOLE_1:1;
A3: ex_sup_of Z1,L by YELLOW_0:17;
then "\/"(Z1,L) in the carrier of S by YELLOW_0:def 19;
then x = "\/"(Z1,L) by A2,A3,YELLOW_0:64;
then x in {"\/"(V,L) where V is finite Subset of X: ex_sup_of V,L} by A3;
hence thesis by WAYBEL_0:def 27;
end;
theorem Th5:
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
proof
let L be complete sup-Semilattice;
let S be join-inheriting non empty full SubRelStr of L;
assume
A1: Bottom L in the carrier of S;
let X be Subset of L;
let Y be Subset of S;
assume
A2: X = Y;
let x be object;
assume x in finsups Y;
then x in {"\/"(V,S) where V is finite Subset of Y: ex_sup_of V,S} by
WAYBEL_0:def 27;
then consider Z be finite Subset of Y such that
A3: x = "\/"(Z,S) and
A4: ex_sup_of Z,S;
reconsider Z as finite Subset of X by A2;
now
per cases;
suppose
Z is non empty;
then reconsider Z1 = Z as finite non empty Subset of S by XBOOLE_1:1;
reconsider xl = "\/"(Z1,L) as Element of S by WAYBEL21:15;
A5: ex_sup_of Z1,L by YELLOW_0:17;
A6: now
let b be Element of S;
reconsider b1 = b as Element of L by YELLOW_0:58;
assume
A7: b is_>=_than Z1;
b1 is_>=_than Z1
by A7,YELLOW_0:59;
then "\/"(Z1, L) <= b1 by A5,YELLOW_0:30;
hence xl <= b by YELLOW_0:60;
end;
A8: "\/"(Z1, L) is_>=_than Z1 by A5,YELLOW_0:30;
xl is_>=_than Z1
proof
let b be Element of S;
reconsider b1 = b as Element of L by YELLOW_0:58;
assume b in Z1;
then b1 <= "\/"(Z1, L) by A8;
hence b <= xl by YELLOW_0:60;
end;
then "\/"(Z1,S) = "\/"(Z1,L) by A6,YELLOW_0:30;
then x in { "\/"(V,L) where V is finite Subset of X: ex_sup_of V,L } by
A3,A5;
hence thesis by WAYBEL_0:def 27;
end;
suppose
A9: Z is empty;
reconsider dL = Bottom L as Element of S by A1;
reconsider dS = Bottom S as Element of L by YELLOW_0:58;
S is lower-bounded by A4,A9,WAYBEL20:6;
then Bottom S <= dL by YELLOW_0:44;
then
A10: dS <= Bottom L by YELLOW_0:59;
A11: ex_sup_of Z,L by YELLOW_0:17;
Bottom L <= dS by YELLOW_0:44;
then dS = Bottom L by A10,YELLOW_0:def 3;
then x in { "\/"(V,L) where V is finite Subset of X: ex_sup_of V,L } by
A3,A9,A11;
hence thesis by WAYBEL_0:def 27;
end;
end;
hence thesis;
end;
theorem Th6:
for L be lower-bounded sup-Semilattice for X be Subset of
InclPoset Ids L holds sup X = downarrow finsups union X
proof
let L be lower-bounded sup-Semilattice;
let X be Subset of InclPoset Ids L;
reconsider a = downarrow finsups union X as Element of InclPoset Ids L by
YELLOW_2:41;
A1: union X c= sup X by Lm1,YELLOW_0:17;
A2: now
let b be Element of InclPoset Ids L;
reconsider b1 = b as Ideal of L by YELLOW_2:41;
assume b is_>=_than X;
then b >= sup X by YELLOW_0:32;
then sup X c= b1 by YELLOW_1:3;
then union X c= b1 by A1;
then downarrow finsups union X c= b1 by WAYBEL_0:61;
hence a <= b by YELLOW_1:3;
end;
A3: union X c= downarrow finsups union X by WAYBEL_0:61;
now
let b be Element of InclPoset Ids L;
assume b in X;
then b c= union X by ZFMISC_1:74;
then b c= downarrow finsups union X by A3;
hence b <= a by YELLOW_1:3;
end;
then a is_>=_than X;
hence thesis by A2,YELLOW_0:32;
end;
theorem Th7:
for L be reflexive transitive RelStr for X be Subset of L holds
downarrow downarrow X = downarrow X
proof
let L be reflexive transitive RelStr;
let X be Subset of L;
A1: downarrow downarrow X c= downarrow X
proof
let x be object;
assume
A2: x in downarrow downarrow X;
then reconsider x1 = x as Element of L;
consider y be Element of L such that
A3: y >= x1 and
A4: y in downarrow X by A2,WAYBEL_0:def 15;
consider z be Element of L such that
A5: z >= y and
A6: z in X by A4,WAYBEL_0:def 15;
z >= x1 by A3,A5,YELLOW_0:def 2;
hence thesis by A6,WAYBEL_0:def 15;
end;
downarrow X c= downarrow downarrow X by WAYBEL_0:16;
hence thesis by A1;
end;
theorem
for L be reflexive transitive RelStr for X be Subset of L holds
uparrow uparrow X = uparrow X
proof
let L be reflexive transitive RelStr;
let X be Subset of L;
A1: uparrow uparrow X c= uparrow X
proof
let x be object;
assume
A2: x in uparrow uparrow X;
then reconsider x1 = x as Element of L;
consider y be Element of L such that
A3: y <= x1 and
A4: y in uparrow X by A2,WAYBEL_0:def 16;
consider z be Element of L such that
A5: z <= y and
A6: z in X by A4,WAYBEL_0:def 16;
z <= x1 by A3,A5,YELLOW_0:def 2;
hence thesis by A6,WAYBEL_0:def 16;
end;
uparrow X c= uparrow uparrow X by WAYBEL_0:16;
hence thesis by A1;
end;
theorem
for L be non empty reflexive transitive RelStr for x be Element of L
holds downarrow downarrow x = downarrow x
proof
let L be non empty reflexive transitive RelStr;
let x be Element of L;
A1: downarrow downarrow x c= downarrow x
proof
let v be object;
assume
A2: v in downarrow downarrow x;
then reconsider v1 = v as Element of L;
consider y be Element of L such that
A3: y >= v1 and
A4: y in downarrow x by A2,WAYBEL_0:def 15;
x >= y by A4,WAYBEL_0:17;
then x >= v1 by A3,YELLOW_0:def 2;
hence thesis by WAYBEL_0:17;
end;
downarrow x c= downarrow downarrow x by WAYBEL_0:16;
hence thesis by A1;
end;
theorem
for L be non empty reflexive transitive RelStr for x be Element of L
holds uparrow uparrow x = uparrow x
proof
let L be non empty reflexive transitive RelStr;
let x be Element of L;
A1: uparrow uparrow x c= uparrow x
proof
let v be object;
assume
A2: v in uparrow uparrow x;
then reconsider v1 = v as Element of L;
consider y be Element of L such that
A3: y <= v1 and
A4: y in uparrow x by A2,WAYBEL_0:def 16;
x <= y by A4,WAYBEL_0:18;
then x <= v1 by A3,YELLOW_0:def 2;
hence thesis by WAYBEL_0:18;
end;
uparrow x c= uparrow uparrow x by WAYBEL_0:16;
hence thesis by A1;
end;
theorem Th11:
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
proof
let L be non empty RelStr;
let S be non empty SubRelStr of L;
let X be Subset of L;
let Y be Subset of S;
assume
A1: X = Y;
let x be object;
assume
A2: x in downarrow Y;
then reconsider x1 = x as Element of S;
consider y1 be Element of S such that
A3: y1 >= x1 and
A4: y1 in Y by A2,WAYBEL_0:def 15;
reconsider x2 = x1, y2 = y1 as Element of L by YELLOW_0:58;
y2 >= x2 by A3,YELLOW_0:59;
hence thesis by A1,A4,WAYBEL_0:def 15;
end;
theorem Th12:
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
proof
let L be non empty RelStr;
let S be non empty SubRelStr of L;
let X be Subset of L;
let Y be Subset of S;
assume
A1: X = Y;
let x be object;
assume
A2: x in uparrow Y;
then reconsider x1 = x as Element of S;
consider y1 be Element of S such that
A3: y1 <= x1 and
A4: y1 in Y by A2,WAYBEL_0:def 16;
reconsider x2 = x1, y2 = y1 as Element of L by YELLOW_0:58;
y2 <= x2 by A3,YELLOW_0:59;
hence thesis by A1,A4,WAYBEL_0:def 16;
end;
theorem
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
proof
let L be non empty RelStr;
let S be non empty SubRelStr of L;
let x be Element of L;
let y be Element of S;
A1: downarrow x = downarrow {x} by WAYBEL_0:def 17;
A2: downarrow y = downarrow {y} by WAYBEL_0:def 17;
assume x = y;
hence thesis by A1,A2,Th11;
end;
theorem
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
proof
let L be non empty RelStr;
let S be non empty SubRelStr of L;
let x be Element of L;
let y be Element of S;
A1: uparrow x = uparrow {x} by WAYBEL_0:def 18;
A2: uparrow y = uparrow {y} by WAYBEL_0:def 18;
assume x = y;
hence thesis by A1,A2,Th12;
end;
begin :: Relational Subsets
definition
let L be non empty RelStr;
let S be Subset of L;
attr S is meet-closed means
:Def1:
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
:Def2:
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
:Def3:
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
:Def4:
subrelstr S is sups-inheriting;
end;
registration
let L be non empty RelStr;
cluster infs-closed -> meet-closed for Subset of L;
coherence;
cluster sups-closed -> join-closed for Subset of L;
coherence;
end;
registration
let L be non empty RelStr;
cluster infs-closed sups-closed non empty for Subset of L;
existence
proof
the carrier of L c= the carrier of L;
then reconsider S = the carrier of L as Subset of L;
take S;
the carrier of subrelstr S = S by YELLOW_0:def 15;
then
for X be Subset of subrelstr S st ex_inf_of X,L holds "/\"(X,L) in the
carrier of subrelstr S;
hence subrelstr S is infs-inheriting;
the carrier of subrelstr S = S by YELLOW_0:def 15;
then
for X be Subset of subrelstr S st ex_sup_of X,L holds "\/"(X,L) in the
carrier of subrelstr S;
hence subrelstr S is sups-inheriting;
thus thesis;
end;
end;
theorem Th15:
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
proof
let L be non empty RelStr;
let S be Subset of L;
thus S is meet-closed implies 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
proof
assume S is meet-closed;
then
A1: subrelstr S is meet-inheriting;
let x,y be Element of L;
assume that
A2: x in S and
A3: y in S and
A4: ex_inf_of {x,y},L;
the carrier of subrelstr S = S by YELLOW_0:def 15;
hence thesis by A1,A2,A3,A4;
end;
assume
A5: 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;
now
let x,y be Element of L;
assume that
A6: x in the carrier of subrelstr S and
A7: y in the carrier of subrelstr S and
A8: ex_inf_of {x,y},L;
the carrier of subrelstr S = S by YELLOW_0:def 15;
hence inf {x,y} in the carrier of subrelstr S by A5,A6,A7,A8;
end;
then subrelstr S is meet-inheriting;
hence thesis;
end;
theorem Th16:
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
proof
let L be non empty RelStr;
let S be Subset of L;
thus S is join-closed implies 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
proof
assume S is join-closed;
then
A1: subrelstr S is join-inheriting;
let x,y be Element of L;
assume that
A2: x in S and
A3: y in S and
A4: ex_sup_of {x,y},L;
the carrier of subrelstr S = S by YELLOW_0:def 15;
hence thesis by A1,A2,A3,A4;
end;
assume
A5: 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;
now
let x,y be Element of L;
assume that
A6: x in the carrier of subrelstr S and
A7: y in the carrier of subrelstr S and
A8: ex_sup_of {x,y},L;
the carrier of subrelstr S = S by YELLOW_0:def 15;
hence sup {x,y} in the carrier of subrelstr S by A5,A6,A7,A8;
end;
then subrelstr S is join-inheriting;
hence thesis;
end;
theorem
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
proof
let L be antisymmetric with_infima RelStr;
let S be Subset of L;
thus S is meet-closed implies for x,y be Element of L st x in S & y in S
holds inf {x,y} in S
by YELLOW_0:21,Th15;
assume for x,y be Element of L st x in S & y in S holds inf {x,y} in S;
then
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;
hence thesis by Th15;
end;
theorem Th18:
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
proof
let L be antisymmetric with_suprema RelStr;
let S be Subset of L;
thus S is join-closed implies for x,y be Element of L st x in S & y in S
holds sup {x,y} in S
by YELLOW_0:20,Th16;
assume for x,y be Element of L st x in S & y in S holds sup {x,y} in S;
then
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;
hence thesis by Th16;
end;
theorem
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
proof
let L be non empty RelStr;
let S be Subset of L;
thus S is infs-closed implies for X be Subset of S st ex_inf_of X,L holds
"/\"(X,L) in S
proof
assume S is infs-closed;
then
A1: subrelstr S is infs-inheriting;
let X be Subset of S;
assume
A2: ex_inf_of X,L;
X is Subset of subrelstr S by YELLOW_0:def 15;
then "/\"(X,L) in the carrier of subrelstr S by A1,A2;
hence thesis by YELLOW_0:def 15;
end;
assume
A3: for X be Subset of S st ex_inf_of X,L holds "/\"(X,L) in S;
now
let X be Subset of subrelstr S;
assume
A4: ex_inf_of X,L;
X is Subset of S by YELLOW_0:def 15;
then "/\"(X,L) in S by A3,A4;
hence "/\"(X,L) in the carrier of subrelstr S by YELLOW_0:def 15;
end;
then subrelstr S is infs-inheriting;
hence thesis;
end;
theorem
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
proof
let L be non empty RelStr;
let S be Subset of L;
thus S is sups-closed implies for X be Subset of S st ex_sup_of X,L holds
"\/"(X,L) in S
proof
assume S is sups-closed;
then
A1: subrelstr S is sups-inheriting;
let X be Subset of S;
assume
A2: ex_sup_of X,L;
X is Subset of subrelstr S by YELLOW_0:def 15;
then "\/"(X,L) in the carrier of subrelstr S by A1,A2;
hence thesis by YELLOW_0:def 15;
end;
assume
A3: for X be Subset of S st ex_sup_of X,L holds "\/"(X,L) in S;
now
let X be Subset of subrelstr S;
assume
A4: ex_sup_of X,L;
X is Subset of S by YELLOW_0:def 15;
then "\/"(X,L) in S by A3,A4;
hence "\/"(X,L) in the carrier of subrelstr S by YELLOW_0:def 15;
end;
then subrelstr S is sups-inheriting;
hence thesis;
end;
theorem Th21:
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)
proof
let L be non empty transitive RelStr;
let S be infs-closed non empty Subset of L;
let X be Subset of S;
A1: X is Subset of subrelstr S by YELLOW_0:def 15;
assume
A2: ex_inf_of X,L;
subrelstr S is infs-inheriting non empty full SubRelStr of L by Def3;
then "/\"(X,L) in the carrier of subrelstr S by A1,A2,YELLOW_0:def 18;
hence thesis by A1,A2,YELLOW_0:63;
end;
theorem Th22:
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)
proof
let L be non empty transitive RelStr;
let S be sups-closed non empty Subset of L;
let X be Subset of S;
A1: X is Subset of subrelstr S by YELLOW_0:def 15;
assume
A2: ex_sup_of X,L;
subrelstr S is sups-inheriting non empty full SubRelStr of L by Def4;
then "\/"(X,L) in the carrier of subrelstr S by A1,A2,YELLOW_0:def 19;
hence thesis by A1,A2,YELLOW_0:64;
end;
theorem
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)
proof
let L be non empty transitive RelStr;
let S be meet-closed non empty Subset of L;
let x,y be Element of S;
A1: x is Element of subrelstr S by YELLOW_0:def 15;
A2: y is Element of subrelstr S by YELLOW_0:def 15;
assume
A3: ex_inf_of {x,y},L;
subrelstr S is meet-inheriting non empty full SubRelStr of L by Def1;
then "/\"({x,y},L) in the carrier of subrelstr S by A1,A2,A3,YELLOW_0:def 16;
hence thesis by A1,A2,A3,YELLOW_0:65;
end;
theorem
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)
proof
let L be non empty transitive RelStr;
let S be join-closed non empty Subset of L;
let x,y be Element of S;
A1: x is Element of subrelstr S by YELLOW_0:def 15;
A2: y is Element of subrelstr S by YELLOW_0:def 15;
assume
A3: ex_sup_of {x,y},L;
subrelstr S is join-inheriting non empty full SubRelStr of L by Def2;
then "\/"({x,y},L) in the carrier of subrelstr S by A1,A2,A3,YELLOW_0:def 17;
hence thesis by A1,A2,A3,YELLOW_0:66;
end;
theorem Th25:
for L be with_infima antisymmetric transitive RelStr for S be
non empty meet-closed Subset of L holds subrelstr S is with_infima
proof
let L be with_infima antisymmetric transitive RelStr;
let S be non empty meet-closed Subset of L;
subrelstr S is non empty meet-inheriting full SubRelStr of L by Def1;
hence thesis;
end;
theorem Th26:
for L be with_suprema antisymmetric transitive RelStr for S be
non empty join-closed Subset of L holds subrelstr S is with_suprema
proof
let L be with_suprema antisymmetric transitive RelStr;
let S be non empty join-closed Subset of L;
subrelstr S is non empty join-inheriting full SubRelStr of L by Def2;
hence thesis;
end;
registration
let L be with_infima antisymmetric transitive RelStr;
let S be non empty meet-closed Subset of L;
cluster subrelstr S -> with_infima;
coherence by Th25;
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;
coherence by Th26;
end;
theorem
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)
proof
let L be complete transitive antisymmetric non empty RelStr;
let S be infs-closed non empty Subset of L;
let X be Subset of S;
ex_inf_of X,L by YELLOW_0:17;
hence thesis by Th21;
end;
theorem
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)
proof
let L be complete transitive antisymmetric non empty RelStr;
let S be sups-closed non empty Subset of L;
let X be Subset of S;
ex_sup_of X,L by YELLOW_0:17;
hence thesis by Th22;
end;
theorem Th29:
for L be Semilattice for S be meet-closed Subset of L holds S is filtered
proof
let L be Semilattice;
let S be meet-closed Subset of L;
subrelstr S is meet-inheriting by Def1;
hence thesis by YELLOW12:26;
end;
theorem Th30:
for L be sup-Semilattice for S be join-closed Subset of L holds S is directed
proof
let L be sup-Semilattice;
let S be join-closed Subset of L;
subrelstr S is join-inheriting by Def2;
hence thesis by YELLOW12:27;
end;
registration
let L be Semilattice;
cluster meet-closed -> filtered for Subset of L;
coherence by Th29;
end;
registration
let L be sup-Semilattice;
cluster join-closed -> directed for Subset of L;
coherence by Th30;
end;
theorem
for L be Semilattice for S be upper non empty Subset of L holds S is
Filter of L iff S is meet-closed
by WAYBEL_0:63;
theorem
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
by WAYBEL_0:64;
theorem Th33:
for L be non empty RelStr for S1,S2 be join-closed Subset of L
holds S1 /\ S2 is join-closed
proof
let L be non empty RelStr;
let S1,S2 be join-closed Subset of L;
A1: subrelstr S2 is join-inheriting by Def2;
A2: subrelstr S1 is join-inheriting by Def2;
now
let x,y be Element of L;
assume that
A3: x in the carrier of subrelstr (S1 /\ S2) and
A4: y in the carrier of subrelstr (S1 /\ S2) and
A5: ex_sup_of {x,y},L;
A6: y in S1 /\ S2 by A4,YELLOW_0:def 15;
then y in S2 by XBOOLE_0:def 4;
then
A7: y in the carrier of subrelstr S2 by YELLOW_0:def 15;
A8: x in S1 /\ S2 by A3,YELLOW_0:def 15;
then x in S2 by XBOOLE_0:def 4;
then x in the carrier of subrelstr S2 by YELLOW_0:def 15;
then sup {x,y} in the carrier of subrelstr S2 by A1,A5,A7;
then
A9: sup {x,y} in S2 by YELLOW_0:def 15;
y in S1 by A6,XBOOLE_0:def 4;
then
A10: y in the carrier of subrelstr S1 by YELLOW_0:def 15;
x in S1 by A8,XBOOLE_0:def 4;
then x in the carrier of subrelstr S1 by YELLOW_0:def 15;
then sup {x,y} in the carrier of subrelstr S1 by A2,A5,A10;
then sup {x,y} in S1 by YELLOW_0:def 15;
then sup {x,y} in S1 /\ S2 by A9,XBOOLE_0:def 4;
hence sup {x,y} in the carrier of subrelstr (S1 /\ S2) by YELLOW_0:def 15;
end;
then subrelstr (S1 /\ S2) is join-inheriting;
hence thesis;
end;
theorem
for L be non empty RelStr for S1,S2 be meet-closed Subset of L holds
S1 /\ S2 is meet-closed
proof
let L be non empty RelStr;
let S1,S2 be meet-closed Subset of L;
A1: subrelstr S2 is meet-inheriting by Def1;
A2: subrelstr S1 is meet-inheriting by Def1;
now
let x,y be Element of L;
assume that
A3: x in the carrier of subrelstr (S1 /\ S2) and
A4: y in the carrier of subrelstr (S1 /\ S2) and
A5: ex_inf_of {x,y},L;
A6: y in S1 /\ S2 by A4,YELLOW_0:def 15;
then y in S2 by XBOOLE_0:def 4;
then
A7: y in the carrier of subrelstr S2 by YELLOW_0:def 15;
A8: x in S1 /\ S2 by A3,YELLOW_0:def 15;
then x in S2 by XBOOLE_0:def 4;
then x in the carrier of subrelstr S2 by YELLOW_0:def 15;
then inf {x,y} in the carrier of subrelstr S2 by A1,A5,A7;
then
A9: inf {x,y} in S2 by YELLOW_0:def 15;
y in S1 by A6,XBOOLE_0:def 4;
then
A10: y in the carrier of subrelstr S1 by YELLOW_0:def 15;
x in S1 by A8,XBOOLE_0:def 4;
then x in the carrier of subrelstr S1 by YELLOW_0:def 15;
then inf {x,y} in the carrier of subrelstr S1 by A2,A5,A10;
then inf {x,y} in S1 by YELLOW_0:def 15;
then inf {x,y} in S1 /\ S2 by A9,XBOOLE_0:def 4;
hence inf {x,y} in the carrier of subrelstr (S1 /\ S2) by YELLOW_0:def 15;
end;
then subrelstr (S1 /\ S2) is meet-inheriting;
hence thesis;
end;
theorem Th35:
for L be sup-Semilattice for x be Element of L holds downarrow x
is join-closed
proof
let L be sup-Semilattice;
let x be Element of L;
reconsider x1 = x as Element of L;
now
let y,z be Element of L;
assume that
A1: y in the carrier of subrelstr downarrow x and
A2: z in the carrier of subrelstr downarrow x and
ex_sup_of {y,z},L;
z in downarrow x by A2,YELLOW_0:def 15;
then
A3: z <= x1 by WAYBEL_0:17;
y in downarrow x by A1,YELLOW_0:def 15;
then y <= x1 by WAYBEL_0:17;
then y"\/"z <= x1 by A3,YELLOW_5:9;
then y"\/"z in downarrow x by WAYBEL_0:17;
then sup {y,z} in downarrow x by YELLOW_0:41;
hence sup {y,z} in the carrier of subrelstr downarrow x by YELLOW_0:def 15;
end;
then subrelstr downarrow x is join-inheriting;
hence thesis;
end;
theorem Th36:
for L be Semilattice for x be Element of L holds downarrow x is meet-closed
proof
let L be Semilattice;
let x be Element of L;
reconsider x1 = x as Element of L;
now
let y,z be Element of L;
assume that
A1: y in the carrier of subrelstr downarrow x and
z in the carrier of subrelstr downarrow x and
ex_inf_of {y,z},L;
y in downarrow x by A1,YELLOW_0:def 15;
then
A2: y <= x1 by WAYBEL_0:17;
y"/\"z <= y by YELLOW_0:23;
then y"/\"z <= x1 by A2,YELLOW_0:def 2;
then y"/\"z in downarrow x by WAYBEL_0:17;
then inf {y,z} in downarrow x by YELLOW_0:40;
hence inf {y,z} in the carrier of subrelstr downarrow x by YELLOW_0:def 15;
end;
then subrelstr downarrow x is meet-inheriting;
hence thesis;
end;
theorem Th37:
for L be sup-Semilattice for x be Element of L holds uparrow x is join-closed
proof
let L be sup-Semilattice;
let x be Element of L;
reconsider x1 = x as Element of L;
now
let y,z be Element of L;
assume that
A1: y in the carrier of subrelstr uparrow x and
z in the carrier of subrelstr uparrow x and
ex_sup_of {y,z},L;
y in uparrow x by A1,YELLOW_0:def 15;
then
A2: y >= x1 by WAYBEL_0:18;
y"\/"z >= y by YELLOW_0:22;
then y"\/"z >= x1 by A2,YELLOW_0:def 2;
then y"\/"z in uparrow x by WAYBEL_0:18;
then sup {y,z} in uparrow x by YELLOW_0:41;
hence sup {y,z} in the carrier of subrelstr uparrow x by YELLOW_0:def 15;
end;
then subrelstr uparrow x is join-inheriting;
hence thesis;
end;
theorem Th38:
for L be Semilattice for x be Element of L holds uparrow x is meet-closed
proof
let L be Semilattice;
let x be Element of L;
reconsider x1 = x as Element of L;
now
let y,z be Element of L;
assume that
A1: y in the carrier of subrelstr uparrow x and
A2: z in the carrier of subrelstr uparrow x and
ex_inf_of {y,z},L;
z in uparrow x by A2,YELLOW_0:def 15;
then
A3: z >= x1 by WAYBEL_0:18;
y in uparrow x by A1,YELLOW_0:def 15;
then y >= x1 by WAYBEL_0:18;
then y"/\"z >= x1"/\"x1 by A3,YELLOW_3:2;
then y"/\"z >= x1 by YELLOW_5:2;
then y"/\"z in uparrow x by WAYBEL_0:18;
then inf {y,z} in uparrow x by YELLOW_0:40;
hence inf {y,z} in the carrier of subrelstr uparrow x by YELLOW_0:def 15;
end;
then subrelstr uparrow x is meet-inheriting;
hence thesis;
end;
registration
let L be sup-Semilattice;
let x be Element of L;
cluster downarrow x -> join-closed;
coherence by Th35;
cluster uparrow x -> join-closed;
coherence by Th37;
end;
registration
let L be Semilattice;
let x be Element of L;
cluster downarrow x -> meet-closed;
coherence by Th36;
cluster uparrow x -> meet-closed;
coherence by Th38;
end;
theorem Th39:
for L be sup-Semilattice for x be Element of L holds waybelow x
is join-closed
proof
let L be sup-Semilattice;
let x be Element of L;
now
let y,z be Element of L;
assume that
A1: y in the carrier of subrelstr waybelow x and
A2: z in the carrier of subrelstr waybelow x and
ex_sup_of {y,z},L;
z in waybelow x by A2,YELLOW_0:def 15;
then
A3: z << x by WAYBEL_3:7;
y in waybelow x by A1,YELLOW_0:def 15;
then y << x by WAYBEL_3:7;
then y"\/"z << x by A3,WAYBEL_3:3;
then y"\/"z in waybelow x by WAYBEL_3:7;
then sup {y,z} in waybelow x by YELLOW_0:41;
hence sup {y,z} in the carrier of subrelstr waybelow x by YELLOW_0:def 15;
end;
then subrelstr waybelow x is join-inheriting;
hence thesis;
end;
theorem Th40:
for L be Semilattice for x be Element of L holds waybelow x is meet-closed
proof
let L be Semilattice;
let x be Element of L;
now
let y,z be Element of L;
assume that
A1: y in the carrier of subrelstr waybelow x and
z in the carrier of subrelstr waybelow x and
ex_inf_of {y,z},L;
y in waybelow x by A1,YELLOW_0:def 15;
then
A2: y << x by WAYBEL_3:7;
y"/\"z <= y by YELLOW_0:23;
then y"/\"z << x by A2,WAYBEL_3:2;
then y"/\"z in waybelow x by WAYBEL_3:7;
then inf {y,z} in waybelow x by YELLOW_0:40;
hence inf {y,z} in the carrier of subrelstr waybelow x by YELLOW_0:def 15;
end;
then subrelstr waybelow x is meet-inheriting;
hence thesis;
end;
theorem Th41:
for L be sup-Semilattice for x be Element of L holds wayabove x
is join-closed
proof
let L be sup-Semilattice;
let x be Element of L;
now
let y,z be Element of L;
assume that
A1: y in the carrier of subrelstr wayabove x and
z in the carrier of subrelstr wayabove x and
ex_sup_of {y,z},L;
y in wayabove x by A1,YELLOW_0:def 15;
then
A2: y >> x by WAYBEL_3:8;
y"\/"z >= y by YELLOW_0:22;
then y"\/"z >> x by A2,WAYBEL_3:2;
then y"\/"z in wayabove x by WAYBEL_3:8;
then sup {y,z} in wayabove x by YELLOW_0:41;
hence sup {y,z} in the carrier of subrelstr wayabove x by YELLOW_0:def 15;
end;
then subrelstr wayabove x is join-inheriting;
hence thesis;
end;
registration
let L be sup-Semilattice;
let x be Element of L;
cluster waybelow x -> join-closed;
coherence by Th39;
cluster wayabove x -> join-closed;
coherence by Th41;
end;
registration
let L be Semilattice;
let x be Element of L;
cluster waybelow x -> meet-closed;
coherence by Th40;
end;
begin :: About Bases of Continuous Lattices
definition
let T be TopStruct;
func weight T -> Cardinal equals
meet the set of all card B where B is Basis of T ;
coherence
proof
set X = the set of all card B1 where B1 is Basis of T ;
defpred P[Ordinal] means $1 in the set of all card B where B is Basis of T;
A1: ex A be Ordinal st P[A]
proof
take card the topology of T;
the topology of T is Basis of T by CANTOR_1:2;
hence thesis;
end;
consider A be Ordinal such that
A2: P[A] and
A3: for C be Ordinal st P[C] holds A c= C from ORDINAL1:sch 1(A1);
ex B be Basis of T st A = card B by A2;
then reconsider A as Cardinal;
A4: now
let x be object;
thus (for y be set holds y in X implies x in y) implies x in A by A2;
assume
A5: x in A;
let y be set;
assume
A6: y in X;
then ex B1 be Basis of T st y = card B1;
then reconsider y1 = y as Cardinal;
A c= y1 by A3,A6;
hence x in y by A5;
end;
the topology of T is Basis of T by CANTOR_1:2;
then card the topology of T in X;
hence thesis by A4,SETFAM_1:def 1;
end;
end;
definition
let T be TopStruct;
attr T is second-countable means
weight T c= omega;
end;
definition :: DEFINITION 4.1
let L be continuous sup-Semilattice;
mode CLbasis of L -> Subset of L means
:Def7:
it is join-closed & for x be Element of L holds x = sup (waybelow x /\ it);
existence
proof
take S = [#]L;
subrelstr S is join-inheriting by WAYBEL_0:64;
hence S is join-closed;
let x be Element of L;
thus x = sup waybelow x by WAYBEL_3:def 5
.= sup (waybelow x /\ S) by XBOOLE_1:28;
end;
end;
definition
let L be non empty RelStr;
let S be Subset of L;
attr S is with_bottom means
:Def8:
Bottom L in S;
end;
definition
let L be non empty RelStr;
let S be Subset of L;
attr S is with_top means
Top L in S;
end;
registration
let L be non empty RelStr;
cluster with_bottom -> non empty for Subset of L;
coherence;
end;
registration
let L be non empty RelStr;
cluster with_top -> non empty for Subset of L;
coherence;
end;
registration
let L be non empty RelStr;
cluster with_bottom for Subset of L;
existence
proof
take [#]L;
thus Bottom L in [#]L;
end;
cluster with_top for Subset of L;
existence
proof
take [#]L;
thus Top L in [#]L;
end;
end;
registration
let L be continuous sup-Semilattice;
cluster with_bottom for CLbasis of L;
existence
proof
A1: now
let x be Element of L;
waybelow x /\ [#]L = waybelow x by XBOOLE_1:28;
hence x = sup (waybelow x /\ [#]L) by WAYBEL_3:def 5;
end;
for x,y be Element of L st x in [#]L & y in [#]L holds sup {x,y} in [#]L;
then [#]L is join-closed by Th18;
then reconsider S = [#]L as CLbasis of L by A1,Def7;
take S;
thus thesis;
end;
cluster with_top for CLbasis of L;
existence
proof
A2: now
let x be Element of L;
waybelow x /\ [#]L = waybelow x by XBOOLE_1:28;
hence x = sup (waybelow x /\ [#]L) by WAYBEL_3:def 5;
end;
for x,y be Element of L st x in [#]L & y in [#]L holds sup {x,y} in [#]L;
then [#]L is join-closed by Th18;
then reconsider S = [#]L as CLbasis of L by A2,Def7;
take S;
thus thesis;
end;
end;
theorem Th42:
for L be lower-bounded antisymmetric non empty RelStr for S be
with_bottom Subset of L holds subrelstr S is lower-bounded
proof
let L be lower-bounded antisymmetric non empty RelStr;
let S be with_bottom Subset of L;
Bottom L in S by Def8;
then reconsider dL = Bottom L as Element of subrelstr S by YELLOW_0:def 15;
take dL;
now
let x be Element of subrelstr S;
assume x in the carrier of subrelstr S;
reconsider x1 = x as Element of L by YELLOW_0:58;
Bottom L <= x1 by YELLOW_0:44;
hence dL <= x by YELLOW_0:60;
end;
hence thesis;
end;
registration
let L be lower-bounded antisymmetric non empty RelStr;
let S be with_bottom Subset of L;
cluster subrelstr S -> lower-bounded;
coherence by Th42;
end;
registration
let L be continuous sup-Semilattice;
cluster -> join-closed for CLbasis of L;
coherence by Def7;
end;
registration
cluster bounded non trivial for continuous LATTICE;
existence
proof
set X = the non empty set;
take BoolePoset X;
thus thesis;
end;
end;
registration
let L be lower-bounded non trivial continuous sup-Semilattice;
cluster -> non empty for CLbasis of L;
coherence
proof
let B be CLbasis of L;
assume
A1: B is empty;
Top L = "\/"(waybelow Top L /\ B,L) by Def7
.= Bottom L by A1;
hence contradiction by WAYBEL_7:3;
end;
end;
theorem Th43:
for L be sup-Semilattice holds the carrier of CompactSublatt L
is join-closed Subset of L
proof
let L be sup-Semilattice;
reconsider C = the carrier of CompactSublatt L as Subset of L by
YELLOW_0:def 13;
subrelstr C = CompactSublatt L by YELLOW_0:def 15;
hence thesis by Def2;
end;
theorem Th44: :: Under 4.1 (i)
for L be algebraic lower-bounded LATTICE holds the carrier of
CompactSublatt L is with_bottom CLbasis of L
proof
let L be algebraic lower-bounded LATTICE;
reconsider C = the carrier of CompactSublatt L as join-closed Subset of L by
Th43;
now
let x be Element of L;
x = sup compactbelow x by WAYBEL_8:def 3;
hence x = sup (waybelow x /\ C) by Th1;
end;
then reconsider C as CLbasis of L by Def7;
Bottom L in C by WAYBEL_8:3;
hence thesis by Def8;
end;
theorem :: 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
proof
let L be continuous lower-bounded sup-Semilattice;
reconsider C = the carrier of CompactSublatt L as Subset of L by Th43;
assume
A1: the carrier of CompactSublatt L is CLbasis of L;
now
let x be Element of L;
x = sup (waybelow x /\ C) by A1,Def7;
hence x = sup compactbelow x by Th1;
end;
then
A2: L is satisfying_axiom_K by WAYBEL_8:def 3;
for x being Element of L holds compactbelow x is non empty directed;
hence thesis by A2,WAYBEL_8:def 4;
end;
theorem Th46: :: 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
proof
let L be continuous lower-bounded LATTICE;
let B be join-closed Subset of L;
thus B is CLbasis of L implies 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
proof
assume
A1: B is CLbasis of L;
let x,y be Element of L such that
A2: not y <= x;
thus ex b be Element of L st b in B & not b <= x & b << y
proof
assume
A3: for b1 be Element of L holds not b1 in B or b1 <= x or not b1 << y;
A4: waybelow y /\ B c= downarrow x
proof
let z be object;
assume
A5: z in waybelow y /\ B;
then reconsider z1 = z as Element of L;
z in waybelow y by A5,XBOOLE_0:def 4;
then
A6: z1 << y by WAYBEL_3:7;
z in B by A5,XBOOLE_0:def 4;
then z1 <= x by A3,A6;
hence thesis by WAYBEL_0:17;
end;
A7: ex_sup_of downarrow x,L by YELLOW_0:17;
ex_sup_of waybelow y /\ B,L by YELLOW_0:17;
then sup (waybelow y /\ B) <= sup (downarrow x) by A7,A4,YELLOW_0:34;
then y <= sup (downarrow x) by A1,Def7;
hence contradiction by A2,WAYBEL_0:34;
end;
end;
assume
A8: 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;
now
let x be Element of L;
A9: ex_sup_of waybelow x,L by YELLOW_0:17;
ex_sup_of waybelow x /\ B,L by YELLOW_0:17;
then
A10: sup (waybelow x /\ B) <= sup waybelow x by A9,XBOOLE_1:17,YELLOW_0:34;
A11: x <= sup (waybelow x /\ B)
proof
assume not x <= sup (waybelow x /\ B);
then consider b be Element of L such that
A12: b in B and
A13: not b <= sup (waybelow x /\ B) and
A14: b << x by A8;
b in waybelow x by A14,WAYBEL_3:7;
then b in waybelow x /\ B by A12,XBOOLE_0:def 4;
hence contradiction by A13,YELLOW_2:22;
end;
x = sup waybelow x by WAYBEL_3:def 5;
hence x = sup (waybelow x /\ B) by A10,A11,YELLOW_0:def 3;
end;
hence thesis by Def7;
end;
theorem Th47: :: 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
proof
let L be continuous lower-bounded LATTICE;
let B be join-closed Subset of L;
assume
A1: Bottom L in B;
thus B is CLbasis of L implies for x,y be Element of L st x << y ex b be
Element of L st b in B & x <= b & b << y
proof
assume
A2: B is CLbasis of L;
let x,y be Element of L;
assume
A3: x << y;
Bottom L << y by WAYBEL_3:4;
then
A4: Bottom L in waybelow y by WAYBEL_3:7;
waybelow y /\ B is join-closed by Th33;
then reconsider
D = waybelow y /\ B as non empty directed Subset of L by A1,A4,
XBOOLE_0:def 4;
y = sup D by A2,Def7;
then consider b be Element of L such that
A5: b in D and
A6: x <= b by A3,WAYBEL_3:def 1;
take b;
b in waybelow y by A5,XBOOLE_0:def 4;
hence thesis by A5,A6,WAYBEL_3:7,XBOOLE_0:def 4;
end;
assume
A7: for x,y be Element of L st x << y ex b be Element of L st b in B &
x <= b & b << y;
now
let x be Element of L;
A8: x <= sup (waybelow x /\ B)
proof
A9: for x being Element of L holds waybelow x is non empty directed;
assume not x <= sup (waybelow x /\ B);
then consider u be Element of L such that
A10: u << x and
A11: not u <= sup (waybelow x /\ B) by A9,WAYBEL_3:24;
consider b be Element of L such that
A12: b in B and
A13: u <= b and
A14: b << x by A7,A10;
b in waybelow x by A14,WAYBEL_3:7;
then
A15: b in waybelow x /\ B by A12,XBOOLE_0:def 4;
A16: sup (waybelow x /\ B) is_>=_than waybelow x /\ B by YELLOW_0:32;
not b <= sup (waybelow x /\ B) by A11,A13,YELLOW_0:def 2;
hence contradiction by A15,A16;
end;
waybelow x /\ B c= waybelow x by XBOOLE_1:17;
then sup (waybelow x /\ B) <= sup waybelow x by WAYBEL_7:1;
then sup (waybelow x /\ B) <= x by WAYBEL_3:def 5;
hence x = sup (waybelow x /\ B) by A8,YELLOW_0:def 3;
end;
hence thesis by Def7;
end;
Lm2: for L be continuous lower-bounded LATTICE for B be join-closed Subset of
L st Bottom L in B holds (for x,y be Element of L st x << y ex b be Element of
L st b in B & x <= b & b << y) implies (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)
proof
let L be continuous lower-bounded LATTICE;
let B be join-closed Subset of L;
assume
A1: Bottom L in B;
assume
A2: for x,y be Element of L st x << y ex b be Element of L st b in B & x
<= b & b << y;
thus the carrier of CompactSublatt L c= B
proof
let z be object;
assume
A3: z in the carrier of CompactSublatt L;
the carrier of CompactSublatt L c= the carrier of L by YELLOW_0:def 13;
then reconsider z1 = z as Element of L by A3;
z1 is compact by A3,WAYBEL_8:def 1;
then z1 << z1 by WAYBEL_3:def 2;
then consider b be Element of L such that
A4: b in B and
A5: z1 <= b and
A6: b << z1 by A2;
b <= z1 by A6,WAYBEL_3:1;
hence thesis by A4,A5,YELLOW_0:def 3;
end;
let x,y be Element of L;
assume
A7: not y <= x;
B is CLbasis of L by A1,A2,Th47;
then consider b be Element of L such that
A8: b in B and
A9: not b <= x and
A10: b << y by A7,Th46;
take b;
thus thesis by A8,A9,A10,WAYBEL_3:1;
end;
Lm3: for L be continuous lower-bounded LATTICE for B be Subset of L holds (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) implies 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
proof
let L be continuous lower-bounded LATTICE;
let B be Subset of L;
assume
A1: 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;
let x,y be Element of L;
A2: for z be Element of L holds waybelow z is non empty directed;
assume not y <= x;
then consider y1 be Element of L such that
A3: y1 << y and
A4: not y1 <= x by A2,WAYBEL_3:24;
consider b be Element of L such that
A5: b in B and
A6: not b <= x and
A7: b <= y1 by A1,A4;
take b;
thus thesis by A3,A5,A6,A7,WAYBEL_3:2;
end;
theorem Th48: :: 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)
proof
let L be continuous lower-bounded LATTICE;
let B be join-closed Subset of L;
assume
A1: Bottom L in B;
thus B is CLbasis of L implies (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)
proof
assume B is CLbasis of L;
then for x,y be Element of L st x << y ex b be Element of L st b in B & x
<= b & b << y by A1,Th47;
hence thesis by A1,Lm2;
end;
assume that
the carrier of CompactSublatt L c= B and
A2: 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;
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 by A2,Lm3;
hence thesis by Th46;
end;
theorem :: 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
proof
let L be continuous lower-bounded LATTICE;
let B be join-closed Subset of L;
assume
A1: Bottom L in B;
thus B is CLbasis of L implies 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
proof
assume B is CLbasis of L;
then for x,y be Element of L st x << y ex b be Element of L st b in B & x
<= b & b << y by A1,Th47;
hence thesis by A1,Lm2;
end;
assume 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;
then 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 by Lm3;
hence thesis by Th46;
end;
theorem Th50:
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
proof
let L be lower-bounded sup-Semilattice;
let S be non empty full SubRelStr of L;
assume that
A1: Bottom L in the carrier of S and
A2: the carrier of S is join-closed Subset of L;
let x be Element of L;
Bottom L << x by WAYBEL_3:4;
then Bottom L in waybelow x by WAYBEL_3:7;
then reconsider
X = waybelow x /\ (the carrier of S) as non empty Subset of S by A1,
XBOOLE_0:def 4,XBOOLE_1:17;
reconsider S1 = the carrier of S as join-closed Subset of L by A2;
A3: now
let a,b be Element of S;
reconsider a1 = a, b1 = b as Element of L by YELLOW_0:58;
assume that
A4: a in X and
A5: b <= a;
a in waybelow x by A4,XBOOLE_0:def 4;
then
A6: a1 << x by WAYBEL_3:7;
b1 <= a1 by A5,YELLOW_0:59;
then b1 << x by A6,WAYBEL_3:2;
then b in waybelow x by WAYBEL_3:7;
hence b in X by XBOOLE_0:def 4;
end;
waybelow x /\ S1 is join-closed by Th33;
hence thesis by A3,WAYBEL10:23,WAYBEL_0:def 19;
end;
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
:Def10:
for I be Ideal of S holds it.I = "\/"(I,L);
existence
proof
deffunc F(set) = "\/"($1,L);
set P = InclPoset Ids S;
A1: for I be set st I in the carrier of P holds F(I) in the carrier of L;
ex f be Function of the carrier of P, the carrier of L st
for I be set
st I in the carrier of P holds f.I = F(I) from FUNCT_2:sch 11 (A1);
then consider f be Function of the carrier of P,the carrier of L such that
A2: for I be set st I in the carrier of P holds f.I = "\/"(I,L);
reconsider f as Function of P,L;
take f;
for I be Ideal of S holds f.I = "\/"(I,L)
proof
let I be Ideal of S;
I in the set of all X where X is Ideal of S ;
then I in the carrier of RelStr(#Ids S, RelIncl Ids S#) by
WAYBEL_0:def 23;
then I in the carrier of P by YELLOW_1:def 1;
hence thesis by A2;
end;
hence thesis;
end;
uniqueness
proof
set P = InclPoset Ids S;
let f,g be Function of InclPoset Ids S, L;
assume that
A3: for I be Ideal of S holds f.I = "\/"(I,L) and
A4: for I be Ideal of S holds g.I = "\/"(I,L);
A5: the carrier of P = the carrier of RelStr(#Ids S, RelIncl Ids S#) by
YELLOW_1:def 1
.= Ids S;
A6: now
let x be object;
assume x in the carrier of P;
then x in the set of all X where X is Ideal of S by A5,
WAYBEL_0:def 23;
then ex I be Ideal of S st x = I;
then reconsider I = x as Ideal of S;
f.I = "\/"(I,L) by A3;
hence f.x = g.x by A4;
end;
A7: dom g = the carrier of P by FUNCT_2:def 1;
dom f = the carrier of P by FUNCT_2:def 1;
hence f = g by A7,A6,FUNCT_1:2;
end;
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
:Def11
:
for I be Ideal of S ex J be Subset of L st I = J & it.I = downarrow J;
existence
proof
defpred P[set,set] means ex J be Subset of L st $1 = J & $2 = downarrow J;
set R = InclPoset Ids L;
set P = InclPoset Ids S;
A1: for I be Element of P ex K be Element of R st P[I,K]
proof
let I be Element of P;
I in the carrier of P;
then I in Ids S by YELLOW_1:1;
then I in the set of all X where X is Ideal of S by
WAYBEL_0:def 23;
then consider J be Ideal of S such that
A2: J = I;
reconsider J as non empty directed Subset of L by YELLOW_2:7;
downarrow J in the set of all X where X is Ideal of L ;
then downarrow J in Ids L by WAYBEL_0:def 23;
then reconsider K = downarrow J as Element of R by YELLOW_1:1;
take K,J;
thus thesis by A2;
end;
ex f be Function of the carrier of P, the carrier of R st for I be
Element of P holds P[I,f.I] from FUNCT_2:sch 3(A1);
then consider f be Function of the carrier of P,the carrier of R such that
A3: for I be Element of P ex J be Subset of L st I = J & f.I = downarrow J;
reconsider f as Function of P,R;
take f;
for I be Ideal of S ex J be Subset of L st I = J & f.I = downarrow J
proof
let I be Ideal of S;
I in the set of all X where X is Ideal of S ;
then I in the carrier of RelStr(#Ids S, RelIncl Ids S#) by
WAYBEL_0:def 23;
then I in the carrier of P by YELLOW_1:def 1;
then consider J be Subset of L such that
A4: I = J and
A5: f.I = downarrow J by A3;
reconsider J as Subset of L;
take J;
thus thesis by A4,A5;
end;
hence thesis;
end;
uniqueness
proof
set P = InclPoset Ids S;
let f,g be Function of InclPoset Ids S, InclPoset Ids L;
assume that
A6: for I be Ideal of S ex J be Subset of L st I = J & f.I = downarrow J and
A7: for I be Ideal of S ex J be Subset of L st I = J & g.I = downarrow J;
A8: the carrier of P = the carrier of RelStr(#Ids S, RelIncl Ids S#) by
YELLOW_1:def 1
.= Ids S;
A9: now
let x be object;
assume x in the carrier of P;
then x in the set of all X where X is Ideal of S by A8,
WAYBEL_0:def 23;
then ex I be Ideal of S st x = I;
then reconsider I = x as Ideal of S;
A10: ex J2 be Subset of L st I = J2 & g.I = downarrow J2 by A7;
ex J1 be Subset of L st I = J1 & f.I = downarrow J1 by A6;
hence f.x = g.x by A10;
end;
A11: dom g = the carrier of P by FUNCT_2:def 1;
dom f = the carrier of P by FUNCT_2:def 1;
hence f = g by A11,A9,FUNCT_1:2;
end;
end;
registration
let L be reflexive RelStr;
let B be Subset of L;
cluster subrelstr B -> reflexive;
coherence;
end;
registration
let L be transitive RelStr;
let B be Subset of L;
cluster subrelstr B -> transitive;
coherence;
end;
registration
let L be antisymmetric RelStr;
let B be Subset of L;
cluster subrelstr B -> antisymmetric;
coherence;
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
:Def12:
for x be Element of L holds it.x = waybelow x /\ B;
existence
proof
defpred P[set,set] means ex y be Element of L st $1 = y & $2 = waybelow y
/\ B;
set P = InclPoset Ids subrelstr B;
A1: for x be Element of L ex z be Element of P st P[x,z]
proof
let x be Element of L;
reconsider y = x as Element of L;
A2: the carrier of subrelstr B = B by YELLOW_0:def 15;
Bottom L in B by Def8;
then waybelow y /\ B is Ideal of subrelstr B by A2,Th50;
then reconsider z = waybelow y /\ B as Element of P by YELLOW_2:41;
take z,y;
thus thesis;
end;
ex f be Function of the carrier of L, the carrier of P st for x be
Element of L holds P[x,f.x] from FUNCT_2:sch 3(A1);
then consider f be Function of the carrier of L,the carrier of P such that
A3: for x be Element of L ex y be Element of L st x = y & f.x =
waybelow y /\ B;
reconsider f as Function of L,P;
take f;
now
let x be Element of L;
ex y be Element of L st x = y & f.x = waybelow y /\ B by A3;
hence f.x = waybelow x /\ B;
end;
hence thesis;
end;
uniqueness
proof
let f,g be Function of L,InclPoset Ids subrelstr B;
assume that
A4: for x be Element of L holds f.x = waybelow x /\ B and
A5: for x be Element of L holds g.x = waybelow x /\ B;
A6: now
let z be object;
assume z in the carrier of L;
then reconsider z1 = z as Element of L;
f.z = waybelow z1 /\ B by A4;
hence f.z = g.z by A5;
end;
A7: dom g = the carrier of L by FUNCT_2:def 1;
dom f = the carrier of L by FUNCT_2:def 1;
hence f = g by A7,A6,FUNCT_1:2;
end;
end;
theorem Th51:
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
proof
let L be non empty reflexive transitive RelStr;
let S be non empty full SubRelStr of L;
set P = InclPoset Ids S;
thus dom(supMap S) = the carrier of P by FUNCT_2:def 1
.= the carrier of RelStr(#Ids S, RelIncl Ids S#) by YELLOW_1:def 1
.= Ids S;
thus thesis;
end;
theorem Th52:
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
proof
let L be non empty reflexive transitive RelStr;
let S be non empty full SubRelStr of L;
let x be set;
hereby
assume x in dom supMap S;
then x in Ids S by Th51;
then x in the set of all X where X is Ideal of S by
WAYBEL_0:def 23;
then ex I be Ideal of S st x = I;
hence x is Ideal of S;
end;
assume x is Ideal of S;
then x in the set of all X where X is Ideal of S;
then x in Ids S by WAYBEL_0:def 23;
hence thesis by Th51;
end;
theorem Th53:
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
proof
let L be non empty reflexive transitive RelStr;
let S be non empty full SubRelStr of L;
set P = InclPoset Ids S;
thus dom(idsMap S) = the carrier of P by FUNCT_2:def 1
.= the carrier of RelStr(#Ids S, RelIncl Ids S#) by YELLOW_1:def 1
.= Ids S;
thus thesis by YELLOW_1:1;
end;
theorem Th54:
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
proof
let L be non empty reflexive transitive RelStr;
let S be non empty full SubRelStr of L;
let x be set;
hereby
assume x in dom idsMap S;
then x in Ids S by Th53;
then x in the set of all X where X is Ideal of S by
WAYBEL_0:def 23;
then ex I be Ideal of S st x = I;
hence x is Ideal of S;
end;
assume x is Ideal of S;
then x in the set of all X where X is Ideal of S;
then x in Ids S by WAYBEL_0:def 23;
hence thesis by Th53;
end;
theorem Th55:
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
proof
let L be non empty reflexive transitive RelStr;
let S be non empty full SubRelStr of L;
let x be set;
assume
A1: x in rng idsMap S;
rng idsMap S is Subset of Ids L by Th53;
then x in Ids L by A1;
then x in the set of all X where X is Ideal of L by WAYBEL_0:def 23;
then ex I be Ideal of L st x = I;
hence thesis;
end;
theorem
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 by FUNCT_2:def 1,YELLOW_1:1;
theorem
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
proof
let L be lower-bounded continuous sup-Semilattice;
let B be with_bottom CLbasis of L;
let x be set;
A1: rng baseMap B is Subset of Ids subrelstr B by YELLOW_1:1;
assume x in rng baseMap B;
then x in Ids subrelstr B by A1;
then x in the set of all X where X is Ideal of subrelstr B by
WAYBEL_0:def 23;
then ex I be Ideal of subrelstr B st x = I;
hence thesis;
end;
theorem Th58:
for L be up-complete non empty Poset for S be non empty full
SubRelStr of L holds supMap S is monotone
proof
let L be up-complete non empty Poset;
let S be non empty full SubRelStr of L;
set f = supMap S;
now
let x, y be Element of InclPoset Ids S;
reconsider I = x, J = y as Ideal of S by YELLOW_2:41;
assume x <= y;
then
A1: I c= J by YELLOW_1:3;
I is non empty directed Subset of L by YELLOW_2:7;
then
A2: ex_sup_of I,L by WAYBEL_0:75;
J is non empty directed Subset of L by YELLOW_2:7;
then
A3: ex_sup_of J,L by WAYBEL_0:75;
A4: f.y = "\/"(J,L) by Def10;
f.x = "\/"(I,L) by Def10;
hence f.x <= f.y by A2,A3,A1,A4,YELLOW_0:34;
end;
hence thesis by WAYBEL_1:def 2;
end;
theorem Th59:
for L be non empty reflexive transitive RelStr for S be non
empty full SubRelStr of L holds idsMap S is monotone
proof
let L be non empty reflexive transitive RelStr;
let S be non empty full SubRelStr of L;
set f = idsMap S;
now
let x, y be Element of InclPoset Ids S;
reconsider I = x, J = y as Ideal of S by YELLOW_2:41;
consider K1 be Subset of L such that
A1: I = K1 and
A2: f.x = downarrow K1 by Def11;
consider K2 be Subset of L such that
A3: J = K2 and
A4: f.y = downarrow K2 by Def11;
assume x <= y;
then I c= J by YELLOW_1:3;
then downarrow K1 c= downarrow K2 by A1,A3,YELLOW_3:6;
hence f.x <= f.y by A2,A4,YELLOW_1:3;
end;
hence thesis by WAYBEL_1:def 2;
end;
theorem Th60:
for L be lower-bounded continuous sup-Semilattice for B be
with_bottom CLbasis of L holds baseMap B is monotone
proof
let L be lower-bounded continuous sup-Semilattice;
let B be with_bottom CLbasis of L;
set f = baseMap B;
now
let x, y be Element of L;
assume
A1: x <= y;
A2: f.y = waybelow y /\ B by Def12;
f.x = waybelow x /\ B by Def12;
then f.x c= f.y by A1,A2,WAYBEL_3:12,XBOOLE_1:26;
hence f.x <= f.y by YELLOW_1:3;
end;
hence thesis by WAYBEL_1:def 2;
end;
registration
let L be up-complete non empty Poset;
let S be non empty full SubRelStr of L;
cluster supMap S -> monotone;
coherence by Th58;
end;
registration
let L be non empty reflexive transitive RelStr;
let S be non empty full SubRelStr of L;
cluster idsMap S -> monotone;
coherence by Th59;
end;
registration
let L be lower-bounded continuous sup-Semilattice;
let B be with_bottom CLbasis of L;
cluster baseMap B -> monotone;
coherence by Th60;
end;
theorem Th61:
for L be lower-bounded continuous sup-Semilattice for B be
with_bottom CLbasis of L holds idsMap (subrelstr B) is sups-preserving
proof
let L be lower-bounded continuous sup-Semilattice;
let B be with_bottom CLbasis of L;
set f = idsMap (subrelstr B);
A1: subrelstr B is join-inheriting by Def2;
A2: Bottom L in B by Def8;
then
A3: Bottom L in the carrier of subrelstr B by YELLOW_0:def 15;
now
let X be Subset of InclPoset Ids subrelstr B;
reconsider supX = sup X as Ideal of subrelstr B by YELLOW_2:41;
reconsider unionX = union X as Subset of L by WAYBEL13:3;
reconsider dfuX = downarrow finsups union X as Subset of L by WAYBEL13:3;
reconsider fuX = finsups union X as Subset of L by WAYBEL13:3;
A4: ex J be Subset of L st supX = J & f.supX = downarrow J by Def11;
now
assume ex_sup_of X,InclPoset Ids subrelstr B;
thus ex_sup_of f.:X,InclPoset Ids L by YELLOW_0:17;
A5: downarrow finsups union (f.:X) c= downarrow dfuX
proof
defpred P[object,object] means
ex I be Element of InclPoset Ids subrelstr B,
z1,z2 be Element of L st z1 = $1 & z2 = $2 & I in X & $2 in I & z1 <= z2;
let x be object;
assume
A6: x in downarrow finsups union (f.:X);
then reconsider x1 = x as Element of L;
consider y1 be Element of L such that
A7: y1 >= x1 and
A8: y1 in finsups union (f.:X) by A6,WAYBEL_0:def 15;
y1 in { "\/"(V,L) where V is finite Subset of union (f.:X) :
ex_sup_of V,L } by A8,WAYBEL_0:def 27;
then consider Y be finite Subset of union (f.:X) such that
A9: y1 = "\/"(Y,L) and
ex_sup_of Y,L;
A10: for z be object st z in Y ex v be Element of B st P[z,v]
proof
let z be object;
assume z in Y;
then consider J be set such that
A11: z in J and
A12: J in f.:X by TARSKI:def 4;
consider I be object such that
I in dom f and
A13: I in X and
A14: J = f.I by A12,FUNCT_1:def 6;
reconsider I as Element of InclPoset Ids subrelstr B by A13;
f.I is Element of InclPoset Ids L;
then reconsider J as Element of InclPoset Ids L by A14;
J is Ideal of L by YELLOW_2:41;
then reconsider z1 = z as Element of L by A11;
reconsider I1 = I as Ideal of subrelstr B by YELLOW_2:41;
consider I2 be Subset of L such that
A15: I1 = I2 and
A16: f.I1 = downarrow I2 by Def11;
consider z2 be Element of L such that
A17: z2 >= z1 and
A18: z2 in I2 by A11,A14,A16,WAYBEL_0:def 15;
reconsider v = z2 as Element of B by A15,A18,YELLOW_0:def 15;
take v,I,z1,z2;
thus thesis by A13,A15,A17,A18;
end;
consider g be Function of Y,B such that
A19: for z be object st z in Y holds P[z,g.z] from MONOID_1:sch 1(A10
);
reconsider Z = rng g as finite Subset of subrelstr B by YELLOW_0:def 15
;
A20: dom g = Y by FUNCT_2:def 1;
A21: "\/"(rng g,L) is_>=_than Y
proof
let a be Element of L;
A22: "\/"(rng g,L) is_>=_than rng g by YELLOW_0:32;
assume
A23: a in Y;
then consider
I be Element of InclPoset Ids subrelstr B, a1,a2 be Element
of L such that
A24: a1 = a and
A25: a2 = g.a and
I in X and
g.a in I and
A26: a1 <= a2 by A19;
g.a in rng g by A20,A23,FUNCT_1:def 3;
then a2 <= "\/"(rng g,L) by A25,A22;
hence a <= "\/"(rng g,L) by A24,A26,YELLOW_0:def 2;
end;
A27: ex_sup_of Z,subrelstr B
proof
per cases;
suppose
Z is non empty;
hence thesis by YELLOW_0:54;
end;
suppose
Z is empty;
hence thesis by YELLOW_0:42;
end;
end;
rng g c= union X
proof
let a be object;
assume a in rng g;
then consider b be object such that
A28: b in dom g and
A29: a = g.b by FUNCT_1:def 3;
ex I be Element of InclPoset Ids subrelstr B, b1,b2 be Element
of L st b1 = b & b2 = g.b & I in X & g.b in I & b1 <= b2 by A19,A28;
hence thesis by A29,TARSKI:def 4;
end;
then "\/"(Z,subrelstr B) in { "\/"(V,subrelstr B) where V is finite
Subset of union X : ex_sup_of V,subrelstr B } by A27;
then
A30: "\/"(rng g,subrelstr B) in finsups union X by WAYBEL_0:def 27;
"\/"(Z,L) in the carrier of subrelstr B
proof
per cases;
suppose
Z is non empty;
hence thesis by A1,WAYBEL21:15;
end;
suppose
Z is empty;
hence thesis by A2,YELLOW_0:def 15;
end;
end;
then reconsider xl = "\/"(Z,L) as Element of subrelstr B;
reconsider srg = "\/"(rng g,subrelstr B) as Element of L by YELLOW_0:58
;
A31: ex_sup_of Z,L by YELLOW_0:17;
A32: now
let b be Element of subrelstr B;
reconsider b1 = b as Element of L by YELLOW_0:58;
assume
A33: b is_>=_than Z;
b1 is_>=_than Z
by A33,YELLOW_0:59;
then "\/"(Z, L) <= b1 by A31,YELLOW_0:30;
hence xl <= b by YELLOW_0:60;
end;
A34: "\/"(Z, L) is_>=_than Z by A31,YELLOW_0:30;
xl is_>=_than Z
proof
let b be Element of subrelstr B;
reconsider b1 = b as Element of L by YELLOW_0:58;
assume b in Z;
then b1 <= "\/"(Z, L) by A34;
hence b <= xl by YELLOW_0:60;
end;
then "\/"(Z,subrelstr B) = "\/"(Z,L) by A32,YELLOW_0:30;
then "\/"(Y,L) <= srg by A21,YELLOW_0:32;
then
A35: x1 <= srg by A7,A9,YELLOW_0:def 2;
finsups union X c= downarrow finsups union X by WAYBEL_0:16;
hence thesis by A35,A30,WAYBEL_0:def 15;
end;
now
let x be set;
assume
A36: x in X;
then reconsider x1 = x as Ideal of subrelstr B by YELLOW_2:41;
consider x2 be Subset of L such that
A37: x1 = x2 and
A38: f.x1 = downarrow x2 by Def11;
x in the carrier of InclPoset Ids subrelstr B by A36;
then x1 in dom f by FUNCT_2:def 1;
then
A39: f.x1 in f.:X by A36,FUNCT_1:def 6;
thus x c= union (f.:X)
proof
let y be object;
assume
A40: y in x;
x c= downarrow x2 by A37,WAYBEL_0:16;
hence thesis by A38,A39,A40,TARSKI:def 4;
end;
end;
then union X c= union (f.:X) by ZFMISC_1:76;
then
A41: finsups unionX c= finsups union (f.:X) by Th2;
finsups union X c= finsups unionX by A3,A1,Th5;
then finsups union X c= finsups union (f.:X) by A41;
then
A42: downarrow fuX c= downarrow finsups union (f.:X) by YELLOW_3:6;
downarrow finsups union X c= downarrow fuX by Th11;
then dfuX c= downarrow finsups union (f.:X) by A42;
then downarrow dfuX c= downarrow downarrow finsups union (f.:X) by
YELLOW_3:6;
then
A43: downarrow dfuX c= downarrow finsups union (f.:X) by Th7;
thus sup (f.:X) = downarrow finsups union (f.:X) by Th6
.= downarrow dfuX by A5,A43
.= f.sup X by A4,Th6;
end;
hence f preserves_sup_of X by WAYBEL_0:def 31;
end;
hence thesis by WAYBEL_0:def 33;
end;
theorem Th62:
for L be up-complete non empty Poset for S be non empty full
SubRelStr of L holds supMap S = (SupMap L)*(idsMap S)
proof
let L be up-complete non empty Poset;
let S be non empty full SubRelStr of L;
A1: now
let x be object;
thus x in dom (supMap S) implies x in dom (idsMap S) & (idsMap S).x in dom
(SupMap L)
proof
assume x in dom (supMap S);
then x is Ideal of S by Th52;
hence x in dom (idsMap S) by Th54;
then (idsMap S).x in rng (idsMap S) by FUNCT_1:def 3;
then (idsMap S).x is Ideal of L by Th55;
hence thesis by YELLOW_2:50;
end;
thus x in dom (idsMap S) & (idsMap S).x in dom (SupMap L) implies x in dom
(supMap S)
proof
assume that
A2: x in dom (idsMap S) and
(idsMap S).x in dom (SupMap L);
x is Ideal of S by A2,Th54;
hence thesis by Th52;
end;
end;
now
let x be object;
assume x in dom (supMap S);
then reconsider I = x as Ideal of S by Th52;
consider J be Subset of L such that
A3: I = J and
A4: (idsMap S).I = downarrow J by Def11;
reconsider J as non empty directed Subset of L by A3,YELLOW_2:7;
A5: ex_sup_of J,L by WAYBEL_0:75;
thus (supMap S).x = "\/"(I,L) by Def10
.= sup (downarrow J) by A3,A5,WAYBEL_0:33
.= (SupMap L).((idsMap S).x) by A4,YELLOW_2:def 3;
end;
hence thesis by A1,FUNCT_1:10;
end;
theorem Th63: :: 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
proof
let L be lower-bounded continuous sup-Semilattice;
let B be with_bottom CLbasis of L;
now
let x be Element of L, y be Element of InclPoset Ids subrelstr B;
reconsider I = y as Ideal of subrelstr B by YELLOW_2:41;
reconsider J = I as non empty directed Subset of L by YELLOW_2:7;
A1: ex_sup_of waybelow x /\ B,L by YELLOW_0:17;
thus x <= (supMap subrelstr B).y implies (baseMap B).x <= y
proof
A2: downarrow J /\ B c= J
proof
let z be object;
assume
A3: z in downarrow J /\ B;
then reconsider z1 = z as Element of L;
z in B by A3,XBOOLE_0:def 4;
then reconsider z2 = z as Element of subrelstr B by YELLOW_0:def 15;
z in downarrow J by A3,XBOOLE_0:def 4;
then consider v1 be Element of L such that
A4: v1 >= z1 and
A5: v1 in J by WAYBEL_0:def 15;
reconsider v2 = v1 as Element of subrelstr B by A5;
z2 <= v2 by A4,YELLOW_0:60;
hence thesis by A5,WAYBEL_0:def 19;
end;
assume x <= (supMap subrelstr B).y;
then x <= "\/"(I,L) by Def10;
then
A6: x <= sup downarrow J by WAYBEL_0:33,YELLOW_0:17;
waybelow x c= downarrow J
proof
let z be object;
assume
A7: z in waybelow x;
then reconsider z1 = z as Element of L;
z1 << x by A7,WAYBEL_3:7;
hence thesis by A6,WAYBEL_3:20;
end;
then waybelow x /\ B c= downarrow J /\ B by XBOOLE_1:26;
then waybelow x /\ B c= y by A2;
then (baseMap B).x c= y by Def12;
hence thesis by YELLOW_1:3;
end;
A8: ex_sup_of J,L by YELLOW_0:17;
thus (baseMap B).x <= y implies x <= (supMap subrelstr B).y
proof
assume (baseMap B).x <= y;
then (baseMap B).x c= y by YELLOW_1:3;
then waybelow x /\ B c= y by Def12;
then sup (waybelow x /\ B) <= sup J by A8,A1,YELLOW_0:34;
then x <= "\/"(I,L) by Def7;
hence thesis by Def10;
end;
end;
hence thesis by WAYBEL_1:8;
end;
theorem Th64: :: 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
proof
let L be lower-bounded continuous sup-Semilattice;
let B be with_bottom CLbasis of L;
[supMap subrelstr B,baseMap B] is Galois by Th63;
hence thesis by WAYBEL_1:9;
end;
theorem Th65: :: 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
proof
let L be lower-bounded continuous sup-Semilattice;
let B be with_bottom CLbasis of L;
A1: Bottom L in B by Def8;
thus rng supMap subrelstr B = the carrier of L
proof
thus rng supMap subrelstr B c= the carrier of L;
let x be object;
assume x in the carrier of L;
then reconsider x1 = x as Element of L;
set z = waybelow x1 /\ B;
z is Subset of B by XBOOLE_1:17;
then reconsider z as Subset of subrelstr B by YELLOW_0:def 15;
A2: now
let a,b be Element of subrelstr B;
reconsider a1 = a, b1 = b as Element of L by YELLOW_0:58;
assume that
A3: a in z and
A4: b <= a;
a in waybelow x1 by A3,XBOOLE_0:def 4;
then
A5: a1 << x1 by WAYBEL_3:7;
b1 <= a1 by A4,YELLOW_0:59;
then b1 << x1 by A5,WAYBEL_3:2;
then
A6: b in waybelow x1 by WAYBEL_3:7;
b in the carrier of subrelstr B;
then b in B by YELLOW_0:def 15;
hence b in z by A6,XBOOLE_0:def 4;
end;
Bottom L << x1 by WAYBEL_3:4;
then
A7: Bottom L in waybelow x1 by WAYBEL_3:7;
waybelow x1 /\ B is join-closed by Th33;
then reconsider z as Ideal of subrelstr B by A1,A7,A2,WAYBEL10:23
,WAYBEL_0:def 19,XBOOLE_0:def 4;
z in the set of all X where X is Ideal of subrelstr B ;
then z in Ids subrelstr B by WAYBEL_0:def 23;
then
A8: z in dom supMap subrelstr B by Th51;
x = "\/"(z,L) by Def7
.= (supMap subrelstr B).z by Def10;
hence thesis by A8,FUNCT_1:def 3;
end;
end;
theorem Th66: :: 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
proof
let L be lower-bounded continuous sup-Semilattice;
let B be with_bottom CLbasis of L;
A1: SupMap L is sups-preserving by WAYBEL13:33;
thus supMap (subrelstr B) is infs-preserving by Th64,WAYBEL_1:12;
A2: supMap (subrelstr B) = (SupMap L)*(idsMap (subrelstr B)) by Th62;
idsMap (subrelstr B) is sups-preserving by Th61;
hence thesis by A2,A1,WAYBEL20:27;
end;
theorem
for L be lower-bounded continuous sup-Semilattice for B be with_bottom
CLbasis of L holds baseMap B is sups-preserving by Th64,WAYBEL_1:13;
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;
coherence by Th66;
cluster baseMap B -> sups-preserving;
coherence by Th64,WAYBEL_1:13;
end;
theorem Th68: :: 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
proof
let L be lower-bounded continuous sup-Semilattice;
let B be with_bottom CLbasis of L;
thus the carrier of CompactSublatt InclPoset(Ids subrelstr B) c= the set of
all downarrow
b where b is Element of subrelstr B
proof
let x be object;
assume
A1: x in the carrier of CompactSublatt InclPoset(Ids subrelstr B);
the carrier of CompactSublatt InclPoset(Ids subrelstr B) c= the
carrier of InclPoset(Ids subrelstr B) by YELLOW_0:def 13;
then reconsider x1 = x as Element of InclPoset(Ids subrelstr B) by A1;
x1 is compact by A1,WAYBEL_8:def 1;
then ex b be Element of subrelstr B st x1 = downarrow b by WAYBEL13:12;
hence thesis;
end;
thus the set of all downarrow b where b is Element of subrelstr B
c= the carrier of CompactSublatt InclPoset(Ids subrelstr B)
proof
let x be object;
assume
x in the set of all downarrow b where b is Element of subrelstr B ;
then
A2: ex b be Element of subrelstr B st x = downarrow b;
then reconsider x1 = x as Element of InclPoset(Ids subrelstr B) by
YELLOW_2:41;
x1 is compact by A2,WAYBEL13:12;
hence thesis by WAYBEL_8:def 1;
end;
end;
theorem :: 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
proof
let L be lower-bounded continuous sup-Semilattice;
let B be with_bottom CLbasis of L;
deffunc F(Element of subrelstr B) = downarrow $1;
A1: for x be Element of subrelstr B holds F(x) is Element of CompactSublatt
InclPoset Ids subrelstr B
proof
let x be Element of subrelstr B;
downarrow x in the set of all
downarrow b where b is Element of subrelstr B ;
hence thesis by Th68;
end;
consider f be Function of subrelstr B,CompactSublatt InclPoset Ids subrelstr
B such that
A2: for x be Element of subrelstr B holds f.x = F(x) from FUNCT_2:sch 9
( A1);
f is isomorphic by A2,WAYBEL13:13;
then
subrelstr B,CompactSublatt InclPoset(Ids subrelstr B) are_isomorphic by
WAYBEL_1:def 8;
hence thesis by WAYBEL_1:6;
end;
Lm4: for L be continuous lower-bounded LATTICE holds L is algebraic implies
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
proof
let L be continuous lower-bounded LATTICE;
assume L is algebraic;
hence the carrier of CompactSublatt L is with_bottom CLbasis of L by Th44;
let B be with_bottom CLbasis of L;
Bottom L in B by Def8;
hence thesis by Th48;
end;
theorem Th70:
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
proof
let L be continuous lower-bounded LATTICE;
let B be with_bottom CLbasis of L;
assume
A1: for B1 be with_bottom CLbasis of L holds B c= B1;
let J be Element of InclPoset Ids subrelstr B;
reconsider J1 = J as Ideal of subrelstr B by YELLOW_2:41;
reconsider J2 = J1 as non empty directed Subset of L by YELLOW_2:7;
set x = "\/"(J,L);
set C = (B \ J2) \/ (waybelow x /\ B);
A2: waybelow x /\ B c= B by XBOOLE_1:17;
B \ J2 c= B by XBOOLE_1:36;
then
A3: C c= B by A2,XBOOLE_1:8;
A4: now
let y be Element of L;
per cases;
suppose
not y <= x;
then consider u be Element of L such that
A5: u in B and
A6: not u <= x and
A7: u << y by Th46;
A8: now
let b be Element of L;
assume
A9: b is_>=_than waybelow y /\ C;
b is_>=_than waybelow y /\ B
proof
let c be Element of L;
u <= c "\/" u by YELLOW_0:22;
then
A10: not c "\/" u <= x by A6,YELLOW_0:def 2;
assume
A11: c in waybelow y /\ B;
then c in B by XBOOLE_0:def 4;
then sup {c,u} in B by A5,Th18;
then
A12: c "\/" u in B by YELLOW_0:41;
J is_<=_than x by YELLOW_0:32;
then not c "\/" u in J by A10;
then c "\/" u in B \ J by A12,XBOOLE_0:def 5;
then
A13: c "\/" u in C by XBOOLE_0:def 3;
c in waybelow y by A11,XBOOLE_0:def 4;
then c << y by WAYBEL_3:7;
then c "\/" u << y by A7,WAYBEL_3:3;
then c "\/" u in waybelow y by WAYBEL_3:7;
then c "\/" u in waybelow y /\ C by A13,XBOOLE_0:def 4;
then
A14: c "\/" u <= b by A9;
c <= c "\/" u by YELLOW_0:22;
hence c <= b by A14,YELLOW_0:def 2;
end;
hence sup(waybelow y /\ B) <= b by YELLOW_0:32;
end;
A15: waybelow y /\ B is_<=_than sup(waybelow y /\ B) by YELLOW_0:32;
sup(waybelow y /\ B) is_>=_than waybelow y /\ C
proof
let b be Element of L;
assume
A16: b in waybelow y /\ C;
then
A17: b in C by XBOOLE_0:def 4;
b in waybelow y by A16,XBOOLE_0:def 4;
then b in waybelow y /\ B by A3,A17,XBOOLE_0:def 4;
hence b <= sup(waybelow y /\ B) by A15;
end;
then sup(waybelow y /\ B) = sup(waybelow y /\ C) by A8,YELLOW_0:32;
hence y = sup(waybelow y /\ C) by Def7;
end;
suppose
A18: y <= x;
A19: waybelow y /\ B c= waybelow y /\ C
proof
let a be object;
assume
A20: a in waybelow y /\ B;
then reconsider a1 = a as Element of L;
A21: a in waybelow y by A20,XBOOLE_0:def 4;
then a1 << y by WAYBEL_3:7;
then a1 << x by A18,WAYBEL_3:2;
then
A22: a1 in waybelow x by WAYBEL_3:7;
a in B by A20,XBOOLE_0:def 4;
then a in waybelow x /\ B by A22,XBOOLE_0:def 4;
then a in C by XBOOLE_0:def 3;
hence thesis by A21,XBOOLE_0:def 4;
end;
waybelow y /\ C c= waybelow y /\ B by A3,XBOOLE_1:26;
then waybelow y /\ B = waybelow y /\ C by A19;
hence y = sup(waybelow y /\ C) by Def7;
end;
end;
A23: subrelstr B is join-inheriting by Def2;
subrelstr C is join-inheriting
proof
let a,b be Element of L;
assume that
A24: a in the carrier of subrelstr C and
A25: b in the carrier of subrelstr C and
A26: ex_sup_of {a,b},L;
A27: b in C by A25,YELLOW_0:def 15;
A28: a in C by A24,YELLOW_0:def 15;
then
A29: sup {a,b} in B by A3,A26,A27,Th16;
reconsider a1 = a, b1 = b as Element of subrelstr B by A3,A28,A27,
YELLOW_0:def 15;
A30: a1 <= a1 "\/" b1 by YELLOW_0:22;
A31: b1 <= a1 "\/" b1 by YELLOW_0:22;
now
per cases by A28,A27,XBOOLE_0:def 3;
suppose
a in B \ J & b in B \ J;
then
A32: not a in J by XBOOLE_0:def 5;
not a "\/" b in J
proof
assume a "\/" b in J;
then a1 "\/" b1 in J1 by A23,YELLOW_0:70;
hence contradiction by A30,A32,WAYBEL_0:def 19;
end;
then not sup {a,b} in J by YELLOW_0:41;
then sup {a,b} in B \ J by A29,XBOOLE_0:def 5;
hence sup {a,b} in C by XBOOLE_0:def 3;
end;
suppose
a in B \ J & b in waybelow x /\ B;
then
A33: not a in J by XBOOLE_0:def 5;
not a "\/" b in J
proof
assume a "\/" b in J;
then a1 "\/" b1 in J1 by A23,YELLOW_0:70;
hence contradiction by A30,A33,WAYBEL_0:def 19;
end;
then not sup {a,b} in J by YELLOW_0:41;
then sup {a,b} in B \ J by A29,XBOOLE_0:def 5;
hence sup {a,b} in C by XBOOLE_0:def 3;
end;
suppose
a in waybelow x /\ B & b in B \ J;
then
A34: not b in J by XBOOLE_0:def 5;
not a "\/" b in J
proof
assume a "\/" b in J;
then a1 "\/" b1 in J1 by A23,YELLOW_0:70;
hence contradiction by A31,A34,WAYBEL_0:def 19;
end;
then not sup {a,b} in J by YELLOW_0:41;
then sup {a,b} in B \ J by A29,XBOOLE_0:def 5;
hence sup {a,b} in C by XBOOLE_0:def 3;
end;
suppose
A35: a in waybelow x /\ B & b in waybelow x /\ B;
then b in waybelow x by XBOOLE_0:def 4;
then
A36: b << x by WAYBEL_3:7;
a in waybelow x by A35,XBOOLE_0:def 4;
then a << x by WAYBEL_3:7;
then a "\/" b << x by A36,WAYBEL_3:3;
then a "\/" b in waybelow x by WAYBEL_3:7;
then sup {a,b} in waybelow x by YELLOW_0:41;
then sup {a,b} in waybelow x /\ B by A29,XBOOLE_0:def 4;
hence sup {a,b} in C by XBOOLE_0:def 3;
end;
end;
hence thesis by YELLOW_0:def 15;
end;
then
A37: C is join-closed;
Bottom L << x by WAYBEL_3:4;
then
A38: Bottom L in waybelow x by WAYBEL_3:7;
reconsider C as CLbasis of L by A37,A4,Def7;
Bottom L in B by Def8;
then Bottom L in waybelow x /\ B by A38,XBOOLE_0:def 4;
then Bottom L in C by XBOOLE_0:def 3;
then C is with_bottom;
then B c= C by A1;
then
A39: B = C by A3;
A40: J c= waybelow x /\ B
proof
let a be object;
assume
A41: a in J;
then a in J1;
then a in the carrier of subrelstr B;
then
A42: a in C by A39,YELLOW_0:def 15;
not a in B \ J2 by A41,XBOOLE_0:def 5;
hence thesis by A42,XBOOLE_0:def 3;
end;
waybelow x /\ B c= J
proof
let a be object;
assume
A43: a in waybelow x /\ B;
then reconsider a1 = a as Element of L;
a in B by A43,XBOOLE_0:def 4;
then reconsider a2 = a as Element of subrelstr B by YELLOW_0:def 15;
a in waybelow x by A43,XBOOLE_0:def 4;
then a1 << x by WAYBEL_3:7;
then consider d1 be Element of L such that
A44: d1 in J2 and
A45: a1 <= d1 by WAYBEL_3:def 1;
reconsider d2 = d1 as Element of subrelstr B by A44;
a2 <= d2 by A45,YELLOW_0:60;
hence thesis by A44,WAYBEL_0:def 19;
end;
hence thesis by A40;
end;
Lm5: for L be continuous lower-bounded LATTICE holds (ex B be with_bottom
CLbasis of L st for B1 be with_bottom CLbasis of L holds B c= B1) implies L is
algebraic
proof
let L be continuous lower-bounded LATTICE;
given B be with_bottom CLbasis of L such that
A1: for B1 be with_bottom CLbasis of L holds B c= B1;
A2: for x,y be Element of InclPoset Ids subrelstr B holds x <= y iff (
supMap subrelstr B).x <= (supMap subrelstr B).y
proof
let x,y be Element of InclPoset Ids subrelstr B;
thus x <= y implies (supMap subrelstr B).x <= (supMap subrelstr B).y by
WAYBEL_1:def 2;
reconsider x1 = x, y1 = y as Ideal of subrelstr B by YELLOW_2:41;
assume
A3: (supMap subrelstr B).x <= (supMap subrelstr B).y;
A4: (supMap subrelstr B).y1 = "\/"(y1,L) by Def10;
(supMap subrelstr B).x1 = "\/"(x1,L) by Def10;
then waybelow "\/"(x1,L) c= waybelow "\/"(y1,L) by A4,A3,WAYBEL_3:25;
then
A5: waybelow "\/"(x1,L) /\ B c= waybelow "\/"(y1,L) /\ B by XBOOLE_1:26;
A6: y = waybelow "\/"(y,L) /\ B by A1,Th70;
x = waybelow "\/"(x,L) /\ B by A1,Th70;
hence thesis by A6,A5,YELLOW_1:3;
end;
the carrier of InclPoset Ids subrelstr B c= rng baseMap B
proof
let J be object;
reconsider JJ=J as set by TARSKI:1;
set x = "\/"(JJ,L);
assume J in the carrier of InclPoset Ids subrelstr B;
then J = waybelow x /\ B by A1,Th70;
then
A7: J = (baseMap B).x by Def12;
dom baseMap B = the carrier of L by FUNCT_2:def 1;
hence thesis by A7,FUNCT_1:def 3;
end;
then rng baseMap B = the carrier of InclPoset Ids subrelstr B;
then
A8: baseMap B is onto by FUNCT_2:def 3;
[supMap subrelstr B,baseMap B] is Galois by Th63;
then
A9: supMap subrelstr B is one-to-one by A8,WAYBEL_1:27;
rng supMap subrelstr B = the carrier of L by Th65;
then supMap subrelstr B is isomorphic by A9,A2,WAYBEL_0:66;
then
A10: InclPoset Ids subrelstr B,L are_isomorphic by WAYBEL_1:def 8;
InclPoset Ids subrelstr B is lower-bounded algebraic by WAYBEL13:10;
hence thesis by A10,WAYBEL13:32;
end;
theorem :: 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 by Lm4,Lm5;
theorem :: 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
proof
let L be continuous lower-bounded LATTICE;
thus L is algebraic implies ex B be with_bottom CLbasis of L st for B1 be
with_bottom CLbasis of L holds B c= B1
proof
assume
A1: L is algebraic;
then
A2: for B be with_bottom CLbasis of L holds the carrier of CompactSublatt
L c= B by Lm4;
the carrier of CompactSublatt L is with_bottom CLbasis of L by A1,Lm4;
hence thesis by A2;
end;
thus thesis by Lm5;
end;
theorem :: WAYBEL31:1, AK, 21.02.2006
for T be TopStruct for b be Basis of T holds weight T c= card b
proof
let T be TopStruct;
let b be Basis of T;
card b in the set of all card B1 where B1 is Basis of T ;
hence thesis by SETFAM_1:3;
end;
theorem :: WAYBEL31:1, AK, 21.02.2006
for T be TopStruct ex b be Basis of T st card b = weight T
proof
let T be TopStruct;
defpred P[Ordinal] means $1 in the set of all card b where b is Basis of T ;
set X = the set of all card b1 where b1 is Basis of T ;
A1: ex A be Ordinal st P[A]
proof
take card the topology of T;
the topology of T is Basis of T by CANTOR_1:2;
hence thesis;
end;
consider A be Ordinal such that
A2: P[A] and
A3: for C be Ordinal st P[C] holds A c= C from ORDINAL1:sch 1(A1);
consider b be Basis of T such that
A4: A = card b by A2;
A5: now
let x be object;
thus (for y be set holds y in X implies x in y) implies x in A by A2;
assume
A6: x in A;
let y be set;
assume
A7: y in X;
then ex B2 be Basis of T st y = card B2;
then reconsider y1 = y as Cardinal;
A c= y1 by A3,A7;
hence x in y by A6;
end;
take b;
the topology of T is Basis of T by CANTOR_1:2;
then card the topology of T in X;
hence thesis by A4,A5,SETFAM_1:def 1;
end;