:: Meet Continuous Lattices Revisited
:: by Artur Korni{\l}owicz
::
:: Received January 6, 2000
:: Copyright (c) 2000-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, TARSKI, SUBSET_1, RELAT_2, ORDERS_2, WAYBEL_0,
YELLOW_1, CARD_FIL, STRUCT_0, ZFMISC_1, XXREAL_0, LATTICE3, ORDINAL2,
YELLOW_0, LATTICES, WAYBEL_2, YELLOW_9, WAYBEL11, REWRITE1, WAYBEL_9,
PRE_TOPC, PROB_1, WAYBEL19, PRELAMB, ORDINAL1, SETFAM_1, CANTOR_1, DIRAF,
RCOMP_1, FINSET_1, RLVECT_3, COMPTS_1, YELLOW_8, TOPS_1, WAYBEL29,
YELLOW13, FUNCT_1, WAYBEL21, RELAT_1, PARTFUN1, MCART_1, TOPS_2,
WAYBEL_3, TDLAT_3, CONNSP_2, EQREL_1, WAYBEL_8, WAYBEL_6, WAYBEL30,
CARD_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1,
PARTFUN1, BINOP_1, FUNCT_3, SETFAM_1, DOMAIN_1, CARD_1, STRUCT_0,
FINSET_1, ORDERS_2, PRE_TOPC, TOPS_1, TOPS_2, COMPTS_1, CONNSP_2,
TDLAT_3, LATTICE3, BORSUK_1, CANTOR_1, YELLOW_0, WAYBEL_0, YELLOW_1,
WAYBEL_1, YELLOW_3, YELLOW_4, WAYBEL_2, WAYBEL_3, YELLOW_8, WAYBEL_6,
WAYBEL_8, WAYBEL_9, WAYBEL11, YELLOW_9, WAYBEL19, WAYBEL21, YELLOW13,
WAYBEL29;
constructors TOPS_1, TOPS_2, TDLAT_3, CANTOR_1, ORDERS_3, WAYBEL_1, YELLOW_4,
WAYBEL_6, WAYBEL_8, YELLOW_8, WAYBEL19, WAYBEL21, YELLOW13, WAYBEL29,
COMPTS_1, WAYBEL_2;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, STRUCT_0, TOPS_1,
BORSUK_1, LATTICE3, YELLOW_0, TEX_1, WAYBEL_0, YELLOW_1, YELLOW_2,
YELLOW_3, YELLOW_4, WAYBEL_2, WAYBEL_3, WAYBEL_4, YELLOW_6, WAYBEL_8,
WAYBEL10, WAYBEL11, WAYBEL14, YELLOW_9, YELLOW12, WAYBEL19, YELLOW13,
PRE_TOPC, CARD_1;
requirements BOOLE, SUBSET;
definitions TARSKI, PRE_TOPC, LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_2,
WAYBEL_3, YELLOW_8, WAYBEL19, WAYBEL11, YELLOW13, XBOOLE_0, TOPS_2;
equalities LATTICE3, WAYBEL_0, WAYBEL_3, WAYBEL11, BINOP_1, STRUCT_0;
expansions TARSKI, PRE_TOPC, LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_3, WAYBEL11,
YELLOW13, XBOOLE_0;
theorems TARSKI, PRE_TOPC, ORDERS_2, TOPS_1, TOPS_2, BORSUK_1, CONNSP_2,
TDLAT_3, COMPTS_1, RELAT_1, ZFMISC_1, FUNCT_1, FUNCT_2, FUNCT_3,
YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_3, YELLOW_4, YELLOW_8, WAYBEL_0,
WAYBEL_2, WAYBEL_3, WAYBEL_8, YELLOW13, WAYBEL11, WAYBEL12, WAYBEL14,
YELLOW_9, WAYBEL19, YELLOW12, WAYBEL21, WAYBEL29, SETFAM_1, XBOOLE_0,
XBOOLE_1, STRUCT_0;
schemes SUBSET_1, FINSET_1, DOMAIN_1;
begin
theorem Th1:
for x being set, D being non empty set holds x /\ union D = union
the set of all x /\ d where d is Element of D
proof
let x be set, D be non empty set;
hereby
let a be object;
assume
A1: a in x /\ union D;
then a in union D by XBOOLE_0:def 4;
then consider Z being set such that
A2: a in Z and
A3: Z in D by TARSKI:def 4;
A4: x /\ Z in the set of all x /\ d where d is Element of D by A3;
a in x by A1,XBOOLE_0:def 4;
then a in x /\ Z by A2,XBOOLE_0:def 4;
hence
a in union the set of all x /\ d where d is Element of D by A4,
TARSKI:def 4;
end;
let a be object;
assume a in union the set of all x /\ d where d is Element of D;
then consider Z being set such that
A5: a in Z and
A6: Z in the set of all x /\ d where d is Element of D by TARSKI:def 4;
consider d being Element of D such that
A7: Z = x /\ d and
not contradiction by A6;
a in d by A5,A7,XBOOLE_0:def 4;
then
A8: a in union D by TARSKI:def 4;
a in x by A5,A7,XBOOLE_0:def 4;
hence thesis by A8,XBOOLE_0:def 4;
end;
theorem Th2:
for R being non empty reflexive transitive RelStr, D being non
empty directed Subset of InclPoset Ids R holds union D is Ideal of R
proof
let R be non empty reflexive transitive RelStr, D be non empty directed
Subset of InclPoset Ids R;
set d = the Element of D;
D c= the carrier of InclPoset Ids R;
then
A1: D c= Ids R by YELLOW_1:1;
A2: D c= bool the carrier of R
proof
let d be object;
assume d in D;
then d in Ids R by A1;
then ex I being Ideal of R st d = I;
hence thesis;
end;
d in Ids R by A1;
then consider I being Ideal of R such that
A3: d = I and
not contradiction;
A4: for X being Subset of R st X in D holds X is directed
proof
let X be Subset of R;
assume X in D;
then X in Ids R by A1;
then ex I being Ideal of R st X = I;
hence thesis;
end;
A5: for X, Y being Subset of R st X in D & Y in D ex Z being Subset of R st
Z in D & X \/ Y c= Z
proof
let X, Y be Subset of R;
assume that
A6: X in D and
A7: Y in D;
reconsider X1 = X, Y1 = Y as Element of InclPoset Ids R by A6,A7;
consider Z1 being Element of InclPoset Ids R such that
A8: Z1 in D and
A9: X1 <= Z1 and
A10: Y1 <= Z1 by A6,A7,WAYBEL_0:def 1;
Z1 in Ids R by A1,A8;
then ex I being Ideal of R st Z1 = I;
then reconsider Z = Z1 as Subset of R;
take Z;
thus Z in D by A8;
A11: Y1 c= Z1 by A10,YELLOW_1:3;
X1 c= Z1 by A9,YELLOW_1:3;
hence thesis by A11,XBOOLE_1:8;
end;
A12: for X being Subset of R st X in D holds X is lower
proof
let X be Subset of R;
assume X in D;
then X in Ids R by A1;
then ex I being Ideal of R st X = I;
hence thesis;
end;
set i = the Element of I;
i in d by A3;
hence thesis by A12,A2,A4,A5,TARSKI:def 4,WAYBEL_0:26,46;
end;
Lm1: now
let R be non empty reflexive transitive RelStr, D be non empty directed
Subset of InclPoset Ids R, UD be Element of InclPoset Ids R such that
A1: UD = union D;
thus D is_<=_than UD
proof
let d be Element of InclPoset Ids R;
assume
A2: d in D;
d c= UD
by A1,A2,TARSKI:def 4;
hence d <= UD by YELLOW_1:3;
end;
end;
Lm2: now
let R be non empty reflexive transitive RelStr, D be non empty directed
Subset of InclPoset Ids R, UD be Element of InclPoset Ids R such that
A1: UD = union D;
thus for b being Element of InclPoset Ids R st b is_>=_than D holds UD <= b
proof
let b be Element of InclPoset Ids R such that
A2: for a being Element of InclPoset Ids R st a in D holds b >= a;
UD c= b
proof
let x be object;
assume x in UD;
then consider Z being set such that
A3: x in Z and
A4: Z in D by A1,TARSKI:def 4;
reconsider Z as Element of InclPoset Ids R by A4;
b >= Z by A2,A4;
then Z c= b by YELLOW_1:3;
hence thesis by A3;
end;
hence thesis by YELLOW_1:3;
end;
end;
:: Exercise 2.16 (i), p. 16
registration
let R be non empty reflexive transitive RelStr;
cluster InclPoset Ids R -> up-complete;
coherence
proof
set I = InclPoset Ids R;
let D be non empty directed Subset of I;
reconsider UD = union D as Ideal of R by Th2;
UD in Ids R;
then reconsider UD as Element of I by YELLOW_1:1;
take UD;
thus thesis by Lm1,Lm2;
end;
end;
theorem Th3:
for R being non empty reflexive transitive RelStr, D being non
empty directed Subset of InclPoset Ids R holds sup D = union D
proof
let R be non empty reflexive transitive RelStr, D be non empty directed
Subset of InclPoset Ids R;
reconsider UD = union D as Ideal of R by Th2;
A1: ex_sup_of D,InclPoset Ids R by WAYBEL_0:75;
UD in Ids R;
then reconsider UD as Element of InclPoset Ids R by YELLOW_1:1;
A2: for b being Element of InclPoset Ids R st b is_>=_than D holds UD <= b
by Lm2;
D is_<=_than UD by Lm1;
hence thesis by A2,A1,YELLOW_0:def 9;
end;
theorem Th4:
for R being Semilattice, D being non empty directed Subset of
InclPoset Ids R, x being Element of InclPoset Ids R holds sup ({x} "/\" D) =
union the set of all x /\ d where d is Element of D
proof
let R be Semilattice, D be non empty directed Subset of InclPoset Ids R, x
be Element of InclPoset Ids R;
set I = InclPoset Ids R, A = the set of all x /\ d where d is Element of D;
set xD = {x "/\" d where d is Element of I: d in D};
xD c= the carrier of I
proof
let a be object;
assume a in xD;
then ex d being Element of I st a = x "/\" d & d in D;
hence thesis;
end;
then reconsider xD as Subset of I;
A1: ex_sup_of {x} "/\" D,I by WAYBEL_2:1;
then ex_sup_of xD,I by YELLOW_4:42;
then
A2: sup xD is_>=_than xD by YELLOW_0:def 9;
hereby
set A = the set of all x /\ w where w is Element of D;
let a be object;
ex_sup_of D,I by WAYBEL_0:75;
then sup ({x} "/\" D) <= x "/\" sup D by A1,YELLOW_4:53;
then
A3: sup ({x} "/\" D) c= x "/\" sup D by YELLOW_1:3;
assume a in sup ({x} "/\" D);
then a in x "/\" sup D by A3;
then
A4: a in x /\ sup D by YELLOW_2:43;
then a in sup D by XBOOLE_0:def 4;
then a in union D by Th3;
then consider d being set such that
A5: a in d and
A6: d in D by TARSKI:def 4;
reconsider d as Element of I by A6;
A7: x /\ d in A by A6;
a in x by A4,XBOOLE_0:def 4;
then a in x /\ d by A5,XBOOLE_0:def 4;
hence a in union A by A7,TARSKI:def 4;
end;
let a be object;
assume a in union A;
then consider Z being set such that
A8: a in Z and
A9: Z in A by TARSKI:def 4;
consider d being Element of D such that
A10: Z = x /\ d and
not contradiction by A9;
reconsider d as Element of I;
A11: xD = {x} "/\" D by YELLOW_4:42;
then x "/\" d in {x} "/\" D;
then sup xD >= x "/\" d by A2,A11;
then
A12: x "/\" d c= sup xD by YELLOW_1:3;
x /\ d = x "/\" d by YELLOW_2:43;
then a in sup xD by A12,A8,A10;
hence thesis by YELLOW_4:42;
end;
:: Exercise 4.8 (i), p. 33
registration
let R be Semilattice;
cluster InclPoset Ids R -> satisfying_MC;
coherence
proof
set I = InclPoset Ids R;
let x be Element of I, D be non empty directed Subset of I;
thus x "/\" sup D = x /\ sup D by YELLOW_2:43
.= x /\ union D by Th3
.= union the set of all x /\ d where d is Element of D by Th1
.= sup ({x} "/\" D) by Th4;
end;
end;
registration
let R be 1-element RelStr;
cluster -> trivial for TopAugmentation of R;
coherence
proof
let T be TopAugmentation of R;
the RelStr of T = the RelStr of R by YELLOW_9:def 4;
hence thesis;
end;
end;
theorem
for S being Scott complete TopLattice, T being complete LATTICE, A
being Scott TopAugmentation of T st the RelStr of S = the RelStr of T holds the
TopRelStr of A = the TopRelStr of S
proof
let S be Scott complete TopLattice, T be complete LATTICE, A be Scott
TopAugmentation of T such that
A1: the RelStr of S = the RelStr of T;
A2: the topology of S = sigma S by WAYBEL14:23
.= sigma T by A1,YELLOW_9:52
.= the topology of A by YELLOW_9:51;
the RelStr of A = the RelStr of S by A1,YELLOW_9:def 4;
hence thesis by A2;
end;
theorem
for N being Lawson complete TopLattice, T being complete LATTICE, A
being Lawson correct TopAugmentation of T st the RelStr of N = the RelStr of T
holds the TopRelStr of A = the TopRelStr of N
proof
let N be Lawson complete TopLattice, T be complete LATTICE, A be Lawson
correct TopAugmentation of T such that
A1: the RelStr of N = the RelStr of T;
A2: omega T = omega N by A1,WAYBEL19:3;
set S = the Scott correct TopAugmentation of T;
set l = the lower correct TopAugmentation of T;
A3: the RelStr of l = the RelStr of T by YELLOW_9:def 4;
A4: the RelStr of S = the RelStr of T by YELLOW_9:def 4;
(the topology of S) \/ (the topology of l) c= bool the carrier of N
proof
let a be object;
assume a in (the topology of S) \/ (the topology of l);
then a in the topology of S or a in the topology of l by XBOOLE_0:def 3;
hence thesis by A1,A4,A3;
end;
then reconsider
X = (the topology of S) \/ (the topology of l) as Subset-Family
of N;
reconsider X as Subset-Family of N;
A5: the topology of l = omega T by WAYBEL19:def 2;
(sigma N) \/ (omega N) is prebasis of N by WAYBEL19:def 3;
then
A6: (sigma T) \/ (omega N) is prebasis of N by A1,YELLOW_9:52;
A7: the topology of S = sigma T by YELLOW_9:51;
the carrier of N = (the carrier of S) \/ (the carrier of l) by A1,A4,A3;
then N is Refinement of S, l by A2,A6,A5,A7,YELLOW_9:def 6;
then
A8: the topology of N = UniCl FinMeetCl X by YELLOW_9:56
.= lambda T by A1,A5,A7,WAYBEL19:33
.= the topology of A by WAYBEL19:def 4;
the RelStr of A = the RelStr of N by A1,YELLOW_9:def 4;
hence thesis by A8;
end;
theorem
for N being Lawson complete TopLattice for S being Scott
TopAugmentation of N for A being Subset of N, J being Subset of S st A = J & J
is closed holds A is closed
proof
let N be Lawson complete TopLattice, S be Scott TopAugmentation of N, A be
Subset of N, J be Subset of S such that
A1: A = J;
assume J is closed;
then
A2: [#]S \ J is open;
A3: the RelStr of N = the RelStr of S by YELLOW_9:def 4;
then N is Lawson correct TopAugmentation of S by YELLOW_9:def 4;
hence [#]N \ A is open by A1,A3,A2,WAYBEL19:37;
end;
registration
let A be complete LATTICE;
cluster lambda A -> non empty;
coherence
proof
set S = the Lawson correct TopAugmentation of A;
InclPoset the topology of S is non trivial;
hence thesis by WAYBEL19:def 4;
end;
end;
registration
let S be Scott complete TopLattice;
cluster InclPoset sigma S -> complete non trivial;
coherence;
end;
registration
let N be Lawson complete TopLattice;
cluster InclPoset sigma N -> complete non trivial;
coherence;
cluster InclPoset lambda N -> complete non trivial;
coherence
proof
set S = the Lawson correct TopAugmentation of N;
InclPoset the topology of S is complete non trivial;
hence thesis by WAYBEL19:def 4;
end;
end;
theorem Th8:
for T being non empty reflexive RelStr holds sigma T c= {W\
uparrow F where W, F is Subset of T: W in sigma T & F is finite}
proof
let T be non empty reflexive RelStr;
let s be object;
reconsider ss=s as set by TARSKI:1;
A1: ss\uparrow {}T = s;
assume s in sigma T;
hence thesis by A1;
end;
theorem Th9:
for N being Lawson complete TopLattice holds lambda N = the topology of N
proof
let N be Lawson complete TopLattice;
N is Lawson correct TopAugmentation of N by YELLOW_9:44;
hence thesis by WAYBEL19:def 4;
end;
theorem Th10:
for N being Lawson complete TopLattice holds sigma N c= lambda N
proof
let N be Lawson complete TopLattice;
set Z = {W\uparrow F where W, F is Subset of N: W in sigma N & F is finite};
Z is Basis of N by WAYBEL19:32;
then Z c= the topology of N by TOPS_2:64;
then
A1: Z c= lambda N by Th9;
sigma N c= Z by Th8;
hence thesis by A1;
end;
theorem
for M, N being complete LATTICE st the RelStr of M = the RelStr of N
holds lambda M = lambda N
proof
let M, N be complete LATTICE such that
A1: the RelStr of M = the RelStr of N;
A2: lambda N = UniCl FinMeetCl ((sigma N) \/ (omega N)) by WAYBEL19:33;
A3: lambda M = UniCl FinMeetCl ((sigma M) \/ (omega M)) by WAYBEL19:33;
sigma M = sigma N by A1,YELLOW_9:52;
hence thesis by A1,A3,A2,WAYBEL19:3;
end;
theorem Th12:
for N being Lawson complete TopLattice, X being Subset of N
holds X in lambda N iff X is open
by Th9;
registration
cluster TopSpace-like -> Scott for reflexive 1-element TopRelStr;
coherence
by TDLAT_3:15;
end;
registration
cluster trivial -> Lawson for complete TopLattice;
coherence
proof
let T be complete TopLattice;
assume T is trivial;
then
the carrier of T is 1-element;
then reconsider W = T as 1-element complete TopLattice
by STRUCT_0:def 19;
set N = the Lawson correct TopAugmentation of W;
A1: the RelStr of T = the RelStr of N by YELLOW_9:def 4;
the topology of W = {{}, the carrier of W} by TDLAT_3:def 2;
then the topology of T = the topology of N by A1,TDLAT_3:def 2
.= lambda T by WAYBEL19:def 4
.= UniCl FinMeetCl ((sigma T) \/ (omega T)) by WAYBEL19:33;
then FinMeetCl ((omega T) \/ (sigma T)) is Basis of T by YELLOW_9:22;
hence (omega T) \/ (sigma T) is prebasis of T by YELLOW_9:23;
end;
end;
registration
cluster strict continuous lower-bounded meet-continuous Scott for complete
TopLattice;
existence
proof
set A = the strict 1-element TopLattice;
take A;
thus thesis;
end;
end;
registration
cluster strict continuous compact Hausdorff Lawson for complete TopLattice;
existence
proof
set R = the strict trivial complete TopLattice;
take R;
thus thesis;
end;
end;
scheme
EmptySch { A() -> Scott TopLattice, X() -> set, F(set) -> set }: { F(w)
where w is Element of A(): w in {} } = {} proof
thus { F(w) where w is Element of A(): w in {} } c= {}
proof
let a be object;
assume a in { F(w) where w is Element of A(): w in {} };
then
A1: ex w being Element of A() st a = F(w) & w in {};
assume not a in {};
thus thesis by A1;
end;
thus thesis;
end;
theorem Th13:
for N being meet-continuous LATTICE, A being Subset of N st A is
property(S) holds uparrow A is property(S)
proof
let N be meet-continuous LATTICE, A be Subset of N such that
A1: for D being non empty directed Subset of N st sup D in A ex y being
Element of N st y in D & for x being Element of N st x in D & x >= y holds x in
A;
let D be non empty directed Subset of N;
assume sup D in uparrow A;
then consider a being Element of N such that
A2: a <= sup D and
A3: a in A by WAYBEL_0:def 16;
reconsider aa = {a} as non empty directed Subset of N by WAYBEL_0:5;
a = sup ({a} "/\" D) by A2,WAYBEL_2:52;
then consider y being Element of N such that
A4: y in aa "/\" D and
A5: for x being Element of N st x in aa "/\" D & x >= y holds x in A by A1,A3;
aa "/\" D = {a "/\" d where d is Element of N: d in D} by YELLOW_4:42;
then consider d being Element of N such that
A6: y = a "/\" d and
A7: d in D by A4;
take d;
thus d in D by A7;
let x be Element of N such that
x in D and
A8: x >= d;
d >= y by A6,YELLOW_0:23;
then
A9: x >= y by A8,ORDERS_2:3;
y in A by A4,A5,ORDERS_2:1;
hence thesis by A9,WAYBEL_0:def 16;
end;
registration
let N be meet-continuous LATTICE, A be property(S) Subset of N;
cluster uparrow A -> property(S);
coherence by Th13;
end;
:: Proposition 2.1 (i), p. 153
theorem Th14:
for N being meet-continuous Lawson complete TopLattice, S
being Scott TopAugmentation of N, A being Subset of N st A in lambda N holds
uparrow A in sigma S
proof
let N be meet-continuous Lawson complete TopLattice, S be Scott
TopAugmentation of N, A be Subset of N;
assume A in lambda N;
then
A1: A is open by Th12;
A2: the RelStr of N = the RelStr of S by YELLOW_9:def 4;
then reconsider Y = A as Subset of S;
A3: S is meet-continuous by A2,YELLOW12:14;
reconsider UA = uparrow A as Subset of S by A2;
A4: uparrow A = uparrow Y by A2,WAYBEL_0:13;
Y is property(S) by A1,A2,WAYBEL19:36,YELLOW12:19;
then UA is open by A3,A4,WAYBEL11:15;
then uparrow A in the topology of S;
hence thesis by WAYBEL14:23;
end;
theorem Th15:
for N being meet-continuous Lawson complete TopLattice for S
being Scott TopAugmentation of N for A being Subset of N, J being Subset of S
st A = J holds A is open implies uparrow J is open
proof
let N be meet-continuous Lawson complete TopLattice, S be Scott
TopAugmentation of N, A be Subset of N, J be Subset of S such that
A1: A = J;
assume A is open;
then A in lambda N by Th12;
then
A2: uparrow A in sigma S by Th14;
the RelStr of N = the RelStr of S by YELLOW_9:def 4;
then uparrow J in sigma S by A2,A1,WAYBEL_0:13;
hence thesis by WAYBEL14:24;
end;
theorem Th16:
for N being meet-continuous Lawson complete TopLattice for S
being Scott TopAugmentation of N for x being Point of S, y being Point of N for
J being Basis of y st x = y holds {uparrow A where A is Subset of N: A in J} is
Basis of x
proof
let N be meet-continuous Lawson complete TopLattice, S be Scott
TopAugmentation of N, x be Point of S, y be Point of N, J be Basis of y such
that
A1: x = y;
set Z = {uparrow A where A is Subset of N: A in J};
set K = Z;
A2: the RelStr of N = the RelStr of S by YELLOW_9:def 4;
K c= bool the carrier of S
proof
let k be object;
assume k in K;
then ex A being Subset of N st k = uparrow A & A in J;
hence thesis by A2;
end;
then reconsider K as Subset-Family of S;
K is Basis of x
proof
A3: K is open
proof
let k be Subset of S;
assume k in K;
then consider A being Subset of N such that
A4: k = uparrow A and
A5: A in J;
reconsider A9 = A as Subset of S by A2;
uparrow A9 is open by A5,Th15,YELLOW_8:12;
then uparrow A9 in the topology of S;
then uparrow A in the topology of S by A2,WAYBEL_0:13;
hence thesis by A4;
end;
K is x-quasi_basis
proof
for k being set st k in K holds x in k
proof
let k be set;
assume k in K;
then consider A being Subset of N such that
A6: k = uparrow A and
A7: A in J;
A8: A c= uparrow A by WAYBEL_0:16;
y in Intersect J by YELLOW_8:def 1;
then y in A by A7,SETFAM_1:43;
hence thesis by A8,A1,A6;
end;
hence x in Intersect K by SETFAM_1:43;
let sA be Subset of S such that
A9: sA is open and
A10: x in sA;
sA is upper by A9,WAYBEL11:def 4;
then
A11: uparrow sA c= sA by WAYBEL_0:24;
reconsider lA = sA as Subset of N by A2;
N is Lawson correct TopAugmentation of S by A2,YELLOW_9:def 4;
then lA is open by A9,WAYBEL19:37;
then lA in lambda N by Th12;
then
A12: uparrow lA in sigma S by Th14;
A13: lA c= uparrow lA by WAYBEL_0:16;
sigma N c= lambda N by Th10;
then sigma S c= lambda N by A2,YELLOW_9:52;
then uparrow lA is open by A12,Th12;
then consider lV1 being Subset of N such that
A14: lV1 in J and
A15: lV1 c= uparrow lA by A13,A1,A10,YELLOW_8:def 1;
reconsider sUV = uparrow lV1 as Subset of S by A2;
take sUV;
thus sUV in K by A14;
A16: lV1 is_coarser_than uparrow lA by A15,WAYBEL12:16;
sA c= uparrow sA by WAYBEL_0:16;
then
A17: sA = uparrow sA by A11;
uparrow sA = uparrow lA by A2,WAYBEL_0:13;
hence thesis by A16,A17,YELLOW12:28;
end;
hence thesis by A3;
end;
hence thesis;
end;
:: Proposition 2.1 (ii), p. 153
theorem Th17:
for N being meet-continuous Lawson complete TopLattice for S
being Scott TopAugmentation of N for X being upper Subset of N, Y being Subset
of S st X = Y holds Int X = Int Y
proof
let N be meet-continuous Lawson complete TopLattice, S be Scott
TopAugmentation of N, X be upper Subset of N, Y be Subset of S such that
A1: X = Y;
A2: the RelStr of N = the RelStr of S by YELLOW_9:def 4;
then reconsider K = uparrow Int X as Subset of S;
reconsider sX = Int X as Subset of S by A2;
A3: K c= Y
proof
let a be object;
A4: Int X c= X by TOPS_1:16;
assume
A5: a in K;
then reconsider x = a as Element of N;
A6: X c= uparrow X by WAYBEL_0:16;
uparrow X c= X by WAYBEL_0:24;
then
A7: uparrow X = X by A6;
ex y being Element of N st y <= x & y in Int X by A5,WAYBEL_0:def 16;
hence thesis by A7,A1,A4,WAYBEL_0:def 16;
end;
A8: Int X c= uparrow Int X by WAYBEL_0:16;
uparrow sX is open by Th15;
then K is open by A2,WAYBEL_0:13;
then uparrow Int X c= Int Y by A3,TOPS_1:24;
hence Int X c= Int Y by A8;
reconsider A = Int Y as Subset of N by A2;
N is Lawson correct TopAugmentation of S by A2,YELLOW_9:def 4;
then A is open by WAYBEL19:37;
hence thesis by A1,TOPS_1:16,24;
end;
:: Proposition 2.1 (iii), p. 153
theorem
for N being meet-continuous Lawson complete TopLattice for S being
Scott TopAugmentation of N for X being lower Subset of N, Y being Subset of S
st X = Y holds Cl X = Cl Y
proof
let N be meet-continuous Lawson complete TopLattice, S be Scott
TopAugmentation of N, X be lower Subset of N, Y be Subset of S such that
A1: X = Y;
A2: the RelStr of N = the RelStr of S by YELLOW_9:def 4;
then reconsider A = Cl Y as Subset of N;
(Cl X)` = (Cl X``)` .= Int X` by TOPS_1:def 1
.= Int Y` by A1,A2,Th17
.= (Cl Y``)` by TOPS_1:def 1
.= A` by A2;
hence thesis by TOPS_1:1;
end;
theorem Th19:
for M, N being complete LATTICE, LM being Lawson correct
TopAugmentation of M, LN being Lawson correct TopAugmentation of N st InclPoset
sigma N is continuous holds the topology of [:LM,LN qua TopSpace:] = lambda [:M
,N:]
proof
let M, N be complete LATTICE, LM be Lawson correct TopAugmentation of M, LN
be Lawson correct TopAugmentation of N such that
A1: InclPoset sigma N is continuous;
set SMN = the non empty Scott correct TopAugmentation of [:M,N:];
set lMN = the non empty lower correct TopAugmentation of [:M,N:];
set LMN = the non empty Lawson correct TopAugmentation of [:M,N:];
A2: [:LM,LN qua TopSpace:] = the TopStruct of LMN
proof
set lN = the non empty lower correct TopAugmentation of N;
set lM = the non empty lower correct TopAugmentation of M;
set SN = the non empty Scott correct TopAugmentation of N;
set SM = the non empty Scott correct TopAugmentation of M;
A3: LN is Refinement of SN, lN by WAYBEL19:29;
A4: the RelStr of lN = the RelStr of N by YELLOW_9:def 4;
(omega LMN) \/ (sigma LMN) is prebasis of LMN by WAYBEL19:def 3;
then
A5: (omega LMN) \/ (sigma LMN) is prebasis of the TopStruct of LMN by
YELLOW12:33;
A6: the RelStr of LM = the RelStr of M by YELLOW_9:def 4;
A7: the RelStr of LN = the RelStr of N by YELLOW_9:def 4;
A8: the RelStr of LMN = the RelStr of [:M,N:] by YELLOW_9:def 4;
A9: the carrier of [:LM,LN qua TopSpace:] = [:the carrier of LM,the
carrier of LN:] by BORSUK_1:def 2
.= the carrier of LMN by A6,A7,A8,YELLOW_3:def 2;
A10: the topology of [:lM,lN qua TopSpace:] = omega [:M,N:] by WAYBEL19:15
.= omega LMN by A8,WAYBEL19:3;
A11: the RelStr of SN = the RelStr of N by YELLOW_9:def 4;
the RelStr of SM = the RelStr of M by YELLOW_9:def 4
.= the RelStr of Sigma M by YELLOW_9:def 4;
then
A12: the TopStruct of SM = the TopStruct of Sigma M by WAYBEL29:13;
A13: the RelStr of lM = the RelStr of M by YELLOW_9:def 4;
the RelStr of SN = the RelStr of N by YELLOW_9:def 4
.= the RelStr of Sigma N by YELLOW_9:def 4;
then the TopStruct of SN = the TopStruct of Sigma N by WAYBEL29:13;
then
A14: the topology of [:SM,SN qua TopSpace:] = the topology of [:Sigma M,(
Sigma N) qua TopSpace:] by A12,WAYBEL29:7
.= sigma [:M,N:] by A1,WAYBEL29:30
.= sigma LMN by A8,YELLOW_9:52;
A15: the RelStr of SM = the RelStr of M by YELLOW_9:def 4;
A16: LM is Refinement of SM, lM by WAYBEL19:29;
then
[:LM,LN qua TopSpace:] is Refinement of [:SM,SN qua TopSpace:], [:lM,
lN qua TopSpace:] by A3,A15,A11,A13,A4,YELLOW12:50;
then the carrier of the TopStruct of LMN = (the carrier of [:SM,SN qua
TopSpace:]) \/ (the carrier of [:lM,lN qua TopSpace:]) by A9,YELLOW_9:def 6
;
then
the TopStruct of LMN is Refinement of [:SM,SN qua TopSpace:], [:lM,lN
qua TopSpace:] by A5,A14,A10,YELLOW_9:def 6;
hence thesis by A16,A3,A15,A11,A13,A4,A9,YELLOW12:49;
end;
LMN is Refinement of SMN, lMN by WAYBEL19:29;
then reconsider R = [:LM,LN qua TopSpace:] as Refinement of SMN, lMN by A2,
YELLOW12:47;
the topology of [:LM,LN qua TopSpace:] = the topology of R;
hence thesis by WAYBEL19:34;
end;
:: Proposition 2.2, p. 153
theorem Th20:
for M, N being complete LATTICE, P being Lawson correct
TopAugmentation of [:M,N:], Q being Lawson correct TopAugmentation of M, R
being Lawson correct TopAugmentation of N st InclPoset sigma N is continuous
holds the TopStruct of P = [:Q,R qua TopSpace:]
proof
let M, N be complete LATTICE, P be Lawson correct TopAugmentation of [:M,N:]
, Q be Lawson correct TopAugmentation of M, R be Lawson correct TopAugmentation
of N such that
A1: InclPoset sigma N is continuous;
A2: the topology of P = lambda [:M,N:] by WAYBEL19:def 4
.= the topology of [:Q,R qua TopSpace:] by A1,Th19;
A3: the RelStr of Q = the RelStr of M by YELLOW_9:def 4;
A4: the RelStr of R = the RelStr of N by YELLOW_9:def 4;
the RelStr of P = the RelStr of [:M,N:] by YELLOW_9:def 4;
then the carrier of P = [:the carrier of Q, the carrier of N:] by A3,
YELLOW_3:def 2
.= the carrier of [:Q,R qua TopSpace:] by A4,BORSUK_1:def 2;
hence thesis by A2;
end;
:: Theorem 2.3, p. 153, first conjunct
theorem Th21:
for N being meet-continuous Lawson complete TopLattice, x
being Element of N holds x"/\" is continuous
proof
let N be meet-continuous Lawson complete TopLattice, x be Element of N;
for X being non empty Subset of N holds x"/\" preserves_inf_of X by
YELLOW13:11;
hence thesis by WAYBEL21:45;
end;
registration
let N be meet-continuous Lawson complete TopLattice, x be Element of N;
cluster x"/\" -> continuous;
coherence by Th21;
end;
:: Theorem 2.3, p. 153, second conjunct
theorem Th22:
for N being meet-continuous Lawson complete TopLattice st
InclPoset sigma N is continuous holds N is topological_semilattice
proof
let N be meet-continuous Lawson complete TopLattice such that
A1: InclPoset sigma N is continuous;
set NN = the Lawson correct TopAugmentation of [:N,N:];
N is TopAugmentation of N by YELLOW_9:44;
then
A2: the TopStruct of NN = [:N,N qua TopSpace:] by A1,Th20;
A3: the RelStr of NN = the RelStr of [:N,N:] by YELLOW_9:def 4;
then reconsider h = inf_op N as Function of NN, N;
A4: the RelStr of N = the RelStr of N;
A5: h is directed-sups-preserving
proof
let X be Subset of NN;
assume X is non empty directed;
then reconsider X1 = X as non empty directed Subset of [:N,N:] by A3,
WAYBEL_0:3;
inf_op N preserves_sup_of X1 by WAYBEL_0:def 37;
hence thesis by A3,A4,WAYBEL_0:65;
end;
A6: h is infs-preserving
by A3,WAYBEL_0:def 32,A4,WAYBEL_0:65;
then h is SemilatticeHomomorphism of NN, N by WAYBEL21:5;
then
A7: h is continuous by A5,A6,WAYBEL21:46;
A8: the TopStruct of N = the TopStruct of N;
let g be Function of [:N,N qua TopSpace:], N;
assume g = inf_op N;
hence thesis by A2,A7,A8,YELLOW12:36;
end;
Lm3: now
let S, T, x1, x2 be set such that
A1: x1 in S and
A2: x2 in T;
A3: dom <:pr2(S,T),pr1(S,T):> = dom pr2(S,T) /\ dom pr1(S,T) by FUNCT_3:def 7
.= dom pr2(S,T) /\ [:S,T:] by FUNCT_3:def 4
.= [:S,T:] /\ [:S,T:] by FUNCT_3:def 5
.= [:S,T:];
[x1,x2] in [:S,T:] by A1,A2,ZFMISC_1:87;
hence
<:pr2(S,T),pr1(S,T):>. [x1,x2] = [pr2(S,T).(x1,x2),pr1(S,T).(x1,x2)] by A3,
FUNCT_3:def 7
.= [x2,pr1(S,T).(x1,x2)] by A1,A2,FUNCT_3:def 5
.= [x2,x1] by A1,A2,FUNCT_3:def 4;
end;
:: Proposition 2.4, p. 153
theorem
for N being meet-continuous Lawson complete TopLattice st InclPoset
sigma N is continuous holds N is Hausdorff iff for X being Subset of [:N,N qua
TopSpace:] st X = the InternalRel of N holds X is closed
proof
let N be meet-continuous Lawson complete TopLattice such that
A1: InclPoset sigma N is continuous;
A2: [:the carrier of N,the carrier of N:] = the carrier of [:N,N qua
TopSpace:] by BORSUK_1:def 2;
hereby
reconsider D = id the carrier of N as Subset of [:N,N qua TopSpace:] by
BORSUK_1:def 2;
set INF = inf_op N, f = <:pr1(the carrier of N,the carrier of N),INF:>;
assume N is Hausdorff;
then
A3: D is closed by YELLOW12:46;
A4: the carrier of [:N,N:] = [:the carrier of N,the carrier of N:] by
YELLOW_3:def 2;
then reconsider
f as Function of [:N,N qua TopSpace:], [:N,N qua TopSpace:] by A2,
FUNCT_3:58;
let X be Subset of [:N,N qua TopSpace:] such that
A5: X = the InternalRel of N;
A6: for x, y being Element of N holds f. [x,y] = [x, x "/\" y]
proof
let x, y be Element of N;
A7: dom (pr1(the carrier of N,the carrier of N)) = [:the carrier of N,
the carrier of N:] by FUNCT_2:def 1;
A8: [x,y] in [:the carrier of N,the carrier of N:] by ZFMISC_1:87;
dom INF = [:the carrier of N,the carrier of N:] by A4,FUNCT_2:def 1;
hence
f. [x,y] = [pr1(the carrier of N,the carrier of N).(x,y),INF.(x,y)]
by A8,A7,FUNCT_3:49
.= [x, INF.(x,y)] by FUNCT_3:def 4
.= [x, x "/\" y] by WAYBEL_2:def 4;
end;
A9: X = f"D
proof
hereby
let a be object;
assume
A10: a in X;
then consider s, t being object such that
A11: s in the carrier of N and
A12: t in the carrier of N and
A13: a = [s,t] by A5,ZFMISC_1:def 2;
reconsider s, t as Element of N by A11,A12;
s <= t by A5,A10,A13,ORDERS_2:def 5;
then s "/\" t = s by YELLOW_0:25;
then f. [s,t] = [s,s] by A6;
then
A14: f.a in D by A13,RELAT_1:def 10;
dom f = the carrier of [:N,N qua TopSpace:] by FUNCT_2:def 1;
then a in dom f by A2,A11,A12,A13,ZFMISC_1:87;
hence a in f"D by A14,FUNCT_1:def 7;
end;
let a be object;
assume
A15: a in f"D;
then
A16: f.a in D by FUNCT_1:def 7;
consider s, t being object such that
A17: s in the carrier of N and
A18: t in the carrier of N and
A19: a = [s,t] by A2,A15,ZFMISC_1:def 2;
reconsider s, t as Element of N by A17,A18;
f.a = [s, s "/\" t] by A6,A19;
then s = s "/\" t by A16,RELAT_1:def 10;
then s <= t by YELLOW_0:25;
hence thesis by A5,A19,ORDERS_2:def 5;
end;
reconsider INF as Function of [:N,N qua TopSpace:], N by A2,A4;
N is topological_semilattice by A1,Th22;
then
A20: INF is continuous;
pr1(the carrier of N,the carrier of N) is continuous Function of [:N,
N qua TopSpace:],N by YELLOW12:39;
then f is continuous by A20,YELLOW12:41;
hence X is closed by A9,A3;
end;
assume
A21: for X being Subset of [:N,N qua TopSpace:] st X = the InternalRel
of N holds X is closed;
A22: (the InternalRel of N) /\ the InternalRel of N~ c= id the carrier of N
by YELLOW12:23;
id the carrier of N c= (the InternalRel of N) /\ the InternalRel of N~
by YELLOW12:22;
then
A23: id the carrier of N = (the InternalRel of N) /\ the InternalRel of N~
by A22;
for A being Subset of [:N,N qua TopSpace:] st A = id the carrier of N
holds A is closed
proof
reconsider f = <:pr2(the carrier of N,the carrier of N), pr1(the carrier
of N,the carrier of N):> as continuous Function of [:N,N qua TopSpace:], [:N,N
qua TopSpace:] by YELLOW12:42;
reconsider X = the InternalRel of N, Y = the InternalRel of N~ as Subset
of [:N,N qua TopSpace:] by BORSUK_1:def 2;
let A be Subset of [:N,N qua TopSpace:] such that
A24: A = id the carrier of N;
reconsider X, Y as Subset of [:N,N qua TopSpace:];
A25: X is closed by A21;
A26: dom f = [:the carrier of N,the carrier of N:] by YELLOW12:4;
A27: f.:X = Y
proof
thus f.:X c= Y
proof
let y be object;
assume y in f.:X;
then consider x being object such that
x in dom f and
A28: x in X and
A29: y = f.x by FUNCT_1:def 6;
consider x1, x2 being object such that
A30: x1 in the carrier of N and
A31: x2 in the carrier of N and
A32: x = [x1,x2] by A28,ZFMISC_1:def 2;
f.x = [x2,x1] by A30,A31,A32,Lm3;
hence thesis by A28,A29,A32,RELAT_1:def 7;
end;
let y be object;
assume
A33: y in Y;
then consider y1, y2 being object such that
A34: y1 in the carrier of N and
A35: y2 in the carrier of N and
A36: y = [y1,y2] by ZFMISC_1:def 2;
A37: [y2,y1] in X by A33,A36,RELAT_1:def 7;
f. [y2,y1] = y by A34,A35,A36,Lm3;
hence thesis by A26,A37,FUNCT_1:def 6;
end;
f is being_homeomorphism by YELLOW12:43;
then Y is closed by A25,A27,TOPS_2:58;
hence thesis by A23,A24,A25;
end;
hence thesis by YELLOW12:46;
end;
:: Definition 2.5, p. 154
definition
let N be non empty reflexive RelStr, X be Subset of N;
func X^0 -> Subset of N equals
{ u where u is Element of N : for D being non
empty directed Subset of N st u <= sup D holds X meets D };
coherence
proof
defpred P[Element of N] means for D being non empty directed Subset of N
st $1 <= sup D holds X meets D;
thus {u where u is Element of N: P[u]} is Subset of N from DOMAIN_1:sch 7;
end;
end;
registration
let N be non empty reflexive antisymmetric RelStr, X be empty Subset of N;
cluster X^0 -> empty;
coherence
proof
X^0 c= {}
proof
let a be object such that
A1: a in X^0 and
not a in {};
consider u being Element of N such that
a = u and
A2: for D being non empty directed Subset of N st u <= sup D holds X
meets D by A1;
reconsider D = {u} as non empty directed Subset of N by WAYBEL_0:5;
A3: X misses D;
u <= sup D by YELLOW_0:39;
hence contradiction by A3,A2;
end;
hence thesis;
end;
end;
theorem
for N being non empty reflexive RelStr, A, J being Subset of N st A c=
J holds A^0 c= J^0
proof
let N be non empty reflexive RelStr, A, J be Subset of N such that
A1: A c= J;
let a be object;
assume a in A^0;
then consider u being Element of N such that
A2: a = u and
A3: for D being non empty directed Subset of N st u <= sup D holds A meets D;
for D being non empty directed Subset of N st u <= sup D holds J meets D
by A1,A3,XBOOLE_1:63;
hence thesis by A2;
end;
:: Remark 2.6 (i), p. 154
theorem Th25:
for N being non empty reflexive RelStr, x being Element of N
holds (uparrow x)^0 = wayabove x
proof
let N be non empty reflexive RelStr, x be Element of N;
thus (uparrow x)^0 c= wayabove x
proof
let a be object;
assume a in (uparrow x)^0;
then consider u being Element of N such that
A1: a = u and
A2: for D being non empty directed Subset of N st u <= sup D holds (
uparrow x) meets D;
u >> x
proof
let D be non empty directed Subset of N;
assume u <= sup D;
then (uparrow x) meets D by A2;
then consider d being object such that
A3: d in (uparrow x) /\ D by XBOOLE_0:4;
reconsider d as Element of N by A3;
take d;
thus d in D by A3,XBOOLE_0:def 4;
d in uparrow x by A3,XBOOLE_0:def 4;
hence thesis by WAYBEL_0:18;
end;
hence thesis by A1;
end;
let a be object;
assume
A4: a in wayabove x;
then reconsider b = a as Element of N;
now
A5: b >> x by A4,WAYBEL_3:8;
let D be non empty directed Subset of N;
assume b <= sup D;
then consider d being Element of N such that
A6: d in D and
A7: x <= d by A5;
d in uparrow x by A7,WAYBEL_0:18;
hence (uparrow x) meets D by A6,XBOOLE_0:3;
end;
hence thesis;
end;
:: Remark 2.6 (ii), p. 154
theorem Th26:
for N being Scott TopLattice, X being upper Subset of N holds Int X c= X^0
proof
let N be Scott TopLattice, X be upper Subset of N;
let x be object;
assume
A1: x in Int X;
then reconsider y = x as Element of N;
now
A2: Int X is upper inaccessible by WAYBEL11:def 4;
let D be non empty directed Subset of N;
assume y <= sup D;
then sup D in Int X by A2,A1;
then D meets Int X by A2;
hence X meets D by TOPS_1:16,XBOOLE_1:63;
end;
hence thesis;
end;
:: Lemma 2.7 (i), p. 154
theorem Th27:
for N being non empty reflexive RelStr, X, Y being Subset of N
holds (X^0) \/ (Y^0) c= (X \/ Y)^0
proof
let N be non empty reflexive RelStr, X, Y be Subset of N;
let a be object;
assume
A1: a in (X^0) \/ (Y^0);
then reconsider b = a as Element of N;
now
let D be non empty directed Subset of N such that
A2: b <= sup D;
now
per cases by A1,XBOOLE_0:def 3;
suppose
a in X^0;
then ex x being Element of N st a = x & for D being
non empty directed Subset of N st x <= sup D holds X meets D;
then X meets D by A2;
then X /\ D <> {};
then X /\ D \/ Y /\ D <> {};
hence (X \/ Y) /\ D <> {} by XBOOLE_1:23;
end;
suppose
a in Y^0;
then ex y being Element of N st a = y & for D being
non empty directed Subset of N st y <= sup D holds Y meets D;
then Y meets D by A2;
then Y /\ D <> {};
then X /\ D \/ Y /\ D <> {};
hence (X \/ Y) /\ D <> {} by XBOOLE_1:23;
end;
end;
hence (X \/ Y) meets D;
end;
hence thesis;
end;
:: Lemma 2.7 (ii), p. 154
theorem Th28:
for N being meet-continuous LATTICE, X, Y being upper Subset of
N holds (X^0) \/ (Y^0) = (X \/ Y)^0
proof
let N be meet-continuous LATTICE, X, Y be upper Subset of N;
thus (X^0) \/ (Y^0) c= (X \/ Y)^0 by Th27;
assume not (X \/ Y)^0 c= (X^0) \/ (Y^0);
then consider s being object such that
A1: s in (X \/ Y)^0 and
A2: not s in (X^0) \/ (Y^0);
A3: not s in X^0 by A2,XBOOLE_0:def 3;
A4: not s in Y^0 by A2,XBOOLE_0:def 3;
reconsider s as Element of N by A1;
consider D being non empty directed Subset of N such that
A5: s <= sup D and
A6: X misses D by A3;
consider E being non empty directed Subset of N such that
A7: s <= sup E and
A8: Y misses E by A4;
s "/\" s = s by YELLOW_0:25;
then s <= (sup D) "/\" (sup E) by A5,A7,YELLOW_3:2;
then
A9: s <= sup (D "/\" E) by WAYBEL_2:51;
ex xy being Element of N st s = xy & for D being non
empty directed Subset of N st xy <= sup D holds (X \/ Y) meets D by A1;
then (X \/ Y) meets (D"/\"E) by A9;
then
A10: (X \/ Y) /\ (D"/\"E) <> {};
X misses (D "/\" E) by A6,YELLOW12:21;
then
A11: X /\ (D "/\" E) = {};
Y misses (D "/\" E) by A8,YELLOW12:21;
then X /\ (D"/\"E) \/ Y /\ (D"/\"E) = {} by A11;
hence contradiction by A10,XBOOLE_1:23;
end;
:: Lemma 2.8, p. 154
theorem Th29:
for S being meet-continuous Scott TopLattice, F being finite
Subset of S holds Int uparrow F c= union { wayabove x where x is Element of S :
x in F }
proof
let S be meet-continuous Scott TopLattice, F be finite Subset of S;
defpred P[set] means ex UU being Subset-Family of S st UU = {uparrow x where
x is Element of S : x in $1} & (union UU)^0 = union { (uparrow x)^0 where x is
Element of S : x in $1 };
A1: for b, J being set st b in F & J c= F & P[J] holds P[J \/ {b}]
proof
let b, J be set;
assume that
A2: b in F and
J c= F;
reconsider bb = b as Element of S by A2;
A3: (union {(uparrow x)^0 where x is Element of S : x in J}) \/ ((uparrow
bb)^0) = union {(uparrow x)^0 where x is Element of S : x in J \/ {b}}
proof
{(uparrow x)^0 where x is Element of S : x in J} c= {(uparrow x)^0
where x is Element of S : x in J \/ {b}}
proof
let a be object;
assume a in {(uparrow x)^0 where x is Element of S : x in J};
then
A4: ex y being Element of S st a = (uparrow y)^0 & y in J;
J c= J \/ {b} by XBOOLE_1:7;
hence thesis by A4;
end;
then
A5: union {(uparrow x)^0 where x is Element of S : x in J} c= union {(
uparrow x)^0 where x is Element of S : x in J \/ {b}} by ZFMISC_1:77;
A6: {b} c= J \/ {b} by XBOOLE_1:7;
b in {b} by TARSKI:def 1;
then (uparrow bb)^0 in {(uparrow x)^0 where x is Element of S : x in J
\/ {b}} by A6;
then (uparrow bb)^0 c= union {(uparrow x)^0 where x is Element of S : x
in J \/ {b}} by ZFMISC_1:74;
hence (union {(uparrow x)^0 where x is Element of S : x in J}) \/ ((
uparrow bb)^0) c= union {(uparrow x)^0 where x is Element of S : x in J \/ {b}}
by A5,XBOOLE_1:8;
let a be object;
assume
a in union {(uparrow x)^0 where x is Element of S : x in J \/ { b}};
then consider A being set such that
A7: a in A and
A8: A in {(uparrow x)^0 where x is Element of S : x in J \/ {b}} by
TARSKI:def 4;
consider y being Element of S such that
A9: A = (uparrow y)^0 and
A10: y in J \/ {b} by A8;
per cases by A10,XBOOLE_0:def 3;
suppose
y in J;
then
(uparrow y)^0 in {(uparrow x)^0 where x is Element of S : x in J};
then
A11: a in union {(uparrow x)^0 where x is Element of S : x in J } by A7,A9,
TARSKI:def 4;
union {(uparrow x)^0 where x is Element of S : x in J} c= (union
{(uparrow x)^0 where x is Element of S : x in J}) \/ ((uparrow bb)^0) by
XBOOLE_1:7;
hence thesis by A11;
end;
suppose
A12: y in {b};
A13: (uparrow bb)^0 c= (union {(uparrow x)^0 where x is Element of S :
x in J}) \/ ((uparrow bb)^0) by XBOOLE_1:7;
y = b by A12,TARSKI:def 1;
hence thesis by A13,A7,A9;
end;
end;
assume P[J];
then consider UU being Subset-Family of S such that
A14: UU = {uparrow x where x is Element of S : x in J} and
A15: (union UU)^0 = union {(uparrow x)^0 where x is Element of S : x in J};
reconsider I = UU \/ {uparrow bb} as Subset-Family of S;
take I;
thus I = {uparrow x where x is Element of S : x in J \/ {b}}
proof
thus I c= {uparrow x where x is Element of S : x in J \/ {b}}
proof
let a be object such that
A16: a in I;
per cases by A16,XBOOLE_0:def 3;
suppose
A17: a in UU;
A18: J c= J \/ {b} by XBOOLE_1:7;
ex x being Element of S st a = uparrow x & x in J by A17,A14;
hence thesis by A18;
end;
suppose
A19: a in {uparrow bb};
A20: b in {b} by TARSKI:def 1;
A21: {b} c= J \/ {b} by XBOOLE_1:7;
a = uparrow bb by A19,TARSKI:def 1;
hence thesis by A20,A21;
end;
end;
let a be object;
assume a in {uparrow x where x is Element of S : x in J \/ {b}};
then consider x being Element of S such that
A22: a = uparrow x and
A23: x in J \/ {b};
per cases by A23,XBOOLE_0:def 3;
suppose
A24: x in J;
A25: UU c= UU \/ {uparrow bb} by XBOOLE_1:7;
uparrow x in UU by A24,A14;
hence thesis by A25,A22;
end;
suppose
A26: x in {b};
A27: {uparrow bb} c= UU \/ {uparrow bb} by XBOOLE_1:7;
A28: a in {uparrow x} by A22,TARSKI:def 1;
x = b by A26,TARSKI:def 1;
hence thesis by A27,A28;
end;
end;
A29: (union UU) \/ uparrow bb = union I
proof
thus (union UU) \/ uparrow bb c= union I
proof
let a be object such that
A30: a in (union UU) \/ uparrow bb;
per cases by A30,XBOOLE_0:def 3;
suppose
A31: a in union UU;
A32: UU c= I by XBOOLE_1:7;
ex A being set st a in A & A in UU by A31,TARSKI:def 4;
hence thesis by A32,TARSKI:def 4;
end;
suppose
A33: a in uparrow bb;
A34: uparrow bb in {uparrow bb} by TARSKI:def 1;
{uparrow bb} c= UU \/ {uparrow bb} by XBOOLE_1:7;
hence thesis by A34,A33,TARSKI:def 4;
end;
end;
let a be object;
assume a in union I;
then consider A being set such that
A35: a in A and
A36: A in I by TARSKI:def 4;
per cases by A36,XBOOLE_0:def 3;
suppose
A in UU;
then A c= union UU by ZFMISC_1:74;
then
A37: a in union UU by A35;
union UU c= (union UU) \/ uparrow bb by XBOOLE_1:7;
hence thesis by A37;
end;
suppose
A38: A in {uparrow bb};
A39: uparrow bb c= (union UU) \/ uparrow bb by XBOOLE_1:7;
A = uparrow bb by A38,TARSKI:def 1;
hence thesis by A39,A35;
end;
end;
for X being Subset of S st X in UU holds X is upper
proof
let X be Subset of S;
assume X in UU;
then ex x being Element of S st X = uparrow x & x in J by A14;
hence thesis;
end;
then union UU is upper by WAYBEL_0:28;
hence thesis by A3,A15,A29,Th28;
end;
A40: P[{}]
proof
deffunc F(Element of S) = (uparrow $1)^0;
reconsider UU = {} as Subset-Family of S by XBOOLE_1:2;
take UU;
reconsider K = union UU as empty Subset of S;
A41: K^0 is empty;
thus UU = {uparrow x where x is Element of S : x in {}}
proof
deffunc F(Element of S) = uparrow $1;
{F(x) where x is Element of S : x in {}} = {} from EmptySch;
hence thesis;
end;
{F(x) where x is Element of S : x in {}} = {} from EmptySch;
hence thesis by A41;
end;
A42: {(uparrow x)^0 where x is Element of S : x in F} = {wayabove x where x
is Element of S : x in F}
proof
thus {(uparrow x)^0 where x is Element of S : x in F} c= {wayabove x where
x is Element of S : x in F}
proof
let a be object;
assume a in {(uparrow x)^0 where x is Element of S : x in F};
then consider x being Element of S such that
A43: a = (uparrow x)^0 and
A44: x in F;
(uparrow x)^0 = wayabove x by Th25;
hence thesis by A43,A44;
end;
let a be object;
assume a in {wayabove x where x is Element of S : x in F};
then consider x being Element of S such that
A45: a = wayabove x and
A46: x in F;
(uparrow x)^0 = wayabove x by Th25;
hence thesis by A45,A46;
end;
A47: F is finite;
P[F] from FINSET_1:sch 2(A47,A40,A1);
then (uparrow F)^0 = union {wayabove x where x is Element of S : x in F} by
A42,YELLOW_9:4;
hence thesis by Th26;
end;
:: Theorem 2.9, p. 154
theorem Th30:
for N being Lawson complete TopLattice holds N is continuous
iff N is meet-continuous Hausdorff
proof
let N be Lawson complete TopLattice;
thus N is continuous implies N is meet-continuous Hausdorff;
assume
A1: N is meet-continuous Hausdorff;
thus
A2: for x being Element of N holds waybelow x is non empty directed;
thus N is up-complete;
for x, y being Element of N st not x <= y ex u being Element of N st u
<< x & not u <= y
proof
reconsider J = {O\uparrow F where O, F is Subset of N: O in sigma N & F is
finite} as Basis of N by WAYBEL19:32;
set S = the Scott TopAugmentation of N;
A3: for N being Semilattice, x, y being Element of N st ex u being
Element of N st u << x & not u <= x "/\" y ex u being Element of N st u << x &
not u <= y
proof
let N be Semilattice, x, y be Element of N;
given u being Element of N such that
A4: u << x and
A5: not u <= x "/\" y;
take u;
thus u << x by A4;
assume
A6: u <= y;
u <= x by A4,WAYBEL_3:1;
then u "/\" u <= x "/\" y by A6,YELLOW_3:2;
hence contradiction by A5,YELLOW_0:25;
end;
let x, y be Element of N;
assume not x <= y;
then x "/\" y <> x by YELLOW_0:23;
then consider W, V being Subset of N such that
A7: W is open and
A8: V is open and
A9: x in W and
A10: x "/\" y in V and
A11: W misses V by A1;
V = union {G where G is Subset of N: G in J & G c= V} by A8,YELLOW_8:9;
then consider K being set such that
A12: x "/\" y in K and
A13: K in {G where G is Subset of N: G in J & G c= V} by A10,TARSKI:def 4;
consider V1 being Subset of N such that
A14: K = V1 and
A15: V1 in J and
A16: V1 c= V by A13;
consider U2, F being Subset of N such that
A17: V1 = U2\uparrow F and
A18: U2 in sigma N and
A19: F is finite by A15;
A20: the RelStr of S = the RelStr of N by YELLOW_9:def 4;
then reconsider x1 = x, y1 = y as Element of S;
A21: ex_inf_of {x1,y1},S by YELLOW_0:21;
reconsider U1 = U2 as Subset of S by A20;
reconsider WU1 = W /\ U2 as Subset of N;
reconsider W1 = WU1 as Subset of S by A20;
A22: uparrow W1 = uparrow WU1 by A20,WAYBEL_0:13;
U2 in sigma S by A20,A18,YELLOW_9:52;
then
A23: U1 is open by WAYBEL14:24;
then
A24: U1 is upper by WAYBEL11:def 4;
WU1 c= uparrow F
proof
A25: W misses V1 by A11,A16,XBOOLE_1:63;
A26: WU1 \ uparrow F c= U1 \ uparrow F by XBOOLE_1:17,33;
let w be object;
assume that
A27: w in WU1 and
A28: not w in uparrow F;
A29: w in W by A27,XBOOLE_0:def 4;
w in WU1 \ uparrow F by A27,A28,XBOOLE_0:def 5;
hence contradiction by A26,A17,A29,A25,XBOOLE_0:3;
end;
then WU1 is_coarser_than uparrow F by WAYBEL12:16;
then
A30: uparrow WU1 c= uparrow F by YELLOW12:28;
A31: x1 "/\" y1 <= x1 by YELLOW_0:23;
x "/\" y = inf {x,y} by YELLOW_0:40
.= "/\"({x1,y1},S) by A20,A21,YELLOW_0:27
.= x1 "/\" y1 by YELLOW_0:40;
then x1 "/\" y1 in U1 by A12,A14,A17,XBOOLE_0:def 5;
then x1 in U1 by A24,A31;
then
A32: x in W1 by A9,XBOOLE_0:def 4;
W1 c= uparrow W1 by WAYBEL_0:16;
then
A33: x in uparrow W1 by A32;
reconsider F1 = F as finite Subset of S by A20,A19;
A34: uparrow F1 = uparrow F by A20,WAYBEL_0:13;
N is Lawson correct TopAugmentation of S by A20,YELLOW_9:def 4;
then U2 is open by A23,WAYBEL19:37;
then uparrow W1 c= Int uparrow F1 by A7,A1,A30,A22,A34,Th15,TOPS_1:24;
then
A35: x in Int uparrow F1 by A33;
S is meet-continuous by A1,A20,YELLOW12:14;
then Int uparrow F1 c= union { wayabove u where u is Element of S : u in
F1 } by Th29;
then consider A being set such that
A36: x in A and
A37: A in { wayabove u where u is Element of S : u in F1 } by A35,TARSKI:def 4;
consider u being Element of S such that
A38: A = wayabove u and
A39: u in F1 by A37;
reconsider u1 = u as Element of N by A20;
A40: wayabove u1 = wayabove u by A20,YELLOW12:13;
now
take u1;
thus u1 << x by A36,A38,A40,WAYBEL_3:8;
uparrow u1 c= uparrow F by A39,YELLOW12:30;
then not x "/\" y in uparrow u1 by A12,A14,A17,XBOOLE_0:def 5;
hence not u1 <= x "/\" y by WAYBEL_0:18;
end;
then consider u2 being Element of N such that
A41: u2 << x and
A42: not u2 <= y by A3;
take u2;
thus thesis by A41,A42;
end;
hence thesis by A2,WAYBEL_3:24;
end;
registration
cluster continuous Lawson -> Hausdorff for complete TopLattice;
coherence;
cluster meet-continuous Lawson Hausdorff -> continuous for
complete TopLattice;
coherence by Th30;
end;
:: Definition 2.10, p. 155
definition
let N be non empty TopRelStr;
attr N is with_small_semilattices means
for x being Point of N ex J being
basis of x st for A being Subset of N st A in J holds subrelstr A is
meet-inheriting;
attr N is with_compact_semilattices means
for x being Point of N ex J being
basis of x st for A being Subset of N st A in J holds subrelstr A is
meet-inheriting & A is compact;
attr N is with_open_semilattices means
:Def4:
for x being Point of N ex J
being Basis of x st for A being Subset of N st A in J holds subrelstr A is
meet-inheriting;
end;
registration
cluster with_open_semilattices -> with_small_semilattices for non empty
TopSpace-like TopRelStr;
coherence
proof
let N be non empty TopSpace-like TopRelStr;
assume
A1: for x being Point of N ex J being Basis of x st for A being Subset
of N st A in J holds subrelstr A is meet-inheriting;
let x be Point of N;
consider J being Basis of x such that
A2: for A being Subset of N st A in J holds subrelstr A is
meet-inheriting by A1;
reconsider J as basis of x by YELLOW13:23;
take J;
thus thesis by A2;
end;
cluster with_compact_semilattices -> with_small_semilattices for non empty
TopSpace-like TopRelStr;
coherence
proof
let N be non empty TopSpace-like TopRelStr;
assume
A3: for x being Point of N ex J being basis of x st for A being Subset
of N st A in J holds subrelstr A is meet-inheriting & A is compact;
let x be Point of N;
consider J being basis of x such that
A4: for A being Subset of N st A in J holds subrelstr A is
meet-inheriting & A is compact by A3;
take J;
thus thesis by A4;
end;
cluster anti-discrete -> with_small_semilattices with_open_semilattices for
non
empty TopRelStr;
coherence
proof
let T be non empty TopRelStr;
assume T is anti-discrete;
then reconsider W = T as anti-discrete non empty TopRelStr;
set J = {the carrier of W};
A5: now
let A be Subset of W;
A6: subrelstr [#]W is infs-inheriting;
assume A in J;
then reconsider
K = subrelstr A as infs-inheriting SubRelStr of T by A6,TARSKI:def 1;
K is meet-inheriting;
hence subrelstr A is meet-inheriting;
end;
A7: W is with_open_semilattices
proof
let x be Point of W;
reconsider J as Basis of x by YELLOW13:13;
take J;
let A be Subset of W;
assume A in J;
hence thesis by A5;
end;
W is with_small_semilattices
proof
let x be Point of W;
reconsider J as basis of x by YELLOW13:21;
take J;
let A be Subset of W;
assume A in J;
hence thesis by A5;
end;
hence thesis by A7;
end;
cluster reflexive TopSpace-like -> with_compact_semilattices
for 1-element TopRelStr;
coherence
proof
let T be 1-element TopRelStr;
assume T is reflexive TopSpace-like;
then reconsider W = T as reflexive 1-element TopSpace-like TopRelStr;
W is with_compact_semilattices
proof
let x be Point of W;
reconsider J = {the carrier of W} as basis of x by YELLOW13:21;
take J;
let A be Subset of W;
assume
A8: A in J;
subrelstr [#]W is infs-inheriting;
then reconsider K = subrelstr A as infs-inheriting SubRelStr of T by A8,
TARSKI:def 1;
K is meet-inheriting;
hence subrelstr A is meet-inheriting;
A = [#]W by A8,TARSKI:def 1;
hence thesis;
end;
hence thesis;
end;
end;
registration
cluster strict trivial lower for TopLattice;
existence
proof
set T = the strict 1-element TopLattice;
take T;
thus thesis;
end;
end;
theorem Th31:
for N being topological_semilattice with_infima TopPoset, C
being Subset of N st subrelstr C is meet-inheriting holds subrelstr Cl C is
meet-inheriting
proof
let N be topological_semilattice with_infima TopPoset, C be Subset of N
such that
A1: subrelstr C is meet-inheriting;
set A = Cl C, S = subrelstr A;
let x, y be Element of N such that
A2: x in the carrier of S and
A3: y in the carrier of S and
ex_inf_of {x,y},N;
A4: the carrier of S = A by YELLOW_0:def 15;
for V being a_neighborhood of x "/\" y holds V meets C
proof
set NN = [:N,N qua TopSpace:];
let V be a_neighborhood of x "/\" y;
A5: the carrier of NN = [:the carrier of N,the carrier of N:] by BORSUK_1:def 2
;
then reconsider xy = [x,y] as Point of NN by YELLOW_3:def 2;
the carrier of [:N,N:] = [:the carrier of N,the carrier of N:] by
YELLOW_3:def 2;
then reconsider f = inf_op N as Function of NN, N by A5;
A6: f.xy = f.(x,y) .= x "/\" y by WAYBEL_2:def 4;
f is continuous by YELLOW13:def 5;
then consider H being a_neighborhood of xy such that
A7: f.:H c= V by A6,BORSUK_1:def 1;
consider A being Subset-Family of NN such that
A8: Int H = union A and
A9: for e being set st e in A ex X1, Y1 being Subset of N st e = [:X1
,Y1:] & X1 is open & Y1 is open by BORSUK_1:5;
xy in union A by A8,CONNSP_2:def 1;
then consider K being set such that
A10: xy in K and
A11: K in A by TARSKI:def 4;
consider Ix, Iy being Subset of N such that
A12: K = [:Ix,Iy:] and
A13: Ix is open and
A14: Iy is open by A9,A11;
A15: x in Ix by A10,A12,ZFMISC_1:87;
A16: y in Iy by A10,A12,ZFMISC_1:87;
A17: Ix = Int Ix by A13,TOPS_1:23;
Iy = Int Iy by A14,TOPS_1:23;
then reconsider Iy as a_neighborhood of y by A16,CONNSP_2:def 1;
Iy meets C by A3,A4,CONNSP_2:27;
then consider iy being object such that
A18: iy in Iy and
A19: iy in C by XBOOLE_0:3;
reconsider Ix as a_neighborhood of x by A15,A17,CONNSP_2:def 1;
Ix meets C by A2,A4,CONNSP_2:27;
then consider ix being object such that
A20: ix in Ix and
A21: ix in C by XBOOLE_0:3;
reconsider ix, iy as Element of N by A20,A18;
now
[ix,iy] in K by A12,A20,A18,ZFMISC_1:87;
then
A22: [ix,iy] in Int H by A8,A11,TARSKI:def 4;
take a = ix "/\" iy;
A23: dom f = the carrier of [:N,N:] by FUNCT_2:def 1;
A24: Int H c= H by TOPS_1:16;
f.(ix,iy) = ix "/\" iy by WAYBEL_2:def 4;
then ix "/\" iy in f.:H by A24,A23,A22,FUNCT_1:def 6;
hence a in V by A7;
A25: ex_inf_of {ix,iy},N by YELLOW_0:21;
the carrier of subrelstr C = C by YELLOW_0:def 15;
then inf{ix,iy} in C by A25,A1,A21,A19;
hence a in C by YELLOW_0:40;
end;
hence thesis by XBOOLE_0:3;
end;
then x "/\" y in Cl C by CONNSP_2:27;
hence thesis by A4,YELLOW_0:40;
end;
:: Theorem 2.11, p. 155
theorem Th32:
for N being meet-continuous Lawson complete TopLattice for S
being Scott TopAugmentation of N holds (for x being Point of S ex J being Basis
of x st for W being Subset of S st W in J holds W is Filter of S) iff N is
with_open_semilattices
proof
let N be meet-continuous Lawson complete TopLattice, S be Scott
TopAugmentation of N;
A1: the RelStr of N = the RelStr of S by YELLOW_9:def 4;
hereby
assume
A2: for x being Point of S ex J being Basis of x st for W being Subset
of S st W in J holds W is Filter of S;
thus N is with_open_semilattices
proof
let x be Point of N;
defpred P[set] means ex U1 being Filter of N, F being finite Subset of N
, W1 being Subset of N st $1 = W1 & U1 \ uparrow F = $1 & x in $1 & W1 is open;
consider SF being Subset-Family of N such that
A3: for W being Subset of N holds W in SF iff P[W] from SUBSET_1:
sch 3;
reconsider SF as Subset-Family of N;
A4: now
reconsider BL = {O\uparrow F where O, F is Subset of N: O in sigma N &
F is finite} as Basis of N by WAYBEL19:32;
A5: BL c= the topology of N by TOPS_2:64;
reconsider y = x as Point of S by A1;
let W be Subset of N such that
A6: W is open and
A7: x in W;
consider By being Basis of y such that
A8: for A being Subset of S st A in By holds A is Filter of S by A2;
W = union { G where G is Subset of N: G in BL & G c= W } by A6,
YELLOW_8:9;
then consider K being set such that
A9: x in K and
A10: K in { G where G is Subset of N: G in BL & G c= W } by A7,TARSKI:def 4;
consider G being Subset of N such that
A11: K = G and
A12: G in BL and
A13: G c= W by A10;
consider V, F being Subset of N such that
A14: G = V \ uparrow F and
A15: V in sigma N and
A16: F is finite by A12;
reconsider F as finite Subset of N by A16;
A17: not x in uparrow F by A9,A11,A14,XBOOLE_0:def 5;
reconsider V as Subset of S by A1;
A18: y in V by A9,A11,A14,XBOOLE_0:def 5;
A19: sigma N = sigma S by A1,YELLOW_9:52;
then V is open by A15,WAYBEL14:24;
then consider U1 being Subset of S such that
A20: U1 in By and
A21: U1 c= V by A18,YELLOW_8:13;
reconsider U2 = U1 as Subset of N by A1;
U1 is Filter of S by A8,A20;
then reconsider U2 as Filter of N by A1,WAYBEL_0:4,25;
U2 \ uparrow F is Subset of N;
then reconsider IT = U1 \ uparrow F as Subset of N;
take U2, F, IT;
thus IT = U2 \ uparrow F;
y in U1 by A20,YELLOW_8:12;
hence x in IT by A17,XBOOLE_0:def 5;
U1 is open by A20,YELLOW_8:12;
then U1 in sigma S by WAYBEL14:24;
then IT in BL by A19;
hence IT is open by A5;
IT c= G by A14,A21,XBOOLE_1:33;
hence IT c= W by A13;
end;
SF is Basis of x
proof
A22: SF is open
proof
let a be Subset of N;
assume
A23: a in SF;
reconsider W = a as Subset of N;
ex U1 being Filter of N, F being finite Subset of
N, W1 being Subset of N st W1 = W & U1 \ uparrow F = W & x in W & W1 is
open by A3,A23;
hence thesis;
end;
SF is x-quasi_basis
proof
for a being set st a in SF holds x in a
proof
let a be set;
assume
A24: a in SF;
then reconsider W = a as Subset of N;
ex U1 being Filter of N, F being finite Subset of
N, W1 being Subset of N st W1 = W & U1 \ uparrow F = W & x in W & W1 is
open by A3,A24;
hence thesis;
end;
hence x in Intersect SF by SETFAM_1:43;
let W be Subset of N;
assume that
A25: W is open and
A26: x in W;
consider U2 being Filter of N, F being finite Subset of N, IT being
Subset of N such that
A27: IT = U2 \ uparrow F and
A28: x in IT and
A29: IT is open and
A30: IT c= W by A25,A26,A4;
take IT;
thus thesis by A3,A27,A28,A29,A30;
end;
hence thesis by A22;
end;
then reconsider SF as Basis of x;
take SF;
let W be Subset of N;
assume W in SF;
then consider U1 being Filter of N, F being finite Subset of N, W1 being
Subset of N such that
W1 = W and
A31: U1 \ uparrow F = W and
x in W and
W1 is open by A3;
set SW = subrelstr W;
thus SW is meet-inheriting
proof
let a, b be Element of N such that
A32: a in the carrier of SW and
A33: b in the carrier of SW and
ex_inf_of {a,b},N;
A34: the carrier of SW = W by YELLOW_0:def 15;
then
A35: b in U1 by A31,A33,XBOOLE_0:def 5;
A36: not a in uparrow F by A34,A31,A32,XBOOLE_0:def 5;
for y being Element of N st y <= a "/\" b holds not y in F
proof
A37: a "/\" b <= a by YELLOW_0:23;
let y be Element of N;
assume y <= a "/\" b;
then y <= a by A37,ORDERS_2:3;
hence thesis by A36,WAYBEL_0:def 16;
end;
then
A38: not a "/\" b in uparrow F by WAYBEL_0:def 16;
a in U1 by A34,A31,A32,XBOOLE_0:def 5;
then consider z being Element of N such that
A39: z in U1 and
A40: z <= a and
A41: z <= b by A35,WAYBEL_0:def 2;
z "/\" z <= a "/\" b by A40,A41,YELLOW_3:2;
then z <= a "/\" b by YELLOW_0:25;
then a "/\" b in U1 by A39,WAYBEL_0:def 20;
then a "/\" b in W by A38,A31,XBOOLE_0:def 5;
hence thesis by A34,YELLOW_0:40;
end;
end;
end;
assume
A42: N is with_open_semilattices;
let x be Point of S;
reconsider y = x as Point of N by A1;
consider J being Basis of y such that
A43: for A being Subset of N st A in J holds subrelstr A is
meet-inheriting by A42;
reconsider J9 = {uparrow A where A is Subset of N: A in J} as Basis of x by
Th16;
take J9;
let W be Subset of S;
assume W in J9;
then consider V being Subset of N such that
A44: W = uparrow V and
A45: V in J;
subrelstr V is meet-inheriting by A43,A45;
then
A46: V is filtered by YELLOW12:26;
x in V by A45,YELLOW_8:12;
hence thesis by A46,A1,A44,WAYBEL_0:4,25;
end;
:: Theorem 2.12, p. 155, r => l
theorem Th33:
for N being Lawson complete TopLattice for S being Scott
TopAugmentation of N for x being Element of N holds {inf A where A is Subset of
S: x in A & A in sigma S} c= {inf J where J is Subset of N : x in J & J in
lambda N}
proof
let N be Lawson complete TopLattice, S be Scott TopAugmentation of N, x be
Element of N;
set s = {inf A where A is Subset of S : x in A & A in sigma S};
let k be object;
assume k in s;
then consider J being Subset of S such that
A1: k = inf J and
A2: x in J and
A3: J in sigma S;
A4: the RelStr of N = the RelStr of S by YELLOW_9:def 4;
then reconsider A = J as Subset of N;
sigma N c= lambda N by Th10;
then
A5: sigma S c= lambda N by A4,YELLOW_9:52;
inf A = inf J by A4,YELLOW_0:17,27;
hence thesis by A5,A1,A2,A3;
end;
:: Theorem 2.12, p. 155
theorem Th34:
for N being meet-continuous Lawson complete TopLattice for S
being Scott TopAugmentation of N for x being Element of N holds {inf A where A
is Subset of S : x in A & A in sigma S} = {inf J where J is Subset of N : x in
J & J in lambda N}
proof
let N be meet-continuous Lawson complete TopLattice, S be Scott
TopAugmentation of N, x be Element of N;
set l = {inf A where A is Subset of N : x in A & A in lambda N}, s = {inf J
where J is Subset of S : x in J & J in sigma S};
thus s c= l by Th33;
let k be object;
assume k in l;
then consider A being Subset of N such that
A1: k = inf A and
A2: x in A and
A3: A in lambda N;
A4: the RelStr of N = the RelStr of S by YELLOW_9:def 4;
then reconsider J = A as Subset of S;
A is open by A3,Th12;
then uparrow J is open by Th15;
then
A5: uparrow J in sigma S by WAYBEL14:24;
A6: J c= uparrow J by WAYBEL_0:16;
inf A = inf J by A4,YELLOW_0:17,27
.= inf uparrow J by WAYBEL_0:38,YELLOW_0:17;
hence thesis by A5,A1,A2,A6;
end;
:: Theorem 2.13, p. 155, 1 <=> 2
theorem Th35:
for N being meet-continuous Lawson complete TopLattice holds N
is continuous iff N is with_open_semilattices & InclPoset sigma N is continuous
proof
let N be meet-continuous Lawson complete TopLattice;
set S = the Scott TopAugmentation of N;
A1: the RelStr of N = the RelStr of S by YELLOW_9:def 4;
hereby
assume
A2: N is continuous;
for x being Point of S ex J being Basis of x st for W being Subset of
S st W in J holds W is Filter of S
proof
let x be Point of S;
consider J being Basis of x such that
A3: for W being Subset of S st W in J holds W is open filtered by A2,
WAYBEL14:35;
take J;
let W be Subset of S;
assume
A4: W in J;
then W is open by A3;
hence thesis by A3,A4,WAYBEL11:def 4,YELLOW_8:12;
end;
hence N is with_open_semilattices by Th32;
InclPoset sigma S is continuous by A2,WAYBEL14:36;
hence InclPoset sigma N is continuous by A1,YELLOW_9:52;
end;
assume that
A5: N is with_open_semilattices and
A6: InclPoset sigma N is continuous;
A7: for x being Element of S ex J being Basis of x st for Y being Subset of
S st Y in J holds Y is open filtered
proof
let x be Element of S;
reconsider y = x as Element of N by A1;
consider J being Basis of y such that
A8: for A being Subset of N st A in J holds subrelstr A is
meet-inheriting by A5;
reconsider J9 = {uparrow A where A is Subset of N: A in J} as Basis of x
by Th16;
take J9;
let Y be Subset of S;
assume
A9: Y in J9;
then consider A being Subset of N such that
A10: Y = uparrow A and
A11: A in J;
subrelstr A is meet-inheriting by A8,A11;
then A is filtered by YELLOW12:26;
hence thesis by A1,A9,A10,WAYBEL_0:4,YELLOW_8:12;
end;
sigma S = sigma N by A1,YELLOW_9:52;
then
for x being Element of S holds x = "\/" ({inf X where X is Subset of S:
x in X & X in sigma S}, S) by A7,A6,WAYBEL14:37;
then S is continuous by WAYBEL14:38;
hence thesis by A1,YELLOW12:15;
end;
registration
cluster continuous -> with_open_semilattices for
Lawson complete TopLattice;
coherence by Th35;
end;
registration
let N be continuous Lawson complete TopLattice;
cluster InclPoset sigma N -> continuous;
coherence by Th35;
end;
:: Theorem 2.13, p. 155, 1 => 3
theorem
for N being continuous Lawson complete TopLattice holds N is compact
Hausdorff topological_semilattice with_open_semilattices
proof
let N be continuous Lawson complete TopLattice;
thus N is compact Hausdorff;
InclPoset sigma N is continuous;
hence N is topological_semilattice by Th22;
thus thesis;
end;
:: Theorem 2.13, p. 155, 3 => 3'
theorem
for N being Hausdorff topological_semilattice with_open_semilattices
Lawson complete TopLattice holds N is with_compact_semilattices
proof
let N be Hausdorff topological_semilattice with_open_semilattices Lawson
complete TopLattice;
let x be Point of N;
consider BO being Basis of x such that
A1: for A being Subset of N st A in BO holds subrelstr A is
meet-inheriting by Def4;
set BC = {Cl A where A is Subset of N: A in BO};
BC c= bool the carrier of N
proof
let k be object;
assume k in BC;
then ex A being Subset of N st k = Cl A & A in BO;
hence thesis;
end;
then reconsider BC as Subset-Family of N;
BC is basis of x
proof
let S be a_neighborhood of x;
A2: Int S c= S by TOPS_1:16;
x in Int S by CONNSP_2:def 1;
then consider W being Subset of N such that
A3: W in BO and
A4: W c= Int S by YELLOW_8:13;
A5: W is open by A3,YELLOW_8:12;
x in W by A3,YELLOW_8:12;
then x in Int W by A5,TOPS_1:23;
then reconsider T = W as a_neighborhood of x by CONNSP_2:def 1;
per cases;
suppose
A6: W <> [#]N;
x in W by A3,YELLOW_8:12;
then {x} c= W by ZFMISC_1:31;
then consider G being Subset of N such that
A7: G is open and
A8: {x} c= G and
A9: Cl G c= W by A5,A6,CONNSP_2:20;
x in G by A8,ZFMISC_1:31;
then consider K being Subset of N such that
A10: K in BO and
A11: K c= G by A7,YELLOW_8:13;
A12: K is open by A10,YELLOW_8:12;
A13: Int K c= Int Cl K by PRE_TOPC:18,TOPS_1:19;
x in K by A10,YELLOW_8:12;
then x in Int K by A12,TOPS_1:23;
then reconsider KK = Cl K as a_neighborhood of x by A13,CONNSP_2:def 1;
take KK;
thus KK in BC by A10;
Cl K c= Cl G by A11,PRE_TOPC:19;
then Cl K c= W by A9;
then KK c= Int S by A4;
hence thesis by A2;
end;
suppose
A14: W = [#]N;
take T;
Cl [#]N = [#]N by TOPS_1:2;
hence T in BC by A3,A14;
thus thesis by A4,A2;
end;
end;
then reconsider BC as basis of x;
take BC;
let A be Subset of N;
assume A in BC;
then consider C being Subset of N such that
A15: A = Cl C and
A16: C in BO;
subrelstr C is meet-inheriting by A1,A16;
hence subrelstr A is meet-inheriting by A15,Th31;
thus thesis by A15,COMPTS_1:8;
end;
:: Theorem 2.13, p. 155, 3' => 4
theorem
for N being meet-continuous Hausdorff Lawson complete TopLattice, x
being Element of N holds x = "\/"({inf V where V is Subset of N: x in V & V in
lambda N},N)
proof
let N be meet-continuous Hausdorff Lawson complete TopLattice, x be
Element of N;
set S = the Scott complete TopAugmentation of N;
A1: InclPoset sigma S is continuous by WAYBEL14:36;
A2: the RelStr of S = the RelStr of N by YELLOW_9:def 4;
then reconsider y = x as Element of S;
for y being Element of S ex J being Basis of y st for X being Subset of
S st X in J holds X is open filtered by WAYBEL14:35;
hence x = "\/" ({inf X where X is Subset of S: y in X & X in sigma S}, S) by
A1,WAYBEL14:37
.= "\/" ({inf X where X is Subset of S: x in X & X in sigma S}, N) by A2,
YELLOW_0:17,26
.= "\/" ({inf V where V is Subset of N: x in V & V in lambda N}, N) by Th34
;
end;
:: Theorem 2.13, p. 155, 1 <=> 4
theorem
for N being meet-continuous Lawson complete TopLattice holds N is
continuous iff for x being Element of N holds x = "\/"({inf V where V is Subset
of N: x in V & V in lambda N},N)
proof
let N be meet-continuous Lawson complete TopLattice;
set S = the complete Scott TopAugmentation of N;
A1: the RelStr of S = the RelStr of N by YELLOW_9:def 4;
hereby
assume
A2: N is continuous;
then
A3: for x being Element of S ex J being Basis of x st for Y being Subset
of S st Y in J holds Y is open filtered by WAYBEL14:35;
let x be Element of N;
InclPoset sigma S is continuous by A2,WAYBEL14:36;
hence x = "\/" ({inf X where X is Subset of S: x in X & X in sigma S}, S )
by A3,A1,WAYBEL14:37
.= "\/" ({inf X where X is Subset of S: x in X & X in sigma S}, N) by A1,
YELLOW_0:17,26
.= "\/"({inf V where V is Subset of N: x in V & V in lambda N},N) by Th34
;
end;
assume
A4: for x being Element of N holds x = "\/"({inf V where V is Subset of
N: x in V & V in lambda N},N);
now
let x be Element of S;
thus x = "\/"({inf V where V is Subset of N: x in V & V in lambda N},N) by
A1,A4
.= "\/"({inf V where V is Subset of S: x in V & V in sigma S},N) by A1
,Th34
.= "\/"({inf V where V is Subset of S: x in V & V in sigma S},S) by A1,
YELLOW_0:17,26;
end;
then S is continuous by WAYBEL14:38;
hence thesis by A1,YELLOW12:15;
end;
:: Exercise 2.16, p. 156, 1 <=> 2
theorem Th40:
for N being meet-continuous Lawson complete TopLattice holds N
is algebraic iff N is with_open_semilattices & InclPoset sigma N is algebraic
proof
let N be meet-continuous Lawson complete TopLattice;
set S = the Scott TopAugmentation of N;
A1: the RelStr of S = the RelStr of N by YELLOW_9:def 4;
hereby
assume
A2: N is algebraic;
then reconsider M = N as algebraic LATTICE;
M is continuous;
hence N is with_open_semilattices;
S is algebraic by A1,A2,WAYBEL_8:17;
then
ex K being Basis of S st K = {uparrow x where x is Element of S: x in
the carrier of CompactSublatt S} by WAYBEL14:42;
then InclPoset sigma S is algebraic by WAYBEL14:43;
hence InclPoset sigma N is algebraic by A1,YELLOW_9:52;
end;
assume that
A3: N is with_open_semilattices and
A4: InclPoset sigma N is algebraic;
reconsider T = InclPoset sigma N as algebraic LATTICE by A4;
T is continuous;
then N is continuous by A3,Th35;
then
for x being Element of S ex K being Basis of x st for Y being Subset of
S st Y in K holds Y is open filtered by WAYBEL14:35;
then
A5: for V being Element of InclPoset sigma S ex VV being Subset of
InclPoset sigma S st V = sup VV & for W being Element of InclPoset sigma S st W
in VV holds W is co-prime by WAYBEL14:39;
InclPoset sigma S is algebraic by A1,A4,YELLOW_9:52;
then ex K being Basis of S st K = {uparrow x where x is Element of S: x in
the carrier of CompactSublatt S} by A5,WAYBEL14:44;
then S is algebraic by WAYBEL14:45;
hence thesis by A1,WAYBEL_8:17;
end;
registration
let N be meet-continuous algebraic Lawson complete TopLattice;
cluster InclPoset sigma N -> algebraic;
coherence by Th40;
end;