:: On the Order-consistent Topology of Complete and Uncomplete
:: Lattices
:: by Ewa Gr\c{a}dzka
::
:: Received May 23, 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, WAYBEL_9, WAYBEL_0, SUBSET_1, CANTOR_1, WAYBEL11,
STRUCT_0, REWRITE1, PRELAMB, YELLOW_9, PRE_TOPC, RELAT_2, ORDINAL2,
CONNSP_2, ZFMISC_1, TARSKI, SETFAM_1, XXREAL_0, RLVECT_3, WAYBEL19,
RCOMP_1, FINSET_1, YELLOW_2, RELAT_1, TOPS_1, LATTICE3, YELLOW_0,
FUNCT_1, ORDERS_2, LATTICES, SEQM_3, YELLOW_6, CARD_FIL, EQREL_1, PROB_1,
T_0TOPSP, ARYTM_3, WAYBEL_7, WAYBEL32, CARD_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FINSET_1,
SETFAM_1, FUNCT_2, DOMAIN_1, STRUCT_0, ORDERS_2, LATTICE3, PRE_TOPC,
TOPS_1, CONNSP_2, T_0TOPSP, YELLOW_0, WAYBEL_0, CANTOR_1, YELLOW_2,
WAYBEL_2, YELLOW_6, WAYBEL_9, RELSET_1, WAYBEL11, WAYBEL19, YELLOW_9;
constructors DOMAIN_1, TOPS_1, TOPS_2, CONNSP_2, LATTICE3, CANTOR_1, WAYBEL_1,
WAYBEL11, YELLOW_9, RELSET_1, WAYBEL_2;
registrations SUBSET_1, FUNCT_1, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0,
WAYBEL_3, YELLOW_6, WAYBEL11, YELLOW_9, WAYBEL21, YELLOW14, WAYBEL29,
TOPS_1, CARD_1, ORDINAL1, RELSET_1;
requirements SUBSET, BOOLE;
definitions TARSKI, WAYBEL_0, WAYBEL11, LATTICE3, WAYBEL_9, XBOOLE_0;
equalities WAYBEL_0, WAYBEL11, XBOOLE_0, SUBSET_1, STRUCT_0;
expansions TARSKI, WAYBEL_0, WAYBEL11, LATTICE3, WAYBEL_9, XBOOLE_0;
theorems YELLOW_9, CANTOR_1, PRE_TOPC, WAYBEL_0, CONNSP_2, WAYBEL11, ZFMISC_1,
TARSKI, YELLOW_6, ORDERS_2, TOPS_2, TOPS_1, YELLOW_8, YELLOW_0, RELAT_1,
FUNCT_1, YELLOW_2, SUBSET_1, FINSET_1, WAYBEL_2, SETFAM_1, TSP_1,
WAYBEL21, WAYBEL_8, FUNCT_2, RELSET_1, XBOOLE_0, XBOOLE_1, STRUCT_0;
schemes FRAENKEL, DOMAIN_1, FUNCT_1, FUNCT_2;
begin
definition
let T be non empty TopRelStr;
attr T is upper means
:Def1:
the set of all (downarrow x)` where x is Element of T is prebasis of T;
end;
registration
cluster Scott up-complete strict for TopLattice;
existence
proof set R = the complete LATTICE;
set T = the strict Scott correct TopAugmentation of R;
take T;
thus thesis;
end;
end;
definition
let T be TopSpace-like non empty reflexive TopRelStr;
attr T is order_consistent means
:Def2:
for x being Element of T holds downarrow x = Cl {x} &
for N being eventually-directed net of T st x = sup N
for V being a_neighborhood of x holds N is_eventually_in V;
end;
registration
cluster -> upper for 1-element reflexive TopSpace-like TopRelStr;
coherence
proof
let T be 1-element reflexive TopSpace-like TopRelStr;
set BB = the set of all (downarrow x)` where x is Element of T;
BB c= bool the carrier of T
proof
let a be object;
assume a in BB;
then ex x being Element of T st a = (downarrow x)`;
hence thesis;
end;
then reconsider C = BB as Subset-Family of T;
reconsider C as Subset-Family of T;
A1: BB c= the topology of T
proof
let a be object;
reconsider aa=a as set by TARSKI:1;
assume a in BB;
then consider x being Element of T such that
A2: a = (downarrow x)`;
aa c= {}
proof
let y be object;
assume
A3: y in aa;
A4: x <= x;
A5: y = x by A2,A3,STRUCT_0:def 10;
x in downarrow x by A4,WAYBEL_0:17;
then
A6: x in (downarrow x) /\ aa by A3,A5,XBOOLE_0:def 4;
(downarrow x) misses aa by A2,XBOOLE_1:79;
hence thesis by A6;
end;
then a = {};
hence thesis by PRE_TOPC:1;
end;
reconsider F = {the carrier of T} as Basis of T by YELLOW_9:10;
BB = {{}}
proof
thus BB c= {{}}
proof
let a be object;
reconsider aa=a as set by TARSKI:1;
assume a in BB;
then consider x being Element of T such that
A7: a = (downarrow x)`;
A8: x <= x;
A9: the carrier of T = {x} by YELLOW_9:9;
x in downarrow x by A8,WAYBEL_0:17;
then a = {} or a = the carrier of T & not x in aa
by A7,A9,XBOOLE_0:def 5,ZFMISC_1:33;
hence thesis by TARSKI:def 1;
end;
set x = the Element of T;
A10: x <= x;
A11: the carrier of T = {x} by YELLOW_9:9;
x in downarrow x by A10,WAYBEL_0:17;
then (downarrow x)` = {} or (downarrow x)` = the carrier of T &
not x in (downarrow x)` by A11,XBOOLE_0:def 5,ZFMISC_1:33;
then {} in BB;
hence thesis by ZFMISC_1:31;
end;
then FinMeetCl C = {{}, the carrier of T} by YELLOW_9:11;
then F c= FinMeetCl C by ZFMISC_1:7;
hence BB is prebasis of T by A1,CANTOR_1:def 4,TOPS_2:64;
end;
end;
registration
cluster upper trivial up-complete strict for TopLattice;
existence
proof
set T = the 1-element up-complete strict TopLattice;
take T;
thus thesis;
end;
end;
theorem Th1:
for T being upper up-complete non empty TopPoset
for A being Subset of T st A is open holds A is upper
proof
let T be upper up-complete non empty TopPoset;
let A be Subset of T;
assume A is open;
then
A1: A in the topology of T by PRE_TOPC:def 2;
reconsider BB = the set of all (downarrow x)` where x is Element of T
as prebasis of T by Def1;
consider F being Basis of T such that
A2: F c= FinMeetCl BB by CANTOR_1:def 4;
the topology of T c= UniCl F by CANTOR_1:def 2;
then consider Y being Subset-Family of T such that
A3: Y c= F and
A4: A = union Y by A1,CANTOR_1:def 1;
let x,y be Element of T;
assume x in A;
then consider Z being set such that
A5: x in Z and
A6: Z in Y by A4,TARSKI:def 4;
Z in F by A3,A6;
then consider X being Subset-Family of T such that
A7: X c= BB and X is finite and
A8: Z = Intersect X by A2,CANTOR_1:def 3;
assume
A9: x <= y;
now
let Q be set;
assume
A10: Q in X;
then Q in BB by A7;
then consider z being Element of T such that
A11: Q = (downarrow z)`;
A12: x in Q by A5,A8,A10,SETFAM_1:43;
(downarrow z) misses Q by A11,XBOOLE_1:79;
then not x in downarrow z by A12,XBOOLE_0:3;
then not x <= z by WAYBEL_0:17;
then not y <= z by A9,ORDERS_2:3;
then not y in downarrow z by WAYBEL_0:17;
hence y in Q by A11,XBOOLE_0:def 5;
end;
then y in Z by A8,SETFAM_1:43;
hence thesis by A4,A6,TARSKI:def 4;
end;
theorem
for T being up-complete non empty TopPoset holds
T is upper implies T is order_consistent
proof
let T be up-complete non empty TopPoset;
assume
A1: T is upper;
then reconsider BB = the set of all (downarrow x)` where x is Element of T
as prebasis of T;
for x being Element of T holds downarrow x = Cl {x} &
for N being eventually-directed net of T st x = sup N
for V being a_neighborhood of x holds N is_eventually_in V
proof
let x be Element of T;
A2: downarrow x c= Cl {x}
proof
let a be object;
assume
A3: a in downarrow x;
then reconsider a9 = a as Point of T;
for G being Subset of T st G is open holds a9 in G implies {x} meets G
proof
let G be Subset of T such that
A4: G is open;
assume
A5: a9 in G;
reconsider v = a9 as Element of T;
A6: v <= x by A3,WAYBEL_0:17;
G is upper by A1,A4,Th1;
then
A7: x in G by A5,A6;
x in {x} by TARSKI:def 1;
hence thesis by A7,XBOOLE_0:3;
end;
hence thesis by PRE_TOPC:24;
end;
Cl {x} c= downarrow x
proof
let a be object;
assume
A8: a in Cl{x};
reconsider BB as Subset-Family of T;
(downarrow x)` in BB;
then A9: (downarrow x)` is open by TOPS_2:def 1;
(downarrow x)` = [#]T\downarrow x;
then
A10: downarrow x is closed by A9,PRE_TOPC:def 3;
x <= x;
then x in downarrow x by WAYBEL_0:17;
then {x} c= downarrow x by ZFMISC_1:31;
hence thesis by A8,A10,PRE_TOPC:15;
end;
hence downarrow x = Cl {x} by A2;
thus for N being eventually-directed net of T st x = sup N
for V being a_neighborhood of x holds N is_eventually_in V
proof
let N be eventually-directed net of T;
assume x = sup N;
then
A11: x = Sup the mapping of N by WAYBEL_2:def 1
.= sup rng netmap (N,T) by YELLOW_2:def 5;
let V be a_neighborhood of x;
A12: x in Int V by CONNSP_2:def 1;
FinMeetCl BB is Basis of T by YELLOW_9:23;
then
A13: the topology of T = UniCl FinMeetCl BB by YELLOW_9:22;
Int V in the topology of T by PRE_TOPC:def 2;
then consider Y being Subset-Family of T such that
A14: Y c= FinMeetCl BB and
A15: Int V = union Y by A13,CANTOR_1:def 1;
consider Y1 being set such that
A16: x in Y1 and
A17: Y1 in Y by A12,A15,TARSKI:def 4;
consider Z being Subset-Family of T such that
A18: Z c= BB and
A19: Z is finite and
A20: Y1 = Intersect Z by A14,A17,CANTOR_1:def 3;
reconsider rngN = rng netmap (N,T) as Subset of T;
rngN is directed by WAYBEL_2:18;
then ex a being Element of T st a is_>=_than rngN &
for b being Element of T st b is_>=_than rngN holds a <= b
by WAYBEL_0:def 39;
then
A21: ex_sup_of rngN,T by YELLOW_0:15;
defpred P[object,object] means
ex D1 being set st D1 = $1 &
for i,j being Element of N st i = $2 & j >= i holds N.j in D1;
A22: for Q being object st Q in Z
ex b being object st b in the carrier of N & P[Q,b]
proof
let Q be object;
assume
A23: Q in Z;
then Q in BB by A18;
then consider v1 being Element of T such that
A24: Q = (downarrow v1)`;
x in (downarrow v1)` by A16,A20,A23,A24,SETFAM_1:43;
then not x in downarrow v1 by XBOOLE_0:def 5;
then
A25: not x <= v1 by WAYBEL_0:17;
not rngN c= downarrow v1
proof
assume
A26: rngN c= downarrow v1;
ex_sup_of downarrow v1,T by WAYBEL_0:34;
then sup rngN <= sup downarrow v1 by A21,A26,YELLOW_0:34;
hence contradiction by A11,A25,WAYBEL_0:34;
end;
then consider w be object such that
A27: w in rngN and
A28: not w in downarrow v1;
reconsider w9 = w as Element of T by A27;
consider i being object such that
A29: i in dom the mapping of N and
A30: w9 = (the mapping of N).i by A27,FUNCT_1:def 3;
reconsider i as Element of N by A29;
consider b being Element of N such that
A31: for l being Element of N st b <= l holds N.i <= N.l by WAYBEL_0:11;
take b;
thus b in the carrier of N;
reconsider QQ=Q as set by TARSKI:1;
take QQ;
thus QQ = Q;
thus for j,k being Element of N st j = b & k >= j holds N.k in QQ
proof
let j,k be Element of N such that
A32: j = b and
A33: k >= j;
A34: N.i <= N.k by A31,A32,A33;
not N.i <= v1 by A28,A30,WAYBEL_0:17;
then not N.k <= v1 by A34,ORDERS_2:3;
then not N.k in downarrow v1 by WAYBEL_0:17;
hence thesis by A24,XBOOLE_0:def 5;
end;
end;
consider f be Function such that
A35: dom f = Z & rng f c= the carrier of N and
A36: for Q being object st Q in Z holds P[Q,f.Q] from FUNCT_1:sch 6(A22);
reconsider rngf = rng f as finite Subset of [#]N by A19,A35,FINSET_1:8;
[#]N is directed by WAYBEL_0:def 6;
then consider k being Element of N such that
k in [#]N and
A37: k is_>=_than rngf by WAYBEL_0:1;
take k;
let k1 be Element of N such that
A38: k <= k1;
now
let Q be set;
assume
A39: Q in Z;
then
A40: f.Q in rngf by A35,FUNCT_1:def 3;
then reconsider j = f.Q as Element of N;
A41: j <= k by A37,A40;
P[Q,f.Q] by A36,A39;
hence N.k1 in Q by A38,ORDERS_2:3,A41;
end;
then
A42: N.k1 in Y1 by A20,SETFAM_1:43;
Y1 c= union Y by A17,ZFMISC_1:74;
then
A43: N.k1 in Int V by A15,A42;
Int V c= V by TOPS_1:16;
hence thesis by A43;
end;
end;
hence thesis;
end;
theorem Th3:
for R being up-complete non empty reflexive transitive antisymmetric
RelStr ex T being TopAugmentation of R st T is Scott
proof
let R be up-complete non empty reflexive transitive antisymmetric RelStr;
set T = the Scott TopAugmentation of R;
take T;
thus thesis;
end;
theorem
for R being up-complete non empty Poset
for T being TopAugmentation of R holds T is Scott implies T is correct;
registration
let R be up-complete non empty reflexive transitive antisymmetric RelStr;
cluster Scott -> correct for TopAugmentation of R;
coherence;
end;
registration
let R be up-complete non empty reflexive transitive antisymmetric RelStr;
cluster Scott correct for TopAugmentation of R;
existence
proof
consider T being TopAugmentation of R such that
A1: T is Scott by Th3;
take T;
thus thesis by A1;
end;
end;
theorem Th5: :: Remark 1.4 (ii)
for T being Scott up-complete non empty reflexive transitive antisymmetric
TopRelStr, x being Element of T holds Cl {x} = downarrow x
proof
let T be Scott up-complete non empty reflexive transitive
antisymmetric TopRelStr, x be Element of T;
reconsider T9 = T as Scott TopAugmentation of T by YELLOW_9:44;
reconsider dx = downarrow x as Subset of T9;
reconsider A = {x} as Subset of T9;
A1: downarrow x is closed by WAYBEL11:11;
x <= x;
then x in downarrow x by WAYBEL_0:17;
then
A2: {x} c= downarrow x by ZFMISC_1:31;
now
let C be Subset of T9 such that
A3: A c= C;
reconsider D = C as Subset of T9;
assume C is closed;
then
A4: D is lower by WAYBEL11:7;
x in C by A3,ZFMISC_1:31;
hence dx c= C by A4,WAYBEL11:6;
end;
hence thesis by A1,A2,YELLOW_8:8;
end;
theorem Th6:
for T being up-complete Scott non empty TopPoset holds
T is order_consistent
proof
let T be up-complete Scott non empty TopPoset;
for x being Element of T holds downarrow x = Cl {x} &
for N being eventually-directed net of T st x = sup N
for V being a_neighborhood of x holds N is_eventually_in V
proof
let x be Element of T;
for N being eventually-directed net of T st x = sup N
for V being a_neighborhood of x holds N is_eventually_in V
proof
let N be eventually-directed net of T;
assume x = sup N;
then x = Sup the mapping of N by WAYBEL_2:def 1;
then
A1: x = sup rng the mapping of N by YELLOW_2:def 5;
let V be a_neighborhood of x;
A2: x in Int V by CONNSP_2:def 1;
reconsider rngN = rng netmap (N,T) as Subset of T;
rngN is directed by WAYBEL_2:18;
then Int V meets rngN by A1,A2,WAYBEL11:def 1;
then consider z being object such that
A3: z in Int V and
A4: z in rngN by XBOOLE_0:3;
reconsider z9 = z as Element of T by A3;
consider i being object such that
A5: i in dom the mapping of N and
A6: z9 = (the mapping of N).i by A4,FUNCT_1:def 3;
reconsider i as Element of N by A5;
consider j being Element of N such that
A7: for k being Element of N st j <= k holds N.i <= N.k by WAYBEL_0:11;
take j;
let l be Element of N;
assume j <= l;
then N.i <= N.l by A7;
then
A8: N.l in Int V by A3,A6,WAYBEL_0:def 20;
Int V c= V by TOPS_1:16;
hence thesis by A8;
end;
hence thesis by Th5;
end;
hence thesis;
end;
theorem Th7:
for R being /\-complete Semilattice, Z be net of R, D be Subset of R st
D = the set of all "/\"({Z.k where k is Element of Z: k >= j},R)
where j is Element of Z holds D is non empty directed
proof
let R be /\-complete Semilattice, Z be net of R, D be Subset of R;
assume
A1: D = the set of all "/\"({Z.k where k is Element of Z: k >= j},R)
where j is Element of Z;
set j = the Element of Z;
"/\"({Z.k where k is Element of Z: k >= j},R) in D by A1;
hence D is non empty;
let x,y be Element of R;
assume x in D;
then consider jx being Element of Z such that
A2: x = "/\"({Z.k where k is Element of Z: k >= jx},R) by A1;
assume y in D;
then consider jy being Element of Z such that
A3: y = "/\"({Z.k where k is Element of Z: k >= jy},R) by A1;
reconsider jx, jy as Element of Z;
consider j being Element of Z such that
A4: j >= jx and
A5: j >= jy by YELLOW_6:def 3;
consider j9 being Element of Z such that
A6: j9 >= j and j9 >= j by YELLOW_6:def 3;
deffunc F(Element of Z) = Z.$1;
defpred Px[Element of Z] means $1 >= jx;
defpred Py[Element of Z] means $1 >= jy;
defpred P[Element of Z] means $1 >= j;
set Ex = {F(k) where k is Element of Z: Px[k]},
Ey = {F(k) where k is Element of Z: Py[k]},
E = {F(k) where k is Element of Z: P[k]};
A7: Z.j in Ex by A4;
A8: Z.j in Ey by A5;
A9: Z.j9 in E by A6;
A10: Ex is Subset of R from DOMAIN_1:sch 8;
A11: Ey is Subset of R from DOMAIN_1:sch 8;
A12: E is Subset of R from DOMAIN_1:sch 8;
take z = "/\"({Z.k where k is Element of Z: k >= j},R);
reconsider Ex9= Ex as non empty Subset of R by A7,A10;
reconsider Ey9 = Ey as non empty Subset of R by A8,A11;
reconsider E9 = E as non empty Subset of R by A9,A12;
A13: ex_inf_of E9,R by WAYBEL_0:76;
A14: ex_inf_of Ex9,R by WAYBEL_0:76;
A15: ex_inf_of Ey9,R by WAYBEL_0:76;
thus z in D by A1;
E9 c= Ex9
proof
let e be object;
assume e in E9;
then consider k being Element of Z such that
A16: e = Z.k and
A17: k >= j;
reconsider k as Element of Z;
k >= jx by A4,A17,YELLOW_0:def 2;
hence thesis by A16;
end;
hence x <= z by A2,A13,A14,YELLOW_0:35;
E9 c= Ey9
proof
let e be object;
assume e in E9;
then consider k being Element of Z such that
A18: e = Z.k and
A19: k >= j;
reconsider k as Element of Z;
k >= jy by A5,A19,YELLOW_0:def 2;
hence thesis by A18;
end;
hence y <= z by A3,A13,A15,YELLOW_0:35;
end;
theorem Th8:
for R being /\-complete Semilattice, S being Subset of R,
a being Element of R holds a in S implies "/\"(S,R) <= a
proof
let R be /\-complete Semilattice, S be Subset of R;
let a be Element of R;
assume
A1: a in S;
then ex_inf_of S,R by WAYBEL_0:76;
then S is_>=_than "/\"(S, R) by YELLOW_0:31;
hence thesis by A1;
end;
theorem Th9:
for R being /\-complete Semilattice, N being monotone reflexive net of R
holds lim_inf N = sup N
proof
let R be /\-complete Semilattice, N be monotone reflexive net of R;
deffunc F(Element of N) = "/\"({N.i where i is Element of N: i >= $1},R);
deffunc G(Element of N) = N.$1;
defpred P[set] means not contradiction;
set X = {F(j) where j is Element of N: P[j]};
A1: for j being Element of N holds G(j) = F(j)
proof
let j be Element of N;
defpred P[Element of N] means $1 >= j;
set Y = {G(i) where i is Element of N: P[i]};
j <= j;
then
A2: N.j in Y;
Y is Subset of R from DOMAIN_1:sch 8;
then
A3: ex_inf_of Y,R by A2,WAYBEL_0:76;
A4: N.j is_<=_than Y
proof
let y be Element of R;
assume y in Y;
then ex i being Element of N st y = N.i & j <= i;
hence N.j <= y by WAYBEL11:def 9;
end;
for b being Element of R st b is_<=_than Y holds N.j >= b
proof
let b be Element of R;
assume
A5: b is_<=_than Y;
reconsider j9 = j as Element of N;
j9 <= j9;
then N.j9 in Y;
hence thesis by A5;
end;
hence thesis by A3,A4,YELLOW_0:def 10;
end;
rng the mapping of N = {G(j) where j is Element of N: P[j]} by WAYBEL11:19
.= X from FRAENKEL:sch 5(A1);
hence lim_inf N = Sup the mapping of N by YELLOW_2:def 5
.= sup N by WAYBEL_2:def 1;
end;
theorem Th10:
for R being /\-complete Semilattice for S being Subset of R
holds S in the topology of ConvergenceSpace Scott-Convergence R
iff S is inaccessible upper
proof
let R be /\-complete Semilattice;
set SC = Scott-Convergence R, T = ConvergenceSpace SC;
A1: the topology of T = { V where V is Subset of R:
for p being Element of R st p in V
for N being net of R st [N,p] in SC holds N is_eventually_in V}
by YELLOW_6:def 24;
let S be Subset of R;
hereby
assume S in the topology of T;
then
A2: ex V being Subset of R st ( S = V)&( for p being Element of
R st p in V for N being net of R st [N,p] in SC holds N is_eventually_in V)
by A1;
thus S is inaccessible
proof
let D be non empty directed Subset of R such that
A3: sup D in S;
A4: dom id D = D by RELAT_1:45;
A5: rng id D = D by RELAT_1:45;
then reconsider f = id D as Function of D, the carrier of R
by A4,FUNCT_2:def 1,RELSET_1:4;
reconsider N = Net-Str(D,f) as strict monotone reflexive net of R
by A5,WAYBEL11:20;
A6: N in NetUniv R by WAYBEL11:21;
lim_inf N = sup N by Th9
.= Sup the mapping of N by WAYBEL_2:def 1
.= "\/"(rng the mapping of N,R) by YELLOW_2:def 5
.= "\/"(rng f,R) by WAYBEL11:def 10
.= sup D by RELAT_1:45;
then sup D is_S-limit_of N;
then [N,sup D] in SC by A6,WAYBEL11:def 8;
then N is_eventually_in S by A2,A3;
then consider i0 being Element of N such that
A7: for j being Element of N st i0 <= j holds N.j in S;
consider j0 being Element of N such that
A8: j0 >= i0 and j0 >= i0 by YELLOW_6:def 3;
A9: N.j0 in S by A7,A8;
A10: D = the carrier of N by WAYBEL11:def 10;
N.j0 = (id D).j0 by WAYBEL11:def 10
.= j0 by A10;
hence thesis by A9,A10,XBOOLE_0:3;
end;
thus S is upper
proof
let x,y be Element of R such that
A11: x in S and
A12: x <= y;
A13: Net-Str y in NetUniv R by WAYBEL11:29;
y = lim_inf Net-Str y by WAYBEL11:28;
then x is_S-limit_of Net-Str y by A12;
then [Net-Str y,x] in SC by A13,WAYBEL11:def 8;
then Net-Str y is_eventually_in S by A2,A11;
hence thesis by WAYBEL11:27;
end;
end;
assume that
A14: S is inaccessible and
A15: S is upper;
for p being Element of R st p in S
for N being net of R st [N,p] in SC holds N is_eventually_in S
proof
let p be Element of R such that
A16: p in S;
reconsider p9 = p as Element of R;
let N be net of R;
assume
A17: [N,p] in SC;
SC c= [:NetUniv R, the carrier of R:] by YELLOW_6:def 18;
then
A18: N in NetUniv R by A17,ZFMISC_1:87;
then ex N9 being strict net of R st N9 = N &
the carrier of N9 in the_universe_of the carrier of R by YELLOW_6:def 11;
then p is_S-limit_of N by A17,A18,WAYBEL11:def 8;
then
A19: p9 <= lim_inf N;
deffunc F(Element of N) = "/\"({N.i where i is Element of N: i >= $1},R);
defpred P[set] means not contradiction;
set X ={F(j) where j is Element of N: P[j]};
X is Subset of R from DOMAIN_1:sch 8;
then reconsider D = X as Subset of R;
reconsider D as non empty directed Subset of R by Th7;
sup D in S by A15,A16,A19;
then D meets S by A14;
then D /\ S <> {};
then consider d being Element of R such that
A20: d in D /\ S by SUBSET_1:4;
reconsider d as Element of R;
d in D by A20,XBOOLE_0:def 4;
then consider j being Element of N such that
A21: d = "/\"({N.i where i is Element of N: i >= j},R);
defpred P[Element of N] means $1 >= j;
deffunc F(Element of N) = N.$1;
{F(i) where i is Element of N: P[i]} is Subset of R from DOMAIN_1:sch 8;
then reconsider Y = {N.i where i is Element of N: i >= j} as Subset of R;
reconsider j as Element of N;
take j;
let i0 be Element of N;
A22: d in S by A20,XBOOLE_0:def 4;
assume j <= i0;
then N.i0 in Y;
then d <= N.i0 by A21,Th8;
hence thesis by A15,A22;
end;
hence thesis by A1;
end;
theorem Th11:
for R being /\-complete up-complete Semilattice,
T being TopAugmentation of R st the topology of T = sigma R holds T is Scott
proof
let R be /\-complete up-complete Semilattice;
let T be TopAugmentation of R such that
A1: the topology of T = sigma R;
A2: the RelStr of T = the RelStr of R by YELLOW_9:def 4;
T is Scott
proof
let S be Subset of T;
reconsider A = S as Subset of R by A2;
thus S is open implies S is inaccessible upper
proof
assume S is open;
then S in the topology of T by PRE_TOPC:def 2;
then A is inaccessible upper by A1,Th10;
hence thesis by A2,WAYBEL_0:25,YELLOW_9:47;
end;
assume
A3: S is inaccessible upper;
A is inaccessible
proof
let D be non empty directed Subset of R such that
A4: sup D in A;
reconsider E = D as Subset of T by A2;
ex a being Element of R st a is_>=_than D &
for b being Element of R st b is_>=_than D holds a <= b
by WAYBEL_0:def 39;
then
A5: ex_sup_of D,R by YELLOW_0:15;
A6: E is directed by A2,WAYBEL_0:3;
sup D = sup E by A2,A5,YELLOW_0:26;
hence thesis by A3,A4,A6;
end;
then A is inaccessible upper by A2,A3,WAYBEL_0:25;
then A in the topology of T by A1,Th10;
hence thesis by PRE_TOPC:def 2;
end;
hence thesis;
end;
registration
let R be /\-complete up-complete Semilattice;
cluster strict Scott correct for TopAugmentation of R;
existence
proof
set T = TopRelStr(#the carrier of R, the InternalRel of R, sigma R#);
the RelStr of T = the RelStr of R;
then reconsider T as TopAugmentation of R by YELLOW_9:def 4;
take T;
thus thesis by Th11,YELLOW_9:48;
end;
end;
theorem
for S being up-complete /\-complete Semilattice,
T being Scott TopAugmentation of S holds sigma S = the topology of T
proof
let S be up-complete /\-complete Semilattice;
let T be Scott TopAugmentation of S;
thus sigma S c= the topology of T
proof
let e be object;
assume
A1: e in sigma S;
then reconsider A = e as Subset of S;
A2: the RelStr of S = the RelStr of T by YELLOW_9:def 4;
then reconsider A9 = A as Subset of T;
A is inaccessible upper by A1,Th10;
then A9 is inaccessible upper by A2,WAYBEL_0:25,YELLOW_9:47;
hence thesis by PRE_TOPC:def 2;
end;
let e be object;
assume
A3: e in the topology of T;
then reconsider A = e as Subset of T;
A4: A is open by A3,PRE_TOPC:def 2;
A5: the RelStr of S = the RelStr of T by YELLOW_9:def 4;
then reconsider A9 = A as Subset of S;
A9 is inaccessible
proof
let D be non empty directed Subset of S such that
A6: sup D in A9;
reconsider E = D as Subset of T by A5;
ex a being Element of S st a is_>=_than D &
for b being Element of S st b is_>=_than D holds a <= b
by WAYBEL_0:def 39;
then
A7: ex_sup_of D,S by YELLOW_0:15;
A8: E is directed by A5,WAYBEL_0:3;
sup D = sup E by A5,A7,YELLOW_0:26;
hence thesis by A4,A6,A8,WAYBEL11:def 1;
end;
then A9 is inaccessible upper by A4,A5,WAYBEL_0:25;
hence thesis by Th10;
end;
theorem :: Remark 1.4 (iii)
for T being Scott up-complete non empty reflexive transitive antisymmetric
TopRelStr holds T is T_0-TopSpace
proof
let T be Scott up-complete
non empty reflexive transitive antisymmetric TopRelStr;
reconsider T9 = T as Scott TopAugmentation of T by YELLOW_9:44;
now
let x,y be Point of T9;
reconsider x9 = x, y9 = y as Element of T9;
A1: Cl {x9} = downarrow x9 by Th5;
A2: Cl {y9} = downarrow y9 by Th5;
assume x <> y;
hence Cl {x} <> Cl {y} by A1,A2,WAYBEL_0:19;
end;
hence thesis by TSP_1:def 5;
end;
registration
let R be up-complete non empty reflexive transitive antisymmetric RelStr;
cluster -> up-complete for TopAugmentation of R;
coherence;
end;
theorem Th14:
for R being up-complete non empty reflexive transitive antisymmetric
RelStr for T being Scott TopAugmentation of R, x being Element of T,
A being upper Subset of T st not x in A
holds (downarrow x)` is a_neighborhood of A
proof
let R be up-complete non empty reflexive transitive antisymmetric RelStr,
T be Scott TopAugmentation of R, x be Element of T,
A be upper Subset of T such that
A1: not x in A;
downarrow x is closed by WAYBEL11:11;
then (downarrow x)` is open;
then
A2: Int (downarrow x)` = (downarrow x)` by TOPS_1:23;
A misses downarrow x by A1,WAYBEL11:5;
then A c= (downarrow x)` by SUBSET_1:23;
hence thesis by A2,CONNSP_2:def 2;
end;
theorem ::Remark 1.4 (iv)
for R being up-complete non empty reflexive transitive antisymmetric
TopRelStr for T being Scott TopAugmentation of R, S being upper Subset of T
ex F being Subset-Family of T st S = meet F &
for X being Subset of T st X in F holds X is a_neighborhood of S
proof
let R be up-complete non empty reflexive transitive antisymmetric
TopRelStr, T be Scott TopAugmentation of R, S be upper Subset of T;
defpred P[set] means $1 is a_neighborhood of S;
set F = { X where X is Subset of T: P[X]};
F is Subset-Family of T from DOMAIN_1:sch 7;
then reconsider F as Subset-Family of T;
take F;
thus S = meet F
proof
[#]T is a_neighborhood of S by CONNSP_2:28;
then
A1: [#]T in F;
now
let Z1 be set;
assume Z1 in F;
then ex X being Subset of T st Z1 = X & X is a_neighborhood of S;
hence S c= Z1 by CONNSP_2:29;
end;
hence S c= meet F by A1,SETFAM_1:5;
let x be object such that
A2: x in meet F and
A3: not x in S;
reconsider p = x as Element of T by A2;
(downarrow p)` is a_neighborhood of S by A3,Th14;
then (downarrow p)` in F;
then
A4: meet F c= (downarrow p)` by SETFAM_1:3;
p <= p;
then p in downarrow p by WAYBEL_0:17;
hence contradiction by A2,A4,XBOOLE_0:def 5;
end;
let X be Subset of T;
assume X in F;
then ex Y being Subset of T st X = Y & Y is a_neighborhood of S;
hence thesis;
end;
theorem ::Remark 1.4 (v)
for T being Scott up-complete non empty reflexive transitive antisymmetric
TopRelStr, S being Subset of T holds S is open iff S is upper property(S)
proof
let T be Scott up-complete non empty reflexive transitive antisymmetric
TopRelStr, S be Subset of T;
hereby
assume
A1: S is open;
hence
S is upper;
thus S is property(S)
proof
let D be non empty directed Subset of T;
assume sup D in S;
then S meets D by A1,WAYBEL11:def 1;
then consider y being object such that
A2: y in S and
A3: y in D by XBOOLE_0:3;
reconsider y as Element of T by A2;
take y;
thus thesis by A1,A2,A3,WAYBEL_0:def 20;
end;
end;
assume that
A4: S is upper and
A5: S is property(S);
S is inaccessible
proof
let D be non empty directed Subset of T;
assume sup D in S;
then consider y being Element of T such that
A6: y in D and
A7: for x being Element of T st x in D & x >= y holds x in S by A5;
y >= y by YELLOW_0:def 1;
then y in S by A6,A7;
hence thesis by A6,XBOOLE_0:3;
end;
hence thesis by A4;
end;
theorem Th17:
for R being up-complete non empty reflexive transitive antisymmetric
TopRelStr, S being non empty directed Subset of R,
a being Element of R holds a in S implies a <= "\/"(S, R)
proof
let R be up-complete non empty reflexive transitive antisymmetric
TopRelStr;
let S be non empty directed Subset of R, a be Element of R;
assume
A1: a in S;
ex_sup_of S,R by WAYBEL_0:75;
then S is_<=_than "\/"(S, R) by YELLOW_0:30;
hence thesis by A1;
end;
::Remark 1.4 (vi)
registration
let T be up-complete non empty reflexive transitive antisymmetric
TopRelStr;
cluster lower -> property(S) for Subset of T;
coherence
proof
let S be Subset of T;
assume
A1: S is lower;
let D be non empty directed Subset of T such that
A2: sup D in S;
consider y being Element of T such that
A3: y in D by SUBSET_1:4;
take y;
thus y in D by A3;
let x be Element of T such that
A4: x in D and x >= y;
x <= sup D by A4,Th17;
hence thesis by A1,A2;
end;
end;
theorem
for T being finite up-complete non empty Poset,
S being Subset of T holds S is inaccessible
proof
let T be finite up-complete non empty Poset,
S be Subset of T, D be non empty directed Subset of T such that
A1: sup D in S;
sup D in D
proof
reconsider D9 = D as finite Subset of T;
D9 c= D9;
then reconsider E = D9 as finite Subset of D;
consider x being Element of T such that
A2: x in D and
A3: x is_>=_than E by WAYBEL_0:1;
A4: for b being Element of T st D is_<=_than b holds b >= x by A2;
for c being Element of T st D is_<=_than c &
for b being Element of T st D is_<=_than b holds b >= c holds c = x
proof
let c be Element of T such that
A5: D is_<=_than c and
A6: for b being Element of T st D is_<=_than b holds b >= c;
A7: x >= c by A3,A6;
c >= x by A2,A5;
hence thesis by A7,ORDERS_2:2;
end;
then ex_sup_of D,T by A3,A4,YELLOW_0:def 7;
hence thesis by A2,A3,A4,YELLOW_0:def 9;
end;
hence thesis by A1,XBOOLE_0:3;
end;
theorem Th19:
for R being complete connected LATTICE,
T being Scott TopAugmentation of R, x being Element of T holds
(downarrow x)` is open
proof
let R be complete connected LATTICE,
T be Scott TopAugmentation of R, x be Element of T;
reconsider S = downarrow x as directly_closed lower Subset of T by WAYBEL11:8
;
S` is open;
hence thesis;
end;
theorem
for R being complete connected LATTICE,
T being Scott TopAugmentation of R, S being Subset of T holds
S is open iff S = the carrier of T or S in the set of all (downarrow x)`
where x is Element of T
proof
let R be complete connected LATTICE,
T be Scott TopAugmentation of R, S be Subset of T;
set DD = the set of all (downarrow x)` where x is Element of T;
thus S is open implies S = the carrier of T or S in DD
proof
assume
A1: S is open;
assume that
A2: S <> the carrier of T and
A3: not S in DD;
A4: [#]T\S <> {} by A2,PRE_TOPC:4;
A5: the RelStr of T = the RelStr of R by YELLOW_9:def 4;
then reconsider K = S` as Subset of R;
reconsider D = K as non empty directed Subset of T by A4,A5,WAYBEL_0:3;
A6: D misses S by SUBSET_1:23;
reconsider x = sup D as Element of T;
S` = downarrow x
proof
thus S` c= downarrow x
proof
let a be object;
assume
A7: a in S`;
then reconsider A = a as Element of T;
x is_>=_than S` by YELLOW_0:32;
then A <= x by A7;
hence thesis by WAYBEL_0:17;
end;
let a be object;
assume
A8: a in downarrow x;
then reconsider A = a as Element of T;
A9: A <= x by A8,WAYBEL_0:17;
not x in S by A1,A6,WAYBEL11:def 1;
then not A in S by A1,A9,WAYBEL_0:def 20;
hence thesis by XBOOLE_0:def 5;
end;
then (downarrow x)` = S;
hence contradiction by A3;
end;
assume
A10: S = the carrier of T or S in DD;
per cases by A10;
suppose
A11: S = the carrier of T;
A12: the RelStr of T = the RelStr of R by YELLOW_9:def 4;
then S = [#]R by A11;
then
A13: S is inaccessible by A12,YELLOW_9:47;
S is upper
by A11;
hence thesis by A13;
end;
suppose S in DD;
then ex x being Element of T st ( S = (downarrow x)`);
hence thesis by Th19;
end;
end;
registration
let R be up-complete non empty Poset;
cluster order_consistent for correct TopAugmentation of R;
correctness
proof
set T = the Scott correct TopAugmentation of R;
take T;
thus thesis by Th6;
end;
end;
registration
cluster order_consistent complete for TopLattice;
correctness
proof
set T = the Scott complete TopLattice;
take T;
thus thesis by Th6;
end;
end;
theorem Th21:
for R being non empty TopRelStr for A being Subset of R holds
(for x being Element of R holds downarrow x = Cl {x}) implies
(A is open implies A is upper)
proof
let R be non empty TopRelStr, A be Subset of R;
assume
A1: for x being Element of R holds downarrow x = Cl {x};
assume
A2: A is open;
let x,y be Element of R such that
A3: x in A and
A4: x <= y;
x in downarrow y by A4,WAYBEL_0:17;
then x in Cl {y} by A1;
then A meets {y} by A2,A3,PRE_TOPC:24;
then consider z be object such that
A5: z in A /\ {y} by XBOOLE_0:4;
A6: z in A by A5,XBOOLE_0:def 4;
z in {y} by A5,XBOOLE_0:def 4;
hence thesis by A6,TARSKI:def 1;
end;
theorem
for R being non empty TopRelStr for A being Subset of R holds
(for x being Element of R holds downarrow x = Cl {x}) implies
for A being Subset of R st A is closed holds A is lower
proof
let R be non empty TopRelStr, A be Subset of R;
assume
A1: for x being Element of R holds downarrow x = Cl {x};
let A be Subset of R such that
A2: A is closed;
let x,y be Element of R such that
A3: x in A and
A4: y <= x;
y in downarrow x by A4,WAYBEL_0:17;
then
A5: y in Cl {x} by A1;
{x} c= A
by A3,TARSKI:def 1;
hence thesis by A2,A5,PRE_TOPC:15;
end;
definition
let S be non empty 1-sorted, R be non empty RelStr,
f be Function of the carrier of R,the carrier of S;
func R*'f -> strict non empty NetStr over S means
:Def3:
the RelStr of it = the RelStr of R & the mapping of it = f;
existence
proof
reconsider M = NetStr (# the carrier of R,the InternalRel of R, f #)
as strict non empty NetStr over S;
take M;
thus thesis;
end;
uniqueness;
end;
registration
let S be non empty 1-sorted, R be non empty transitive RelStr,
f be Function of the carrier of R,the carrier of S;
cluster R*'f -> transitive;
coherence
proof
the RelStr of R*'f = the RelStr of R by Def3;
hence thesis by WAYBEL_8:13;
end;
end;
registration
let S be non empty 1-sorted, R be non empty directed RelStr,
f be Function of the carrier of R,the carrier of S;
cluster R*'f -> directed;
coherence
proof
A1: the RelStr of R*'f = the RelStr of R by Def3;
[#]R is directed by WAYBEL_0:def 6;
hence [#](R*'f) is directed by A1,WAYBEL_0:3;
end;
end;
definition
let R be non empty RelStr, N be prenet of R;
func inf_net N -> strict prenet of R means
:Def4:
ex f being Function of N,R st it = N*'f & for i being Element of N holds
f.i = "/\"({N.k where k is Element of N: k >= i},R);
existence
proof
deffunc F(Element of N) = "/\"({N.k where k is Element of N: k >= $1},R);
consider g being Function of the carrier of N, the carrier of R such that
A1: for i being Element of N holds g.i = F(i) from FUNCT_2:sch 4;
reconsider f = g as Function of N,R;
reconsider M = N*'f as strict prenet of R;
take M;
thus thesis by A1;
end;
uniqueness
proof
let M, P be strict prenet of R such that
A2: ex f being Function of N,R st M = N*'f & for i being Element of N holds
f.i = "/\"({N.k where k is Element of N: k >= i},R) and
A3: ex f being Function of N,R st P = N*'f & for i being Element of N holds
f.i = "/\"({N.k where k is Element of N: k >= i},R);
consider f1 being Function of N,R such that
A4: M = N*'f1 and
A5: for i being Element of N holds f1.i = "/\" ({N.k where k is Element
of N: k >= i},R)
by A2;
consider f2 being Function of N,R such that
A6: P = N*'f2 and
A7: for i being Element of N holds f2.i = "/\" ({N.k where k is Element
of N: k >= i},R)
by A3;
for i being object st i in the carrier of N holds f1.i = f2.i
proof
let i be object;
assume i in the carrier of N;
then reconsider i as Element of N;
f1.i = "/\" ({N.k where k is Element of N: k >= i},R) by A5
.= f2.i by A7;
hence thesis;
end;
hence thesis by A4,A6,FUNCT_2:12;
end;
end;
registration
let R be non empty RelStr, N be net of R;
cluster inf_net N -> transitive;
coherence
proof
ex f being Function of N,R st inf_net N = N*'f &
for i being Element of N holds
f.i = "/\"({N.k where k is Element of N: k >= i},R) by Def4;
hence thesis;
end;
end;
registration
let R be non empty RelStr, N be net of R;
cluster inf_net N -> directed;
coherence;
end;
registration
let R be /\-complete non empty reflexive antisymmetric RelStr,
N be net of R;
cluster inf_net N -> monotone;
coherence
proof
let i,j be Element of inf_net N such that
A1: i <= j;
consider f being Function of N,R such that
A2: inf_net N = N*'f and
A3: for i being Element of N holds f.i = "/\"({N.k where k is Element of
N: k >= i},R)
by Def4;
A4: the RelStr of inf_net N = the RelStr of N by A2,Def3;
then reconsider i9=i,j9=j as Element of N;
deffunc F(Element of N) = N.$1;
defpred P[Element of N] means $1 >= j9;
defpred Q[Element of N] means $1 >= i9;
set J= {F(k) where k is Element of N: P[k]};
set I= {F(k) where k is Element of N: Q[k]};
A5: J is Subset of R from DOMAIN_1:sch 8;
consider j0 being Element of N such that
A6: j0 >= j9 and j0 >= j9 by YELLOW_6:def 3;
N.j0 in J by A6;
then reconsider J9= J as non empty Subset of R by A5;
A7: I is Subset of R from DOMAIN_1:sch 8;
consider j1 being Element of N such that
A8: j1 >= i9 and j1 >= i9 by YELLOW_6:def 3;
N.j1 in I by A8;
then reconsider I9= I as non empty Subset of R by A7;
A9: ex_inf_of J9,R by WAYBEL_0:76;
A10: ex_inf_of I9,R by WAYBEL_0:76;
A11: J9 c= I9
proof
let a be object;
assume
A12: a in J9;
then reconsider x = a as Element of R;
consider k being Element of N such that
A13: x = N.k and
A14: k >= j9 by A12;
reconsider k9 = k as Element of N;
i9 <= j9 by A1,A4,YELLOW_0:1;
then i9 <= k9 by A14,YELLOW_0:def 2;
hence thesis by A13;
end;
A15: f.i9 = "/\"(I,R) by A3;
A16: f.j9 = "/\"(J,R) by A3;
the mapping of (inf_net N) = f by A2,Def3;
hence thesis by A9,A10,A11,A15,A16,YELLOW_0:35;
end;
end;
registration
let R be /\-complete non empty reflexive antisymmetric RelStr,
N be net of R;
cluster inf_net N -> eventually-directed;
coherence;
end;
theorem Th23:
for R being non empty RelStr, N being net of R
holds rng the mapping of (inf_net N) =
the set of all "/\"({N.i where i is Element of N: i >= j},R) where
j is Element of N
proof
let R be non empty RelStr, N be net of R;
consider f being Function of N,R such that
A1: inf_net N = N*'f and
A2: for i being Element of N holds f.i = "/\" ({N.k where k is Element
of N: k >= i},R)
by Def4;
A3: the RelStr of inf_net N = the RelStr of N by A1,Def3;
A4: the mapping of (inf_net N) = f by A1,Def3;
then
A5: the carrier of inf_net N = dom f by FUNCT_2:def 1;
thus rng the mapping of inf_net N c=
the set of all "/\"({N.i where i is Element of N: i >= j},R) where
j is Element of N
proof
let e be object;
assume e in rng the mapping of inf_net N;
then consider u being object such that
A6: u in dom f and
A7: e = f.u by A4,FUNCT_1:def 3;
reconsider u as Element of N by A6;
f.u = "/\"({N.k where k is Element of N: k >= u},R) by A2;
hence thesis by A7;
end;
let e be object;
assume e in the set of all
"/\"({N.i where i is Element of N: i >= j},R) where
j is Element of N;
then consider j being Element of N such that
A8: e = "/\"({N.i where i is Element of N: i >= j},R);
e = (the mapping of inf_net N).j by A2,A4,A8;
hence thesis by A3,A4,A5,FUNCT_1:def 3;
end;
theorem Th24:
for R being up-complete /\-complete LATTICE, N being net of R holds
sup inf_net N = lim_inf N
proof
let R be up-complete /\-complete LATTICE, N be net of R;
defpred P[set] means not contradiction;
deffunc F(Element of N) = "/\"({N.l where l is Element of N: l >= $1},R);
sup inf_net N = Sup the mapping of (inf_net N) by WAYBEL_2:def 1
.= sup rng the mapping of (inf_net N) by YELLOW_2:def 5
.= lim_inf N by Th23;
hence thesis;
end;
theorem
for R being up-complete /\-complete LATTICE, N being net of R,
i being Element of N holds sup inf_net N = lim_inf (N|i)
proof
let R be up-complete /\-complete LATTICE, N be net of R, i be Element of N;
sup inf_net N = lim_inf N by Th24;
hence thesis by WAYBEL21:41;
end;
theorem Th26:
for R being /\-complete Semilattice, N being net of R,
V being upper Subset of R holds
inf_net N is_eventually_in V implies N is_eventually_in V
proof
let R be /\-complete Semilattice, N be net of R, V be upper Subset of R;
consider f being Function of N,R such that
A1: inf_net N = N*'f and
A2: for i being Element of N holds f.i = "/\" ({N.k where k is Element
of N: k >= i},R)
by Def4;
A3: the RelStr of inf_net N = the RelStr of N by A1,Def3;
assume inf_net N is_eventually_in V;
then consider i being Element of inf_net N such that
A4: for j being Element of inf_net N st i <= j holds (inf_net N).j in V;
consider j0 being Element of inf_net N such that
A5: i <= j0 and i <= j0 by YELLOW_6:def 3;
A6: (inf_net N).j0 in V by A4,A5;
reconsider j9 = j0 as Element of N by A3;
take j9;
let j be Element of N such that
A7: j9 <= j;
defpred P[Element of N] means $1 >= j9;
deffunc F(Element of N) = N.$1;
set E = {F(k) where k is Element of N: P[k]};
E is Subset of R from DOMAIN_1:sch 8;
then reconsider E as Subset of R;
the mapping of (inf_net N) = f by A1,Def3;
then
A8: (inf_net N).j0 = "/\"(E,R) by A2;
N.j in E by A7;
then "/\"(E,R) <= N.j by Th8;
hence thesis by A6,A8,WAYBEL_0:def 20;
end;
theorem
for R being /\-complete Semilattice, N being net of R,
V being lower Subset of R holds
N is_eventually_in V implies inf_net N is_eventually_in V
proof
let R be /\-complete Semilattice, N be net of R, V be lower Subset of R;
consider f being Function of N,R such that
A1: inf_net N = N*'f and
A2: for i being Element of N holds f.i = "/\" ({N.k where k is Element
of N: k >= i},R)
by Def4;
A3: the RelStr of inf_net N = the RelStr of N by A1,Def3;
assume N is_eventually_in V;
then consider i being Element of N such that
A4: for j being Element of N st i <= j holds N.j in V;
reconsider i9 = i as Element of inf_net N by A3;
take i9;
let j be Element of inf_net N such that
A5: i9 <= j;
reconsider j0 = j as Element of N by A3;
defpred P[Element of N] means $1 >= j0;
deffunc F(Element of N) = N.$1;
set E = {F(k) where k is Element of N: P[k]};
consider j1 being Element of N such that
A6: j1 >= j0 and j1 >= j0 by YELLOW_6:def 3;
E is Subset of R from DOMAIN_1:sch 8;
then reconsider E as Subset of R;
i <= j0 by A3,A5,YELLOW_0:1;
then i <= j1 by A6,YELLOW_0:def 2;
then
A7: N.j1 in V by A4;
N.j1 in E by A6;
then
A8: "/\"(E,R) <= N.j1 by Th8;
the mapping of (inf_net N) = f by A1,Def3;
then (inf_net N).j = "/\"(E,R) by A2;
hence thesis by A7,A8,WAYBEL_0:def 19;
end;
theorem Th28:
for R being order_consistent up-complete /\-complete non empty TopLattice
for N being net of R, x being Element of R holds
x <= lim_inf N implies x is_a_cluster_point_of N
proof
let R be order_consistent up-complete /\-complete non empty TopLattice,
N be net of R, x be Element of R;
assume
A1: x <= lim_inf N;
defpred P[Element of N] means not contradiction;
deffunc F(Element of N) = "/\"({N.i where i is Element of N:i >= $1}, R);
set X = {F(j) where j is Element of N: P[j]};
X is Subset of R from DOMAIN_1:sch 8;
then reconsider D = X as Subset of R;
reconsider D as non empty directed Subset of R by Th7;
sup D = lim_inf N;
then
A2: sup D = sup inf_net N by Th24;
let V be a_neighborhood of x;
for a being Element of R holds downarrow a = Cl {a} by Def2;
then
A3: Int V is upper by Th21;
x in Int V by CONNSP_2:def 1;
then sup D in Int V by A1,A3;
then reconsider W = Int V as a_neighborhood of (sup D) by CONNSP_2:3;
A4: Int V c= V by TOPS_1:16;
inf_net N is_eventually_in W by A2,Def2;
then N is_eventually_in W by A3,Th26;
then N is_eventually_in V by A4,WAYBEL_0:8;
hence thesis by YELLOW_6:19;
end;
theorem
for R being order_consistent up-complete /\-complete non empty TopLattice
for N being eventually-directed net of R, x being Element of R holds
x <= lim_inf N iff x is_a_cluster_point_of N
proof
let R be order_consistent up-complete /\-complete non empty TopLattice,
N be eventually-directed net of R, x be Element of R;
thus x <= lim_inf N implies x is_a_cluster_point_of N by Th28;
thus x is_a_cluster_point_of N implies x <= lim_inf N
proof
assume
A1: x is_a_cluster_point_of N;
defpred P[Element of N] means not contradiction;
deffunc F(Element of N) = "/\"({N.i where i is Element of N:i >= $1}, R);
set X = {F(j) where j is Element of N: P[j]};
X is Subset of R from DOMAIN_1:sch 8;
then reconsider D = X as Subset of R;
reconsider D as non empty directed Subset of R by Th7;
for G being Subset of R st G is open holds x in G implies {sup D} meets G
proof
let G be Subset of R such that
A2: G is open;
assume x in G;
then reconsider G as a_neighborhood of x by A2,CONNSP_2:3;
A3: N is_often_in G by A1;
now
let i be Element of N;
consider j1 being Element of N such that
i <= j1 and
A4: N.j1 in G by A3;
consider j2 being Element of N such that
A5: for k being Element of N st j2 <= k holds N.j1 <= N.k by WAYBEL_0:11;
defpred P[Element of N] means $1 >= j2;
deffunc F(Element of N) = N.$1;
set E = {F(k) where k is Element of N: P[k]};
A6: E is Subset of R from DOMAIN_1:sch 8;
consider j9 being Element of N such that
A7: j9 >= j2 and j9 >= j2 by YELLOW_6:def 3;
N.j9 in E by A7;
then reconsider E9 = E as non empty Subset of R by A6;
A8: ex_inf_of E9,R by WAYBEL_0:76;
N.j1 is_<=_than E9
proof
let b be Element of R;
assume b in E9;
then ex k being Element of N st ( b = N.k)&( k >= j2);
hence N.j1 <= b by A5;
end;
then
A9: N.j1 <= "/\"(E9,R) by A8,YELLOW_0:31;
for a being Element of R holds downarrow a = Cl {a} by Def2;
then
A10: G is upper by A2,Th21;
then
A11: "/\"(E9,R) in G by A4,A9;
"/\"(E9,R) in D;
then "/\"(E9,R) <= sup D by Th17;
hence sup D in G by A10,A11;
end;
then
A12: sup D in G;
sup D in {sup D} by TARSKI:def 1;
hence thesis by A12,XBOOLE_0:3;
end;
then x in Cl {sup D} by PRE_TOPC:24;
then x in downarrow sup D by Def2;
hence thesis by WAYBEL_0:17;
end;
end;