:: Scott Topology
:: by Andrzej Trybulec
::
:: Received January 29, 1997
:: Copyright (c) 1997-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 ORDERS_2, SUBSET_1, XXREAL_0, XBOOLE_0, TARSKI, REWRITE1,
WAYBEL_0, SETFAM_1, LATTICES, LATTICE3, EQREL_1, RELAT_2, FINSET_1,
ORDINAL2, YELLOW_0, ZFMISC_1, STRUCT_0, CARD_1, RELAT_1, CARD_FIL,
WAYBEL_9, RCOMP_1, NATTRA_1, PRE_TOPC, T_0TOPSP, CONNSP_2, TOPS_1,
FUNCT_1, YELLOW_6, SEQM_3, CLASSES2, CLASSES1, YELLOW_2, PROB_1,
WAYBEL_3, ORDINAL1, CARD_3, PBOOLE, WAYBEL_5, FUNCT_6, RLVECT_2,
WAYBEL_6, RLVECT_3, YELLOW_8, WAYBEL11;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, RELAT_1, SETFAM_1,
FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCT_6, DOMAIN_1,
ORDINAL1, NUMBERS, STRUCT_0, WAYBEL_6, PRE_TOPC, TOPS_1, TOPS_2,
CANTOR_1, CONNSP_2, T_0TOPSP, TDLAT_3, PBOOLE, CLASSES1, CLASSES2,
CARD_3, PRALG_1, ORDERS_2, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1,
YELLOW_2, WAYBEL_1, YELLOW_3, YELLOW_4, WAYBEL_2, WAYBEL_3, WAYBEL_5,
YELLOW_6, WAYBEL_9, YELLOW_8;
constructors DOMAIN_1, CLASSES1, CLASSES2, TOPS_1, CONNSP_2, TDLAT_3,
T_0TOPSP, CANTOR_1, PRALG_1, PRALG_2, ORDERS_3, WAYBEL_1, YELLOW_4,
WAYBEL_3, WAYBEL_5, WAYBEL_6, WAYBEL_9, YELLOW_8, RELSET_1, TOPS_2,
WAYBEL_2, NUMBERS;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, FUNCT_2, FUNCOP_1, FINSET_1,
CARD_3, CLASSES2, PBOOLE, STRUCT_0, LATTICE3, YELLOW_0, TDLAT_3,
WAYBEL_0, YELLOW_1, WAYBEL_3, YELLOW_6, WAYBEL_5, WAYBEL_9, RELSET_1,
TOPS_1;
requirements SUBSET, BOOLE;
definitions STRUCT_0, XBOOLE_0, TARSKI, PRE_TOPC, WAYBEL_0, LATTICE3,
YELLOW_0, RELAT_1, YELLOW_6, YELLOW_4, WAYBEL_1, WAYBEL_3, TOPS_2,
YELLOW_8, WAYBEL_6;
equalities STRUCT_0, SUBSET_1, WAYBEL_0, YELLOW_6, WAYBEL_3, BINOP_1;
expansions XBOOLE_0, TARSKI, PRE_TOPC, WAYBEL_0, LATTICE3, YELLOW_0, YELLOW_6,
YELLOW_4, WAYBEL_1, WAYBEL_3;
theorems TSP_1, WAYBEL_0, YELLOW_0, TARSKI, SUBSET_1, TOPS_1, YELLOW_2,
SETFAM_1, CONNSP_2, ZFMISC_1, RELSET_1, TDLAT_3, TEX_1, ORDERS_2,
LATTICE3, YELLOW_6, WAYBEL_5, DOMAIN_1, WAYBEL_7, YELLOW_1, YELLOW_3,
WAYBEL_3, FUNCT_1, FUNCT_2, YELLOW_7, PRALG_1, WAYBEL_2, CLASSES1,
RELAT_1, WAYBEL_4, YELLOW_8, XBOOLE_0, XBOOLE_1, PARTFUN1;
schemes RELSET_1, DOMAIN_1, FRAENKEL, PBOOLE, XFAMILY;
begin :: Preliminaries
Lm1: for R,S being RelStr, p,q being Element of R, p9,q9 being Element of S
st p = p9 & q = q9 & the RelStr of R = the RelStr of S
holds p <= q implies p9 <= q9
proof
let R,S be RelStr, p,q be Element of R, p9,q9 be Element of S such that
A1: p = p9 and
A2: q = q9 and
A3: the RelStr of R = the RelStr of S;
assume p <= q;
then [p9,q9] in the InternalRel of S by A1,A2,A3,ORDERS_2:def 5;
hence thesis by ORDERS_2:def 5;
end;
scheme Irrel{D,I() -> non empty set, P[set], F(set)->set, F(set,set)-> set}:
{ F(u) where u is Element of D(): P[u]}
= { F(i,v) where i is Element of I(), v is Element of D(): P[v]}
provided
A1: for i being Element of I(), u being Element of D() holds F(u) = F(i,u)
proof
set A = { F(u) where u is Element of D(): P[u]},
B = { F(i,v) where i is Element of I(), v is Element of D(): P[v]};
thus A c= B
proof
let e be object;
set i = the Element of I();
assume e in A;
then consider u being Element of D() such that
A2: e = F(u) and
A3: P[u];
e = F(i,u) by A1,A2;
hence thesis by A3;
end;
let e be object;
assume e in B;
then consider i being Element of I(), u being Element of D() such that
A4: e = F(i,u) and
A5: P[u];
e = F(u) by A1,A4;
hence thesis by A5;
end;
theorem Th1:
for L being complete LATTICE, X,Y being Subset of L st Y is_coarser_than X
holds "/\"(X,L) <= "/\"(Y,L)
proof
let L be complete LATTICE, X,Y be Subset of L such that
A1: Y is_coarser_than X;
"/\"(X,L) is_<=_than Y
proof
let y be Element of L;
assume y in Y;
then consider x being Element of L such that
A2: x in X and
A3: x <= y by A1;
"/\"(X,L) <= x by A2,YELLOW_2:22;
hence "/\"(X,L) <= y by A3,YELLOW_0:def 2;
end;
hence thesis by YELLOW_0:33;
end;
theorem Th2:
for L being complete LATTICE, X,Y being Subset of L st X is_finer_than Y
holds "\/"(X,L) <= "\/"(Y,L)
proof
let L be complete LATTICE, X,Y be Subset of L such that
A1: X is_finer_than Y;
"\/"(Y,L) is_>=_than X
proof
let x be Element of L;
assume x in X;
then consider y being Element of L such that
A2: y in Y and
A3: x <= y by A1;
"\/"(Y,L) >= y by A2,YELLOW_2:22;
hence thesis by A3,YELLOW_0:def 2;
end;
hence thesis by YELLOW_0:32;
end;
theorem
for T being RelStr, A being upper Subset of T, B being directed Subset of T
holds A /\ B is directed
proof
let T be RelStr, A be upper Subset of T, B be directed Subset of T;
let x,y be Element of T such that
A1: x in A /\ B and
A2: y in A /\ B;
A3: x in B by A1,XBOOLE_0:def 4;
y in B by A2,XBOOLE_0:def 4;
then consider z being Element of T such that
A4: z in B and
A5: x <= z and
A6: y <= z by A3,WAYBEL_0:def 1;
take z;
x in A by A1,XBOOLE_0:def 4;
then z in A by A5,WAYBEL_0:def 20;
hence z in A /\ B by A4,XBOOLE_0:def 4;
thus thesis by A5,A6;
end;
registration
let T be reflexive non empty RelStr;
cluster non empty directed finite for Subset of T;
existence
proof set x = the Element of T;
take {x};
thus thesis by WAYBEL_0:5;
end;
end;
theorem Th4: :: uogolnione WAYBEL_3:16
for T being with_suprema Poset,
D being non empty directed finite Subset of T holds sup D in D
proof
let T be reflexive transitive antisymmetric with_suprema RelStr,
D be non empty directed finite Subset of T;
D c= D;
then reconsider E = D as finite Subset of D;
consider x being Element of T such that
A1: x in D and
A2: x is_>=_than E by WAYBEL_0:1;
A3: for b being Element of T st D is_<=_than
b holds b >= x by A1;
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
A4: D is_<=_than c and
A5: for b being Element of T st D is_<=_than b holds b >= c;
A6: x >= c by A2,A5;
c >= x by A1,A4;
hence thesis by A6,ORDERS_2:2;
end;
then ex_sup_of D,T by A2,A3;
hence thesis by A1,A2,A3,YELLOW_0:def 9;
end;
registration
cluster reflexive transitive 1-element antisymmetric
with_suprema with_infima finite strict for RelStr;
existence
proof
0 in {0} by TARSKI:def 1;
then reconsider r = {[0,0]} as Relation of {0} by RELSET_1:3;
reconsider T = RelStr(#{0},r#) as non empty RelStr;
take T;
thus T is reflexive
proof
let x be Element of T;
x = 0 by TARSKI:def 1;
then [x,x] in {[0,0]} by TARSKI:def 1;
hence thesis by ORDERS_2:def 5;
end;
then reconsider T9 = T as 1-element reflexive RelStr;
T9 is transitive;
hence T is transitive;
thus T is 1-element;
T9 is antisymmetric;
hence T is antisymmetric;
T9 is with_suprema;
hence T is with_suprema;
T9 is with_infima;
hence T is with_infima;
thus T is finite;
thus thesis;
end;
end;
registration
let T be finite 1-sorted;
cluster -> finite for Subset of T;
coherence;
end;
registration
let R be RelStr;
cluster empty -> lower upper for Subset of R;
coherence;
end;
registration
let R be 1-element RelStr;
cluster -> upper for Subset of R;
coherence
proof
let S be Subset of R;
ex x being Element of R st ( the carrier of R = {x}) by TEX_1:def 1;
then S = {}R or S = [#]R by ZFMISC_1:33;
hence thesis;
end;
end;
theorem Th5:
for T being non empty RelStr, x being Element of T,
A being upper Subset of T st not x in A holds A misses downarrow x
proof
let T be non empty RelStr, x be Element of T,
A be upper Subset of T such that
A1: not x in A;
assume A meets downarrow x;
then consider y being object such that
A2: y in A and
A3: y in downarrow x by XBOOLE_0:3;
reconsider y as Element of T by A2;
y <= x by A3,WAYBEL_0:17;
hence contradiction by A1,A2,WAYBEL_0:def 20;
end;
theorem Th6:
for T being non empty RelStr, x being Element of T,
A being lower Subset of T st x in A holds downarrow x c= A
proof
let T be non empty RelStr, x be Element of T, A be lower Subset of T;
assume x in A;
then not x in A` by XBOOLE_0:def 5;
then A` misses downarrow x by Th5;
then A` c= (downarrow x)` by SUBSET_1:23;
hence thesis by SUBSET_1:12;
end;
begin :: Scott Topology
definition
let T be non empty reflexive RelStr, S be Subset of T;
attr S is inaccessible_by_directed_joins means
:Def1:
for D being non empty directed Subset of T st sup D in S holds D meets S;
attr S is closed_under_directed_sups means
:Def2:
for D being non empty directed Subset of T st D c= S holds sup D in S;
attr S is property(S) means
:Def3:
for D being non empty directed Subset of T st sup D in S
ex y being Element of T st y in D &
for x being Element of T st x in D & x >= y holds x in S;
end;
notation
let T be non empty reflexive RelStr, S be Subset of T;
synonym S is inaccessible for S is inaccessible_by_directed_joins; synonym
S is directly_closed for S is closed_under_directed_sups;
end;
registration
let T be non empty reflexive RelStr;
cluster empty -> property(S) directly_closed for Subset of T;
coherence;
end;
registration
let T be non empty reflexive RelStr;
cluster property(S) directly_closed for Subset of T;
existence
proof
take {}T;
thus thesis;
end;
end;
registration
let T be non empty reflexive RelStr, S be property(S) Subset of T;
cluster S` -> directly_closed;
coherence
proof
let D be non empty directed Subset of T such that
A1: D c= S`;
assume not sup D in S`;
then sup D in S by XBOOLE_0:def 5;
then consider y being Element of T such that
A2: y in D and
A3: for x being Element of T st x in D & x >= y holds x in S by Def3;
y <= y;
then y in S by A2,A3;
then D /\ S <> {} by A2,XBOOLE_0:def 4;
then D meets S;
hence contradiction by A1,SUBSET_1:23;
end;
end;
definition
let T be reflexive non empty TopRelStr;
attr T is Scott means
:Def4:
for S being Subset of T holds S is open iff S is inaccessible upper;
end;
registration
let T be reflexive transitive antisymmetric non empty with_suprema
finite RelStr;
cluster -> inaccessible for Subset of T;
coherence
proof
let S be Subset of T, D be non empty directed Subset of T such that
A1: sup D in S;
sup D in D by Th4;
hence thesis by A1,XBOOLE_0:3;
end;
end;
definition
let T be reflexive transitive antisymmetric non empty with_suprema
finite TopRelStr;
redefine attr T is Scott means :: redefines Scott (WAYBEL11, definition)
for S being Subset of T holds S is open iff S is upper;
compatibility;
end;
registration
cluster complete strict 1-element Scott for TopLattice;
existence
proof
set T = the reflexive 1-element discrete strict finite TopRelStr;
take T;
thus T is complete strict 1-element;
let S be Subset of T;
thus thesis by TDLAT_3:15;
end;
end;
registration
let T be non empty reflexive RelStr;
cluster [#]T -> directly_closed inaccessible;
coherence
proof
thus [#]T is directly_closed;
let D be non empty directed Subset of T such that sup D in [#]T;
ex p being Element of T st ( p in D) by SUBSET_1:4;
hence D meets [#]T by XBOOLE_0:3;
end;
end;
registration
let T be non empty reflexive RelStr;
cluster directly_closed lower inaccessible upper for Subset of T;
existence
proof
take [#]T;
thus thesis;
end;
end;
registration
let T be non empty reflexive RelStr, S be inaccessible Subset of T;
cluster S` -> directly_closed;
coherence
proof
let D be non empty directed Subset of T;
assume D c= S`;
then D misses S by SUBSET_1:23;
then not sup D in S by Def1;
hence thesis by XBOOLE_0:def 5;
end;
end;
registration
let T be non empty reflexive RelStr, S be directly_closed Subset of T;
cluster S` -> inaccessible;
coherence
proof
let D be non empty directed Subset of T;
assume sup D in S`;
then not sup D in S by XBOOLE_0:def 5;
then not D c= S`` by Def2;
hence thesis by SUBSET_1:23;
end;
end;
theorem Th7: :: p. 100, Remark 1.4 (i)
for T being up-complete Scott non empty reflexive transitive TopRelStr,
S being Subset of T holds S is closed iff S is directly_closed lower
proof
let T be up-complete Scott non empty reflexive transitive TopRelStr,
S be Subset of T;
hereby
assume S is closed;
then S` is open;
then reconsider A = S` as inaccessible upper Subset of T by Def4;
A` is directly_closed lower;
hence S is directly_closed lower;
end;
assume S is directly_closed lower;
then reconsider S as directly_closed lower Subset of T;
S` is open by Def4;
hence thesis;
end;
theorem Th8:
for T being up-complete non empty reflexive transitive antisymmetric
TopRelStr, x being Element of T holds downarrow x is directly_closed
proof
let T be up-complete
non empty reflexive transitive antisymmetric TopRelStr, x be Element of T;
downarrow x is directly_closed
proof
let D be non empty directed Subset of T;
assume
A1: D c= downarrow x;
ex a being Element of T st a is_>=_than D &
for b being Element of T st b is_>=_than D holds a <= b
by WAYBEL_0:def 39;
then
A2: ex_sup_of D,T by YELLOW_0:15;
x is_>=_than D
by A1,WAYBEL_0:17;
then sup D <= x by A2,YELLOW_0:30;
hence thesis by WAYBEL_0:17;
end;
hence thesis;
end;
theorem Th9: :: p. 100, Remark 1.4 (ii)
for T being complete Scott TopLattice, x being Element of T
holds Cl {x} = downarrow x
proof
let T be complete Scott TopLattice, x be Element of T;
downarrow x is directly_closed by Th8;
then
A1: downarrow x is closed by Th7;
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 T such that
A3: {x} c= C;
reconsider D = C as Subset of T;
assume C is closed;
then
A4: D is lower by Th7;
x in C by A3,ZFMISC_1:31;
hence downarrow x c= C by A4,Th6;
end;
hence thesis by A1,A2,YELLOW_8:8;
end;
theorem :: p. 100, Remark 1.4 (iii)
for T being complete Scott TopLattice holds T is T_0-TopSpace
proof
let T be complete Scott TopLattice;
now
let x,y be Point of T;
reconsider x9 = x, y9 = y as Element of T;
A1: Cl {x9} = downarrow x9 by Th9;
A2: Cl {y9} = downarrow y9 by Th9;
assume x <> y;
hence Cl {x} <> Cl {y} by A1,A2,WAYBEL_0:19;
end;
hence thesis by TSP_1:def 5;
end;
theorem Th11:
for T being Scott up-complete non empty reflexive transitive antisymmetric
TopRelStr, x being Element of T holds downarrow x is closed
by Th8,Th7;
theorem Th12:
for T being up-complete Scott TopLattice, x being Element of T
holds (downarrow x)` is open
proof
let T be up-complete Scott TopLattice, x be Element of T;
downarrow x is closed by Th11;
hence thesis;
end;
theorem Th13:
for T being up-complete Scott TopLattice, 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 T be up-complete Scott TopLattice, x be Element of T,
A be upper Subset of T such that
A1: not x in A;
(downarrow x)` is open by Th12;
then
A2: Int (downarrow x)` = (downarrow x)` by TOPS_1:23;
A misses downarrow x by A1,Th5;
then A c= (downarrow x)` by SUBSET_1:23;
hence thesis by A2,CONNSP_2:def 2;
end;
theorem :: p. 100, Remark 1.4 (iv)
for T being complete Scott TopLattice, 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 T be complete Scott TopLattice, 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,Th13;
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 :: p. 100, Remark 1.4 (v)
for T being Scott TopLattice, S being Subset of T
holds S is open iff S is upper property(S)
proof
let T be Scott TopLattice, S be Subset of T;
hereby
assume
A1: S is open;
hence
A2: S is upper by Def4;
thus S is property(S)
proof
let D be non empty directed Subset of T such that
A3: sup D in S;
S is inaccessible by A1,Def4;
then S meets D by A3;
then consider y being object such that
A4: y in S and
A5: y in D by XBOOLE_0:3;
reconsider y as Element of T by A4;
take y;
thus thesis by A2,A4,A5;
end;
end;
assume that
A6: S is upper and
A7: 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
A8: y in D and
A9: for x being Element of T st x in D & x >= y holds x in S by A7;
y >= y by YELLOW_0:def 1;
then y in S by A8,A9;
hence thesis by A8,XBOOLE_0:3;
end;
hence thesis by A6,Def4;
end;
registration
let T be complete TopLattice;
:: p. 100, Remark 1.4 (vi)
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,YELLOW_2:22;
hence thesis by A1,A2;
end;
end;
Lm2: for T being non empty reflexive TopRelStr holds [#]T is property(S)
proof
let T be non empty reflexive TopRelStr;
let D be non empty directed Subset of T such that sup D in [#]T;
consider y being Element of T such that
A1: y in D by SUBSET_1:4;
take y;
thus y in D by A1;
let x be Element of T such that x in D and x >= y;
thus thesis;
end;
theorem :: p. 100, Remark 1.4 (vii)
for T being non empty transitive reflexive TopRelStr st
the topology of T = { S where S is Subset of T: S is property(S)}
holds T is TopSpace-like
proof
let T be non empty transitive reflexive TopRelStr such that
A1: the topology of T = { S where S is Subset of T: S is property(S)};
[#]T is property(S) by Lm2;
hence the carrier of T in the topology of T by A1;
hereby
let a be Subset-Family of T such that
A2: a c= the topology of T;
union a is property(S)
proof
let D be non empty directed Subset of T;
assume sup D in union a;
then consider x being set such that
A3: sup D in x and
A4: x in a by TARSKI:def 4;
x in the topology of T by A2,A4;
then consider X being Subset of T such that
A5: x = X and
A6: X is property(S) by A1;
consider y being Element of T such that
A7: y in D and
A8: for x being Element of T st x in D & x >=
y holds x in X by A3,A5,A6;
take y;
thus y in D by A7;
let u be Element of T;
assume that
A9: u in D and
A10: u >= y;
u in X by A8,A9,A10;
hence thesis by A4,A5,TARSKI:def 4;
end;
hence union a in the topology of T by A1;
end;
let a,b be Subset of T;
assume a in the topology of T;
then consider A being Subset of T such that
A11: a = A and
A12: A is property(S) by A1;
assume b in the topology of T;
then consider B being Subset of T such that
A13: b = B and
A14: B is property(S) by A1;
A /\ B is property(S)
proof
let D be non empty directed Subset of T;
assume
A15: sup D in A /\ B;
then sup D in A by XBOOLE_0:def 4;
then consider x being Element of T such that
A16: x in D and
A17: for z being Element of T st z in D & z >= x holds z in A by A12;
sup D in B by A15,XBOOLE_0:def 4;
then consider y being Element of T such that
A18: y in D and
A19: for z being Element of T st z in D & z >= y holds z in B by A14;
consider z being Element of T such that
A20: z in D and
A21: x <= z and
A22: y <= z by A16,A18,WAYBEL_0:def 1;
take z;
thus z in D by A20;
let u be Element of T such that
A23: u in D;
assume
A24: u >= z;
then u >= x by A21,YELLOW_0:def 2;
then
A25: u in A by A17,A23;
u >= y by A22,A24,YELLOW_0:def 2;
then u in B by A19,A23;
hence thesis by A25,XBOOLE_0:def 4;
end;
hence thesis by A1,A11,A13;
end;
begin :: Scott Convergence
reserve R for non empty RelStr,
N for net of R,
i for Element of N;
definition
let R,N;
func lim_inf N -> Element of R equals
"\/"((the set of all "/\"({N.i:i >= j},R) where j is Element of N),R);
correctness;
end;
definition
let R be reflexive non empty RelStr;
let N be net of R, p be Element of R;
pred p is_S-limit_of N means
p <= lim_inf N;
end;
definition
let R be reflexive non empty RelStr;
func Scott-Convergence R -> Convergence-Class of R means
:Def8:
for N being strict net of R st N in NetUniv R for p being Element of R
holds [N,p] in it iff p is_S-limit_of N;
existence
proof
defpred P[set,Element of R] means
ex N being strict net of R st N = $1 & $2 is_S-limit_of N;
consider C being Relation of NetUniv R, the carrier of R such that
A1: for x being Element of NetUniv R, y being Element of R
holds [x,y] in C iff P[x,y] from RELSET_1:sch 2;
reconsider C as Convergence-Class of R by YELLOW_6:def 18;
take C;
let N be strict net of R such that
A2: N in NetUniv R;
let p be Element of R;
hereby
assume [N,p] in C;
then ex M being strict net of R st M = N & p is_S-limit_of M by A1,A2;
hence p is_S-limit_of N;
end;
thus thesis by A1,A2;
end;
uniqueness
proof
let it1,it2 be Convergence-Class of R such that
A3: for N being strict net of R st N in NetUniv R for p being Element of R
holds [N,p] in it1 iff p is_S-limit_of N and
A4: for N being strict net of R st N in NetUniv R for p being Element of R
holds [N,p] in it2 iff p is_S-limit_of N;
let x,y be object;
A5: it1 c= [:NetUniv R, the carrier of R:] by YELLOW_6:def 18;
A6: it2 c= [:NetUniv R, the carrier of R:] by YELLOW_6:def 18;
hereby
assume
A7: [x,y] in it1;
then
A8: x in NetUniv R by A5,ZFMISC_1:87;
then consider N being strict net of R such that
A9: N = x and the carrier of N in the_universe_of the carrier of R by
YELLOW_6:def 11;
reconsider p = y as Element of R by A5,A7,ZFMISC_1:87;
p is_S-limit_of N by A3,A7,A8,A9;
hence [x,y] in it2 by A4,A8,A9;
end;
assume
A10: [x,y] in it2;
then
A11: x in NetUniv R by A6,ZFMISC_1:87;
then consider N being strict net of R such that
A12: N = x and the carrier of N in the_universe_of the carrier of R by
YELLOW_6:def 11;
reconsider p = y as Element of R by A6,A10,ZFMISC_1:87;
p is_S-limit_of N by A4,A10,A11,A12;
hence thesis by A3,A11,A12;
end;
end;
:: remarks, p.98
theorem
for R being complete LATTICE, N being net of R, p,q being Element of R
st p is_S-limit_of N & N is_eventually_in downarrow q holds p <= q
proof
let R be complete LATTICE, N be net of R, p,q be Element of R such that
A1: p <= lim_inf N and
A2: N is_eventually_in downarrow q;
consider j0 being Element of N such that
A3: for i being Element of N st j0 <= i holds N.i in downarrow q
by A2;
set X = the set of all "/\"({N.i where i is Element of N:
i >= j},R) where j is Element of N;
reconsider q9= q as Element of R;
q9 is_>=_than X
proof
let x be Element of R;
assume x in X;
then consider j1 being Element of N such that
A4: x = "/\"({N.i where i is Element of N: i >= j1},R);
set Y = {N.i where i is Element of N: i >= j1};
reconsider j1 as Element of N;
consider j2 being Element of N such that
A5: j2 >= j0 and
A6: j2 >= j1 by YELLOW_6:def 3;
N.j2 in Y by A6;
then
A7: x <= N.j2 by A4,YELLOW_2:22;
N.j2 in downarrow q by A3,A5;
then N.j2 <= q9 by WAYBEL_0:17;
hence x <= q9 by A7,YELLOW_0:def 2;
end;
then lim_inf N <= q9 by YELLOW_0:32;
hence thesis by A1,YELLOW_0:def 2;
end;
theorem Th18:
for R being complete LATTICE, N being net of R, p,q being Element of R
st N is_eventually_in uparrow q holds lim_inf N >= q
proof
let R be complete LATTICE, N be net of R, p,q be Element of R;
assume N is_eventually_in uparrow q;
then consider j0 being Element of N such that
A1: for i being Element of N st j0 <= i holds N.i in uparrow q;
set X = the set of all "/\"({N.i where i is Element of N:
i >= j},R) where j is Element of N;
set Y = {N.i where i is Element of N: i >= j0};
reconsider q9= q as Element of R;
"/\"(Y,R) in X;
then
A2: lim_inf N >= "/\"(Y,R) by YELLOW_2:22;
q9 is_<=_than Y
proof
let y be Element of R;
assume y in Y;
then consider i1 being Element of N such that
A3: y = N.i1 and
A4: i1 >= j0;
reconsider i19 = i1 as Element of N;
N.i19 in uparrow q by A1,A4;
hence q9 <= y by A3,WAYBEL_0:18;
end;
then "/\"(Y,R) >= q9 by YELLOW_0:33;
hence thesis by A2,YELLOW_0:def 2;
end;
definition
let R be reflexive non empty RelStr, N be non empty NetStr over R;
redefine attr N is monotone means :: redefines monotone (WAYBEL_0, definition)
:Def9:
for i,j being Element of N st i <= j holds N.i <= N.j;
compatibility
proof
hereby
assume N is monotone;
then
A1: netmap(N,R) is monotone;
let i,j be Element of N;
assume i <= j;
hence N.i <= N.j by A1;
end;
assume
A2: for i,j being Element of N st i <= j holds N.i <= N.j;
netmap(N,R) is monotone
proof
let x,y be Element of N;
A3: netmap(N,R).x = N.x;
A4: netmap(N,R).y = N.y;
assume x <= y;
hence netmap(N,R).x <= netmap(N,R).y by A2,A3,A4;
end;
hence thesis;
end;
end;
definition
let R be non empty RelStr;
let S be non empty set, f be Function of S, the carrier of R;
func Net-Str(S,f) -> strict non empty NetStr over R means
:Def10:
the carrier of it = S & the mapping of it = f &
for i,j being Element of it holds i <= j iff it.i <= it.j;
existence
proof
defpred P[Element of S, Element of S] means f.$1 <= f.$2;
consider R being Relation of S,S such that
A1: for x,y being Element of S holds [x,y] in R iff P[x,y] from RELSET_1:sch 2;
take N = NetStr(#S,R,f#);
thus the carrier of N = S;
thus the mapping of N = f;
let i,j be Element of N;
reconsider x = i, y = j as Element of S;
[x,y] in the InternalRel of N iff f.x <= f.y by A1;
hence thesis by ORDERS_2:def 5;
end;
uniqueness
proof
let it1,it2 be strict non empty NetStr over R such that
A2: the carrier of it1 = S and
A3: the mapping of it1 = f and
A4: for i,j being Element of it1 holds i <= j iff it1.i <= it1.j and
A5: the carrier of it2 = S and
A6: the mapping of it2 = f and
A7: for i,j being Element of it2 holds i <= j iff it2.i <= it2.j;
the InternalRel of it1 = the InternalRel of it2
proof
let x,y be object;
hereby
assume
A8: [x,y] in the InternalRel of it1;
then reconsider i=x, j=y as Element of it1 by ZFMISC_1:87;
reconsider i9=x, j9=y as Element of it2 by A2,A5,A8,ZFMISC_1:87;
A9: it1.i = it2.i9 by A3,A6;
A10: it1.j = it2.j9 by A3,A6;
i <= j by A8,ORDERS_2:def 5;
then it2.i9 <= it2.j9 by A4,A9,A10;
then i9 <= j9 by A7;
hence [x,y] in the InternalRel of it2 by ORDERS_2:def 5;
end;
assume
A11: [x,y] in the InternalRel of it2;
then reconsider i=x, j=y as Element of it2 by ZFMISC_1:87;
reconsider i9=x, j9=y as Element of it1 by A2,A5,A11,ZFMISC_1:87;
A12: it2.i = it1.i9 by A3,A6;
A13: it2.j = it1.j9 by A3,A6;
i <= j by A11,ORDERS_2:def 5;
then it1.i9 <= it1.j9 by A7,A12,A13;
then i9 <= j9 by A4;
hence thesis by ORDERS_2:def 5;
end;
hence thesis by A2,A3,A5,A6;
end;
end;
theorem Th19:
for L being non empty 1-sorted, N being non empty NetStr over L
holds rng the mapping of N =
the set of all N.i where i is Element of N
proof
let L be non empty 1-sorted, N be non empty NetStr over L;
set X = the set of all N.i where i is Element of N;
A1: the carrier of N = dom the mapping of N by FUNCT_2:def 1;
thus rng the mapping of N c=
the set of all N.i where i is Element of N
proof
let e be object;
assume e in rng the mapping of N;
then consider u being object such that
A2: u in dom the mapping of N and
A3: e = (the mapping of N).u by FUNCT_1:def 3;
reconsider u as Element of N by A2;
e = N.u by A3;
hence thesis;
end;
let e be object;
assume e in X;
then ex i being Element of N st ( e = N.i);
hence thesis by A1,FUNCT_1:def 3;
end;
theorem Th20:
for R being non empty RelStr,
S being non empty set, f be Function of S, the carrier of R
st rng f is directed holds Net-Str(S,f) is directed
proof
let R be non empty RelStr,
S be non empty set, f be Function of S, the carrier of R such that
A1: rng f is directed;
set N = Net-Str(S,f);
let x,y be Element of N;
f = the mapping of N by Def10;
then
A2: rng f = the set of all N.i where i is Element of N by Th19;
then
A3: N.x in rng f;
N.y in rng f by A2;
then consider p being Element of R such that
A4: p in rng f and
A5: N.x <= p and
A6: N.y <= p by A1,A3;
consider z being object such that
A7: z in dom f and
A8: p = f.z by A4,FUNCT_1:def 3;
reconsider z as Element of N by A7,Def10;
take z;
p = N.z by A8,Def10;
hence thesis by A5,A6,Def10;
end;
registration
let R be non empty RelStr;
let S be non empty set, f be Function of S, the carrier of R;
cluster Net-Str(S,f) -> monotone;
coherence
proof
set N = Net-Str(S,f);
netmap(N,R) is monotone
proof
let x,y be Element of N;
A1: netmap(N,R).x = N.x;
A2: netmap(N,R).y = N.y;
assume x <= y;
hence netmap(N,R).x <= netmap(N,R).y by A1,A2,Def10;
end;
hence thesis;
end;
end;
registration
let R be transitive non empty RelStr;
let S be non empty set, f be Function of S, the carrier of R;
cluster Net-Str(S,f) -> transitive;
coherence
proof
set N = Net-Str(S,f);
let x,y,z be Element of N;
assume that
A1: x <= y and
A2: y <= z;
A3: N.x <= N.y by A1,Def10;
N.y <= N.z by A2,Def10;
then N.x <= N.z by A3,YELLOW_0:def 2;
hence thesis by Def10;
end;
end;
registration
let R be reflexive non empty RelStr;
let S be non empty set, f be Function of S, the carrier of R;
cluster Net-Str(S,f) -> reflexive;
coherence
proof
let x be Element of Net-Str(S,f);
Net-Str(S,f).x <= Net-Str(S,f).x;
hence thesis by Def10;
end;
end;
theorem Th21:
for R being non empty transitive RelStr,
S being non empty set, f be Function of S, the carrier of R
st S c= the carrier of R & Net-Str(S,f) is directed
holds Net-Str(S,f) in NetUniv R
proof
let R be non empty transitive RelStr,
S be non empty set, f be Function of S, the carrier of R such that
A1: S c= the carrier of R and
A2: Net-Str(S,f) is directed;
reconsider N = Net-Str(S,f) as strict net of R by A2;
set UN = the_universe_of the carrier of R;
reconsider UN as universal set;
the_transitive-closure_of the carrier of R in UN by CLASSES1:2;
then the carrier of R in UN by CLASSES1:3,52;
then
A3: S in UN by A1,CLASSES1:def 1;
the carrier of N = S by Def10;
hence thesis by A3,YELLOW_6:def 11;
end;
registration
let R be LATTICE;
cluster monotone reflexive strict for net of R;
existence
proof
reconsider f = id the carrier of R
as Function of the carrier of R, the carrier of R;
rng f = [#]R by RELAT_1:45;
then reconsider N = Net-Str(the carrier of R,f) as strict reflexive net of
R by Th20;
take N;
thus thesis;
end;
end;
defpred P[set] means not contradiction;
theorem Th22:
for R being complete LATTICE, N being monotone reflexive net of R
holds lim_inf N = sup N
proof
let R be complete LATTICE, N be monotone reflexive net of R;
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]};
deffunc G(Element of N) = N.$1;
A1: for j being Element of N holds G(j) = F(j)
proof
let j be Element of N;
set Y = {N.i where i is Element of N: i >= j};
A2: 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 Def9;
end;
for b being Element of R st b is_<=_than Y holds N.j >= b
proof
let b be Element of R;
assume
A3: b is_<=_than Y;
reconsider j9 = j as Element of N;
j9 <= j9;
then N.j9 in Y;
hence thesis by A3;
end;
hence thesis by A2,YELLOW_0:33;
end;
rng the mapping of N = { G(j) where j is Element of N: P[j]} by Th19
.= 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 Th23:
for R being complete LATTICE, N being constant net of R
holds the_value_of N = lim_inf N
proof
let R be complete LATTICE, N be constant net of R;
set X = the set of all "/\"({N.i where i is Element of N:
i >= j},R) where j is Element of N;
set j = the Element of N;
A1: N.j is_>=_than X
proof
let b be Element of R;
assume b in X;
then consider j0 being Element of N such that
A2: b = "/\"({N.i where i is Element of N: i >= j0},R);
reconsider j0 as Element of N;
consider i0 being Element of N such that
A3: i0 >= j0 and i0 >= j0 by YELLOW_6:def 3;
A4: N.i0 in {N.i where i is Element of N: i >= j0} by A3;
N.i0 = the_value_of N by YELLOW_6:16
.= N.j by YELLOW_6:16;
hence thesis by A2,A4,YELLOW_2:22;
end;
A5: for b being Element of R st b is_>=_than X holds N.j <= b
proof
let b be Element of R;
set Y = {N.i where i is Element of N: i >= j};
A6: "/\"(Y,R) in X;
assume b is_>=_than X;
then
A7: b >= "/\"(Y,R) by A6;
A8: N.j is_<=_than Y
proof
let c be Element of R;
assume c in Y;
then consider i0 being Element of N such that
A9: c = N.i0 and i0 >= j;
N.j = the_value_of N by YELLOW_6:16
.= N.i0 by YELLOW_6:16;
hence N.j <= c by A9;
end;
for b being Element of R st b is_<=_than Y holds N.j >= b
proof
let c be Element of R;
consider i0 being Element of N such that
A10: i0 >= j and i0 >= j by YELLOW_6:def 3;
A11: N.i0 in Y by A10;
assume
A12: c is_<=_than Y;
N.j = the_value_of N by YELLOW_6:16
.= N.i0 by YELLOW_6:16;
hence thesis by A11,A12;
end;
hence thesis by A7,A8,YELLOW_0:33;
end;
thus the_value_of N = N.j by YELLOW_6:16
.= lim_inf N by A1,A5,YELLOW_0:32;
end;
theorem Th24:
for R being complete LATTICE, N being constant net of R
holds the_value_of N is_S-limit_of N
by Th23;
definition
let S be non empty 1-sorted, e be Element of S;
func Net-Str e -> strict NetStr over S means
:Def11:
the carrier of it = {e} & the InternalRel of it = {[e,e]} &
the mapping of it = id {e};
existence
proof
e in {e} by TARSKI:def 1;
then reconsider r = {[e,e]} as Relation of {e} by RELSET_1:3;
A1: dom id{e} = {e} by RELAT_1:45;
rng id{e} = {e} by RELAT_1:45;
then reconsider f = id{e} as Function of {e}, the carrier of S
by A1,RELSET_1:4;
take NetStr(#{e},r,f#);
thus thesis;
end;
uniqueness;
end;
registration
let S be non empty 1-sorted, e be Element of S;
cluster Net-Str e -> non empty;
coherence
proof
set N = Net-Str e;
the carrier of N = {e} by Def11;
hence the carrier of N is non empty;
end;
end;
theorem Th25:
for S being non empty 1-sorted, e being Element of S,
x being Element of Net-Str e holds x = e
proof
let S be non empty 1-sorted, e be Element of S, x be Element of Net-Str e;
the carrier of Net-Str e = {e} by Def11;
hence thesis by TARSKI:def 1;
end;
theorem Th26:
for S being non empty 1-sorted, e being Element of S,
x being Element of Net-Str e holds (Net-Str e).x = e
proof
let S be non empty 1-sorted, e be Element of S, x be Element of Net-Str e;
set N = Net-Str e;
A1: the carrier of Net-Str e = {e} by Def11;
then
A2: x = e by TARSKI:def 1;
thus N.x = (id{e}).x by Def11
.= e by A1,A2;
end;
registration
let S be non empty 1-sorted, e be Element of S;
cluster Net-Str e -> reflexive transitive directed antisymmetric;
coherence
proof
set N = Net-Str e;
the carrier of N = {e} by Def11;
then reconsider e as Element of N by TARSKI:def 1;
the InternalRel of N = {[e,e]} by Def11;
then
A1: [e,e] in the InternalRel of N by TARSKI:def 1;
thus N is reflexive
proof
let x be Element of N;
x = e by Th25;
hence thesis by A1,ORDERS_2:def 5;
end;
thus N is transitive
proof
let x,y,z be Element of N such that x <= y and y <= z;
A2: x = e by Th25;
z = e by Th25;
hence thesis by A1,A2,ORDERS_2:def 5;
end;
thus N is directed
proof
let x,y be Element of N;
take e;
A3: x = e by Th25;
y = e by Th25;
hence thesis by A1,A3,ORDERS_2:def 5;
end;
let x,y be Element of N such that x <= y and y <= x;
x = e by Th25;
hence thesis by Th25;
end;
end;
theorem Th27:
for S being non empty 1-sorted, e being Element of S, X being set holds
Net-Str e is_eventually_in X iff e in X
proof
let S be non empty 1-sorted, e be Element of S, X be set;
set N = Net-Str e;
the carrier of N = {e} by Def11;
then reconsider d = e as Element of N by TARSKI:def 1;
hereby
assume N is_eventually_in X;
then consider x being Element of N such that
A1: for y being Element of N st x <= y holds N.y in X;
N.x in X by A1;
hence e in X by Th26;
end;
assume
A2: e in X;
take d;
let j be Element of N such that d <= j;
thus thesis by A2,Th26;
end;
theorem Th28:
for S being reflexive antisymmetric non empty RelStr, e being Element of S
holds e = lim_inf Net-Str e
proof
let S be reflexive antisymmetric non empty RelStr, e be Element of S;
set N = Net-Str e, X = the set of all "/\"({N.i where i is Element of N:
i >= j},S) where j is Element of N;
reconsider e9 = e as Element of S;
A1: X c= {e9}
proof
let u be object;
assume u in X;
then consider j being Element of N such that
A2: u = "/\"({N.i where i is Element of N: i >= j},S);
set Y = {N.i where i is Element of N: i >= j};
A3: Y c= {e9}
proof
let v be object;
assume v in Y;
then consider i being Element of N such that
A4: v = N.i and i >= j;
reconsider i9 = i as Element of N;
N.i9 = e by Th26;
hence thesis by A4,TARSKI:def 1;
end;
reconsider j9 = j as Element of N;
j9 <= j9;
then N.j in Y;
then Y = {e9} by A3,ZFMISC_1:33;
then u = e9 by A2,YELLOW_0:39;
hence thesis by TARSKI:def 1;
end;
set j = the Element of N;
"/\"({N.i where i is Element of N: i >= j},S) in X;
then X = {e9} by A1,ZFMISC_1:33;
hence thesis by YELLOW_0:39;
end;
theorem Th29:
for S being non empty reflexive RelStr, e being Element of S
holds Net-Str e in NetUniv S
proof
let S be non empty reflexive RelStr, e be Element of S;
set N = Net-Str e, UN = the_universe_of the carrier of S;
A1: the carrier of N = {e} by Def11;
reconsider UN as universal set;
the_transitive-closure_of the carrier of S in UN by CLASSES1:2;
then the carrier of S in UN by CLASSES1:3,52;
then the carrier of N in the_universe_of the carrier of S by A1,
CLASSES1:def 1;
hence thesis by YELLOW_6:def 11;
end;
theorem Th30:
for R being complete LATTICE, 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 LATTICE, 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;
set E1 = {Z.k where k is Element of Z: k >= jx},
Ey = {Z.k where k is Element of Z: k >= jy},
E = {Z.k where k is Element of Z: k >= j};
take z = "/\"({Z.k where k is Element of Z: k >= j},R);
thus z in D by A1;
E c= E1
proof
let e be object;
assume e in E;
then consider k being Element of Z such that
A6: e = Z.k and
A7: k >= j;
reconsider k as Element of Z;
k >= jx by A4,A7,YELLOW_0:def 2;
hence thesis by A6;
end;
hence x <= z by A2,WAYBEL_7:1;
E c= Ey
proof
let e be object;
assume e in E;
then consider k being Element of Z such that
A8: e = Z.k and
A9: k >= j;
reconsider k as Element of Z;
k >= jy by A5,A9,YELLOW_0:def 2;
hence thesis by A8;
end;
hence y <= z by A3,WAYBEL_7:1;
end;
theorem Th31: :: 1.2. Lemma, p.99
for L being complete LATTICE for S being Subset of L
holds S in the topology of ConvergenceSpace Scott-Convergence L
iff S is inaccessible upper
proof
let L be complete LATTICE;
set SC = Scott-Convergence L, T = ConvergenceSpace SC;
A1: the topology of T = { V where V is Subset of L:
for p being Element of L st p in V
for N being net of L st [N,p] in SC holds N is_eventually_in V}
by YELLOW_6:def 24;
let S be Subset of L;
hereby
assume S in the topology of T;
then
A2: ex V being Subset of L st ( S = V)&( for p being Element of
L st p in V for N being net of L 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 L 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 L
by A4,RELSET_1:4;
reconsider N = Net-Str(D,f) as strict monotone reflexive net of L
by A5,Th20;
A6: N in NetUniv L by Th21;
lim_inf N = sup N by Th22
.= Sup the mapping of N by WAYBEL_2:def 1
.= "\/"(rng the mapping of N,L) by YELLOW_2:def 5
.= "\/"(rng f,L) by Def10
.= sup D by RELAT_1:45;
then sup D is_S-limit_of N;
then [N,sup D] in SC by A6,Def8;
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 Def10;
N.j0 = (id D).j0 by Def10
.= j0 by A10;
hence thesis by A9,A10,XBOOLE_0:3;
end;
thus S is upper
proof
let x,y be Element of L such that
A11: x in S and
A12: x <= y;
A13: Net-Str y in NetUniv L by Th29;
y = lim_inf Net-Str y by Th28;
then x is_S-limit_of Net-Str y by A12;
then [Net-Str y,x] in SC by A13,Def8;
then Net-Str y is_eventually_in S by A2,A11;
hence thesis by Th27;
end;
end;
assume that
A14: S is inaccessible and
A15: S is upper;
for p being Element of L st p in S
for N being net of L st [N,p] in SC holds N is_eventually_in S
proof
let p be Element of L such that
A16: p in S;
reconsider p9 = p as Element of L;
let N be net of L;
assume
A17: [N,p] in SC;
SC c= [:NetUniv L, the carrier of L:] by YELLOW_6:def 18;
then
A18: N in NetUniv L by A17,ZFMISC_1:87;
then ex N9 being strict net of L st N9 = N & the carrier of N9 in
the_universe_of the carrier of L by YELLOW_6:def 11;
then p is_S-limit_of N by A17,A18,Def8;
then
A19: p9 <= lim_inf N;
deffunc F(Element of N) = "/\"({N.i where i is Element of N: i >= $1},L);
set X ={F(j) where j is Element of N: P[j]};
X is Subset of L from DOMAIN_1:sch 8;
then reconsider D = X as Subset of L;
reconsider D as non empty directed Subset of L by Th30;
sup D in S by A15,A16,A19;
then D meets S by A14;
then D /\ S <> {};
then consider d being Element of L such that
A20: d in D /\ S by SUBSET_1:4;
reconsider d as Element of L;
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},L);
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 {N.i where i is Element of N: i >= j};
then d <= N.i0 by A21,YELLOW_2:22;
hence thesis by A15,A22;
end;
hence thesis by A1;
end;
theorem Th32:
for T being complete Scott TopLattice
holds the TopStruct of T = ConvergenceSpace Scott-Convergence T
proof
let T be complete Scott TopLattice;
set CSC = ConvergenceSpace Scott-Convergence T;
the topology of T = the topology of CSC
proof
thus the topology of T c= the topology of CSC
proof
let e be object;
assume
A1: e in the topology of T;
then reconsider A = e as Subset of T;
A is open by A1;
then A is inaccessible upper by Def4;
hence thesis by Th31;
end;
let e be object;
assume
A2: e in the topology of CSC;
then reconsider A = e as Subset of T by YELLOW_6:def 24;
A is inaccessible upper by A2,Th31;
then A is open by Def4;
hence thesis;
end;
hence thesis by YELLOW_6:def 24;
end;
theorem Th33:
for T being complete TopLattice
st the TopStruct of T = ConvergenceSpace Scott-Convergence T
for S being Subset of T holds S is open iff S is inaccessible upper
proof
let T be complete TopLattice;
set SC = Scott-Convergence T;
assume the TopStruct of T = ConvergenceSpace SC;
then
A1: the topology of T = { V where V is Subset of T:
for p being Element of T st p in V
for N being net of T st [N,p] in SC holds N is_eventually_in V}
by YELLOW_6:def 24;
let S be Subset of T;
hereby
assume S is open;
then S in the topology of T;
then
A2: ex V being Subset of T st ( S = V)&( for p being Element of
T st p in V for N being net of T 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 T 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 T
by A4,RELSET_1:4;
reconsider N = Net-Str(D,f) as strict monotone reflexive net of T
by A5,Th20;
A6: N in NetUniv T by Th21;
lim_inf N = sup N by Th22
.= Sup the mapping of N by WAYBEL_2:def 1
.= "\/"(rng the mapping of N,T) by YELLOW_2:def 5
.= "\/"(rng f,T) by Def10
.= sup D by RELAT_1:45;
then sup D is_S-limit_of N;
then [N,sup D] in SC by A6,Def8;
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 Def10;
N.j0 = (id D).j0 by Def10
.= j0 by A10;
hence thesis by A9,A10,XBOOLE_0:3;
end;
thus S is upper
proof
let x,y be Element of T such that
A11: x in S and
A12: x <= y;
A13: Net-Str y in NetUniv T by Th29;
y = lim_inf Net-Str y by Th28;
then x is_S-limit_of Net-Str y by A12;
then [Net-Str y,x] in SC by A13,Def8;
then Net-Str y is_eventually_in S by A2,A11;
hence thesis by Th27;
end;
end;
assume that
A14: S is inaccessible and
A15: S is upper;
for p being Element of T st p in S
for N being net of T st [N,p] in SC holds N is_eventually_in S
proof
let p be Element of T such that
A16: p in S;
reconsider p9 = p as Element of T;
let N be net of T;
assume
A17: [N,p] in SC;
SC c= [:NetUniv T, the carrier of T:] by YELLOW_6:def 18;
then
A18: N in NetUniv T by A17,ZFMISC_1:87;
then ex N9 being strict net of T st N9 = N & the carrier of N9 in
the_universe_of the carrier of T by YELLOW_6:def 11;
then p is_S-limit_of N by A17,A18,Def8;
then
A19: p9 <= lim_inf N;
deffunc F(Element of N) = "/\"({N.i where i is Element of N: i >= $1},T);
set X ={F(j) where j is Element of N: P[j]};
X is Subset of T from DOMAIN_1:sch 8;
then reconsider D = X as Subset of T;
reconsider D as non empty directed Subset of T by Th30;
sup D in S by A15,A16,A19;
then D meets S by A14;
then D /\ S <> {};
then consider d being Element of T such that
A20: d in D /\ S by SUBSET_1:4;
reconsider d as Element of T;
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},T);
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 {N.i where i is Element of N: i >= j};
then d <= N.i0 by A21,YELLOW_2:22;
hence thesis by A15,A22;
end;
then S in the topology of T by A1;
hence thesis;
end;
theorem Th34:
for T being complete TopLattice
st the TopStruct of T = ConvergenceSpace Scott-Convergence T
holds T is Scott
by Th33;
registration
let R be complete LATTICE;
:: 1.6. Proposition (i)
cluster Scott-Convergence R -> (CONSTANTS);
coherence
proof
let N be constant net of R;
assume
A1: N in NetUniv R;
then consider M being strict net of R such that
A2: M = N and the carrier of M in the_universe_of the carrier of R
by YELLOW_6:def 11;
the_value_of M is_S-limit_of M by A2,Th24;
hence thesis by A1,A2,Def8;
end;
end;
registration
let R be complete LATTICE;
:: 1.6. Proposition (i)
cluster Scott-Convergence R -> (SUBNETS);
coherence
proof
set S = Scott-Convergence R;
let N be net of R, Y be subnet of N;
A1: S c= [:NetUniv R,the carrier of R:] by YELLOW_6:def 18;
assume
A2: Y in NetUniv R;
then consider Y9 being strict net of R such that
A3: Y9 = Y and the carrier of Y9 in the_universe_of the carrier of R
by YELLOW_6:def 11;
let p be Element of R;
assume
A4: [N,p] in S;
then
A5: N in NetUniv R by A1,ZFMISC_1:87;
then consider N9 being strict net of R such that
A6: N9 = N and the carrier of N9 in the_universe_of the carrier of R
by YELLOW_6:def 11;
deffunc F(Element of N) = "/\"({N.i where i is Element of N: i >= $1},R);
reconsider X1 = {F(j) where j is Element of N: P[j]}
as Subset of R from DOMAIN_1:sch 8;
deffunc G(Element of Y) = "/\"({Y.i where i is Element of Y: i >= $1},R);
reconsider X2 = {G(j) where j is Element of Y: P[j]}
as Subset of R from DOMAIN_1:sch 8;
p is_S-limit_of N9 by A4,A5,A6,Def8;
then
A7: p <= lim_inf N by A6;
consider f being Function of Y, N such that
A8: the mapping of Y = (the mapping of N)*f and
A9: for m being Element of N ex n being Element of Y st
for p being Element of Y st n <= p holds m <= f.p by YELLOW_6:def 9;
X1 is_finer_than X2
proof
let a be Element of R;
assume a in X1;
then consider j being Element of N such that
A10: a = "/\"({N.i where i is Element of N: i >= j},R);
reconsider j as Element of N;
consider n being Element of Y such that
A11: for p being Element of Y st n <= p holds j <= f.p by A9;
set X3 = {Y.i where i is Element of Y: i >= n},
X4 = {N.i where i is Element of N: i >= j};
take b = "/\"(X3,R);
thus b in X2;
X3 c= X4
proof
let u be object;
assume u in X3;
then consider m being Element of Y such that
A12: u = Y.m and
A13: m >= n;
reconsider m as Element of Y;
A14: f.m >= j by A11,A13;
u = N.(f.m) by A8,A12,FUNCT_2:15;
hence thesis by A14;
end;
hence a <= b by A10,WAYBEL_7:1;
end;
then "\/"(X1,R) <= "\/"(X2,R) by Th2;
then p <= lim_inf Y by A7,YELLOW_0:def 2;
then p is_S-limit_of Y9 by A3;
hence thesis by A2,A3,Def8;
end;
end;
theorem Th35: :: YELLOW_6:32
for S being non empty 1-sorted, N being net of S, X being set
for M being subnet of N st M = N"X for i being Element of M holds M.i in X
proof
let S be non empty 1-sorted, N be net of S, X be set;
let M be subnet of N such that
A1: M = N"X;
let j be Element of M;
j in the carrier of M;
then j in (the mapping of N)"X by A1,YELLOW_6:def 10;
then
A2: (the mapping of N).j in X by FUNCT_1:def 7;
the mapping of M = (the mapping of N)|the carrier of M by A1,YELLOW_6:def 6;
hence thesis by A2,FUNCT_1:49;
end;
definition
let L be non empty reflexive RelStr;
func sigma L -> Subset-Family of L equals
the topology of ConvergenceSpace Scott-Convergence L;
coherence by YELLOW_6:def 24;
end;
theorem Th36: :: 1.5 Examples (5), p.100
for L being continuous complete Scott TopLattice, x be Element of L
holds wayabove x is open
proof
let L be continuous complete Scott TopLattice, x be Element of L;
set W = wayabove x;
W is inaccessible
proof
let D be non empty directed Subset of L;
assume sup D in W;
then x << sup D by WAYBEL_3:8;
then consider d being Element of L such that
A1: d in D and
A2: x << d by WAYBEL_4:53;
d in W by A2;
hence thesis by A1,XBOOLE_0:3;
end;
hence thesis by Def4;
end;
theorem Th37:
for T being complete TopLattice st the topology of T = sigma T
holds T is Scott
proof
let T be complete TopLattice;
set CSC = ConvergenceSpace Scott-Convergence T;
assume the topology of T = sigma T;
then the TopStruct of T =
TopStruct(#the carrier of CSC, the topology of CSC#) by YELLOW_6:def 24;
hence thesis by Th34;
end;
:: non automated structural loci :
Lm3: for T1,T2 being TopStruct
st the TopStruct of T1 = the TopStruct of T2 & T1 is TopSpace-like
holds T2 is TopSpace-like;
Lm4: for
S1,S2 being non empty 1-sorted st the carrier of S1 = the carrier of S2
for N being strict net of S1 holds N is strict net of S2;
Lm5: for
S1,S2 being non empty 1-sorted st the carrier of S1 = the carrier of S2
holds NetUniv S1 = NetUniv S2
proof
let S1,S2 be non empty 1-sorted;
assume
A1: the carrier of S1 = the carrier of S2;
defpred P[set] means ex N being strict net of S2 st
N = $1 & the carrier of N in the_universe_of the carrier of S2;
A2: now
let x be set;
hereby
assume x in NetUniv S1;
then consider N being strict net of S1 such that
A3: N = x and
A4: the carrier of N in the_universe_of the carrier of S1 by YELLOW_6:def 11;
reconsider N as strict net of S2 by A1;
thus P[x]
proof
take N;
thus thesis by A1,A3,A4;
end;
end;
assume P[x];
then consider N being strict net of S2 such that
A5: N = x and
A6: the carrier of N in the_universe_of the carrier of S2;
reconsider N as strict net of S1 by A1;
now
take N;
thus N = x & the carrier of N in the_universe_of the carrier of S1
by A1,A5,A6;
end;
hence x in NetUniv S1 by YELLOW_6:def 11;
end;
A7: for x being set holds x in NetUniv S2 iff P[x] by YELLOW_6:def 11;
thus NetUniv S1 = NetUniv S2 from XFAMILY:sch 2(A2,A7);
end;
Lm6: for T1,T2 being non empty 1-sorted, X be set
for N1 being net of T1, N2 being net of T2 st N1 = N2 & N1 is_eventually_in X
holds N2 is_eventually_in X
proof
let T1,T2 be non empty 1-sorted, X be set;
let N1 be net of T1, N2 be net of T2 such that
A1: N1 = N2;
assume N1 is_eventually_in X;
then consider i being Element of N1 such that
A2: for j being Element of N1 st i <= j holds N1.j in X;
reconsider ii = i as Element of N2 by A1;
take ii;
let jj be Element of N2;
reconsider j = jj as Element of N1 by A1;
assume
A3: ii <= jj;
N2.jj = N1.j by A1;
hence thesis by A1,A2,A3;
end;
Lm7: for T1,T2 being non empty TopSpace
st the TopStruct of T1 = the TopStruct of T2
for N1 being net of T1, N2 being net of T2 st N1 = N2
for p1 being Point of T1, p2 being Point of T2 st p1 = p2 & p1 in Lim N1
holds p2 in Lim N2
proof
let T1,T2 be non empty TopSpace such that
A1: the TopStruct of T1 = the TopStruct of T2;
let N1 be net of T1, N2 be net of T2 such that
A2: N1 = N2;
let p1 be Point of T1, p2 be Point of T2 such that
A3: p1 = p2 and
A4: p1 in Lim N1;
for V being a_neighborhood of p2 holds N2 is_eventually_in V
proof
let V be a_neighborhood of p2;
reconsider W = V as Subset of T1 by A1;
p2 in Int V by CONNSP_2:def 1;
then consider G being Subset of T2 such that
A5: G is open and
A6: G c= V and
A7: p2 in G by TOPS_1:22;
reconsider H = G as Subset of T1 by A1;
G in the topology of T2 by A5;
then H is open by A1;
then p1 in Int W by A3,A6,A7,TOPS_1:22;
then reconsider W = V as a_neighborhood of p1 by CONNSP_2:def 1;
thus N2 is_eventually_in V
proof
N1 is_eventually_in W by A4,YELLOW_6:def 15;
then consider i being Element of N1 such that
A8: for j being Element of N1 st i <= j holds N1.j in W;
reconsider ii = i as Element of N2 by A2;
take ii;
let jj be Element of N2;
reconsider j = jj as Element of N1 by A2;
assume
A9: ii <= jj;
N2.jj = N1.j by A2;
hence thesis by A2,A8,A9;
end;
end;
hence thesis by YELLOW_6:def 15;
end;
Lm8: for T1,T2 being non empty TopSpace
st the TopStruct of T1 = the TopStruct of T2
holds Convergence T1 = Convergence T2
proof
let T1,T2 be non empty TopSpace such that
A1: the TopStruct of T1 = the TopStruct of T2;
A2: Convergence T1 c= [:NetUniv T1,the carrier of T1:] by YELLOW_6:def 18;
A3: Convergence T2 c= [:NetUniv T2,the carrier of T2:] by YELLOW_6:def 18;
let u1,u2 be object;
hereby
assume
A4: [u1,u2] in Convergence T1;
then consider N1 being Element of NetUniv T1, p1 being Point of T1
such that
A5: [u1,u2] = [N1,p1] by A2,DOMAIN_1:1;
A6: N1 in NetUniv T1;
ex N being strict net of T1 st N = N1 &
the carrier of N in the_universe_of the carrier of T1 by YELLOW_6:def 11;
then reconsider N1 as net of T1;
A7: p1 in Lim N1 by A4,A5,YELLOW_6:def 19;
reconsider N2 = N1 as net of T2 by A1;
reconsider p2 =p1 as Point of T2 by A1;
A8: N2 in NetUniv T2 by A1,A6,Lm5;
p2 in Lim N2 by A1,A7,Lm7;
hence [u1,u2] in Convergence T2 by A5,A8,YELLOW_6:def 19;
end;
assume
A9: [u1,u2] in Convergence T2;
then consider N1 being Element of NetUniv T2, p1 being Point of T2 such that
A10: [u1,u2] = [N1,p1] by A3,DOMAIN_1:1;
A11: N1 in NetUniv T2;
ex N being strict net of T2 st N = N1 &
the carrier of N in the_universe_of the carrier of T2 by YELLOW_6:def 11;
then reconsider N1 as net of T2;
A12: p1 in Lim N1 by A9,A10,YELLOW_6:def 19;
reconsider N2 = N1 as net of T1 by A1;
reconsider p2 =p1 as Point of T1 by A1;
A13: N2 in NetUniv T1 by A1,A11,Lm5;
p2 in Lim N2 by A1,A12,Lm7;
hence thesis by A10,A13,YELLOW_6:def 19;
end;
Lm9: for R1,R2 being non empty RelStr
st the RelStr of R1 = the RelStr of R2 & R1 is LATTICE holds R2 is LATTICE
proof
let R1,R2 be non empty RelStr such that
A1: the RelStr of R1 = the RelStr of R2 and
A2: R1 is LATTICE;
A3: R2 is with_infima
proof
let x,y be Element of R2;
reconsider x9 = x, y9 = y as Element of R1 by A1;
consider z9 being Element of R1 such that
A4: z9 <= x9 and
A5: z9 <= y9 and
A6: for w9 being Element of R1 st w9 <= x9 & w9 <= y9 holds w9 <= z9
by A2,LATTICE3:def 11;
reconsider z = z9 as Element of R2 by A1;
take z;
thus z <= x & z <= y by A1,A4,A5,Lm1;
let w be Element of R2;
reconsider w9 = w as Element of R1 by A1;
assume that
A7: w <= x and
A8: w <= y;
A9: w9 <= x9 by A1,A7,Lm1;
w9 <= y9 by A1,A8,Lm1;
then w9 <= z9 by A6,A9;
hence thesis by A1,Lm1;
end;
A10: R2 is with_suprema
proof
let x,y be Element of R2;
reconsider x9 = x, y9 = y as Element of R1 by A1;
consider z9 being Element of R1 such that
A11: z9 >= x9 and
A12: z9 >= y9 and
A13: for w9 being Element of R1 st w9 >= x9 & w9 >= y9 holds w9 >= z9
by A2,LATTICE3:def 10;
reconsider z = z9 as Element of R2 by A1;
take z;
thus z >= x & z >= y by A1,A11,A12,Lm1;
let w be Element of R2;
reconsider w9 = w as Element of R1 by A1;
assume that
A14: w >= x and
A15: w >= y;
A16: w9 >= x9 by A1,A14,Lm1;
w9 >= y9 by A1,A15,Lm1;
then w9 >= z9 by A13,A16;
hence thesis by A1,Lm1;
end;
A17: R2 is reflexive
by A1,A2,YELLOW_0:def 1,Lm1;
A18: R2 is transitive
proof
let x,y,z be Element of R2;
reconsider x9 = x, y9 = y, z9 = z as Element of R1 by A1;
assume that
A19: x <= y and
A20: y <= z;
A21: x9 <= y9 by A1,A19,Lm1;
y9 <= z9 by A1,A20,Lm1;
then x9 <= z9 by A2,A21,YELLOW_0:def 2;
hence thesis by A1,Lm1;
end;
R2 is antisymmetric
proof
let x,y be Element of R2;
reconsider x9 = x, y9 = y as Element of R1 by A1;
assume that
A22: x <= y and
A23: y <= x;
A24: x9 <= y9 by A1,A22,Lm1;
y9 <= x9 by A1,A23,Lm1;
hence thesis by A2,A24,YELLOW_0:def 3;
end;
hence thesis by A3,A10,A17,A18;
end;
Lm10: for R1,R2 being LATTICE, X being set
st the RelStr of R1 = the RelStr of R2
for p1 being Element of R1, p2 being Element of R2 st
p1 = p2 & X is_<=_than p1 holds X is_<=_than p2
by Lm1;
Lm11: for R1,R2 being LATTICE, X being set
st the RelStr of R1 = the RelStr of R2
for p1 being Element of R1, p2 being Element of R2 st
p1 = p2 & X is_>=_than p1 holds X is_>=_than p2
by Lm1;
Lm12: for R1,R2 being complete LATTICE st the RelStr of R1 = the RelStr of R2
for D being set holds "\/"(D,R1) = "\/"(D,R2)
proof
let R1,R2 be complete LATTICE such that
A1: the RelStr of R1 = the RelStr of R2;
let D be set;
reconsider b = "\/"(D,R1) as Element of R2 by A1;
A2: ex_sup_of D,R2 by YELLOW_0:17;
A3: ex_sup_of D,R1 by YELLOW_0:17;
then D is_<=_than "\/"(D,R1) by YELLOW_0:def 9;
then
A4: D is_<=_than b by A1,Lm10;
for a being Element of R2 st D is_<=_than a holds a >= b
proof
let a be Element of R2;
reconsider a9 = a as Element of R1 by A1;
assume D is_<=_than a;
then D is_<=_than a9 by A1,Lm10;
then a9 >= "\/"(D,R1) by A3,YELLOW_0:def 9;
hence thesis by A1,Lm1;
end;
hence thesis by A2,A4,YELLOW_0:def 9;
end;
Lm13: for R1,R2 being complete LATTICE st the RelStr of R1 = the RelStr of R2
for D being set holds "/\"(D,R1) = "/\"(D,R2)
proof
let R1,R2 be complete LATTICE such that
A1: the RelStr of R1 = the RelStr of R2;
let D be set;
reconsider b = "/\"(D,R1) as Element of R2 by A1;
A2: ex_inf_of D,R2 by YELLOW_0:17;
A3: ex_inf_of D,R1 by YELLOW_0:17;
then D is_>=_than "/\"(D,R1) by YELLOW_0:def 10;
then
A4: D is_>=_than b by A1,Lm11;
for a being Element of R2 st D is_>=_than a holds a <= b
proof
let a be Element of R2;
reconsider a9 = a as Element of R1 by A1;
assume D is_>=_than a;
then D is_>=_than a9 by A1,Lm11;
then a9 <= "/\"(D,R1) by A3,YELLOW_0:def 10;
hence thesis by A1,Lm1;
end;
hence thesis by A2,A4,YELLOW_0:def 10;
end;
Lm14: for R1,R2 being non empty reflexive RelStr
st the RelStr of R1 = the RelStr of R2
for D being Subset of R1, D9 being Subset of R2 st D = D9 & D is directed
holds D9 is directed
proof
let R1,R2 be non empty reflexive RelStr such that
A1: the RelStr of R1 = the RelStr of R2;
let D be Subset of R1, D9 be Subset of R2 such that
A2: D = D9 and
A3: D is directed;
let x2,y2 be Element of R2 such that
A4: x2 in D9 and
A5: y2 in D9;
reconsider x1 = x2, y1 = y2 as Element of R1 by A1;
consider z1 being Element of R1 such that
A6: z1 in D and
A7: x1 <= z1 and
A8: y1 <= z1 by A2,A3,A4,A5;
reconsider z2 = z1 as Element of R2 by A1;
take z2;
thus z2 in D9 by A2,A6;
thus x2 <= z2 & y2 <= z2 by A1,A7,A8,Lm1;
end;
Lm15: for R1,R2 being complete LATTICE st the RelStr of R1 = the RelStr of R2
for p,q being Element of R1 st p << q
for p9,q9 being Element of R2 st p = p9 & q = q9 holds p9 << q9
proof
let R1,R2 be complete LATTICE such that
A1: the RelStr of R1 = the RelStr of R2;
let p,q be Element of R1 such that
A2: p << q;
let p9,q9 be Element of R2 such that
A3: p = p9 and
A4: q = q9;
let D9 be non empty directed Subset of R2 such that
A5: q9 <= sup D9;
reconsider D = D9 as non empty Subset of R1 by A1;
reconsider D as non empty directed Subset of R1 by A1,Lm14;
sup D = sup D9 by A1,Lm12;
then q <= sup D by A1,A4,A5,Lm1;
then consider d be Element of R1 such that
A6: d in D and
A7: p <= d by A2;
reconsider d9 = d as Element of R2 by A1;
take d9;
thus d9 in D9 by A6;
thus thesis by A1,A3,A7,Lm1;
end;
Lm16: for R1,R2 being complete LATTICE st the RelStr of R1 = the RelStr of R2
for N1 being net of R1, N2 being net of R2 st N1 = N2
holds lim_inf N1 = lim_inf N2
proof
let R1,R2 be complete LATTICE such that
A1: the RelStr of R1 = the RelStr of R2;
let N1 be net of R1, N2 be net of R2 such that
A2: N1 = N2;
set X1 = the set of all "/\"({N1.i where i is Element of N1:
i >= j},R1) where j is Element of N1;
set X2 = the set of all "/\"({N2.i where i is Element of N2:
i >= j},R2) where j is Element of N2;
X1 = X2
proof
thus X1 c= X2
proof
let e be object;
assume e in X1;
then consider j1 being Element of N1 such that
A3: e = "/\"({N1.i where i is Element of N1: i >= j1},R1);
reconsider j2 = j1 as Element of N2 by A2;
set Y1 = {N1.i where i is Element of N1: i >= j1},
Y2 = {N2.i where i is Element of N2: i >= j2};
Y1 = Y2
proof
thus Y1 c= Y2
proof
let u be object;
assume u in Y1;
then consider i1 being Element of N1 such that
A4: u = N1.i1 and
A5: j1 <= i1;
reconsider i2 = i1 as Element of N2 by A2;
N2.i2 = u by A2,A4;
hence thesis by A2,A5;
end;
let u be object;
assume u in Y2;
then consider i2 being Element of N2 such that
A6: u = N2.i2 and
A7: j2 <= i2;
reconsider i1 = i2 as Element of N1 by A2;
N1.i1 = u by A2,A6;
hence thesis by A2,A7;
end;
then e = "/\"(Y2,R2) by A1,A3,Lm13;
hence thesis;
end;
let e be object;
assume e in X2;
then consider j1 being Element of N2 such that
A8: e = "/\"({N2.i where i is Element of N2: i >= j1},R2);
reconsider j2 = j1 as Element of N1 by A2;
set Y1 = {N2.i where i is Element of N2: i >= j1},
Y2 = {N1.i where i is Element of N1: i >= j2};
Y1 = Y2
proof
thus Y1 c= Y2
proof
let u be object;
assume u in Y1;
then consider i1 being Element of N2 such that
A9: u = N2.i1 and
A10: j1 <= i1;
reconsider i2 = i1 as Element of N1 by A2;
N1.i2 = u by A2,A9;
hence thesis by A2,A10;
end;
let u be object;
assume u in Y2;
then consider i2 being Element of N1 such that
A11: u = N1.i2 and
A12: j2 <= i2;
reconsider i1 = i2 as Element of N2 by A2;
N2.i1 = u by A2,A11;
hence thesis by A2,A12;
end;
then e = "/\"(Y2,R1) by A1,A8,Lm13;
hence thesis;
end;
hence thesis by A1,Lm12;
end;
Lm17: for R1,R2 being non empty reflexive RelStr, X being non empty set
for N1 being net of R1, N2 being net of R2 st N1 = N2
for J1 being net_set of the carrier of N1,R1,
J2 being net_set of the carrier of N2,R2 st J1 = J2
holds Iterated J1 = Iterated J2
proof
let R1,R2 be non empty reflexive RelStr, X be non empty set;
let N1 be net of R1, N2 be net of R2 such that
A1: N1 = N2;
let J1 be net_set of the carrier of N1,R1,
J2 be net_set of the carrier of N2,R2 such that
A2: J1 = J2;
A3: the RelStr of Iterated J1 = [:N1, product J1:] by YELLOW_6:def 13;
A4: the RelStr of Iterated J2 = [:N2, product J2:] by YELLOW_6:def 13;
set f = the mapping of Iterated J1, g = the mapping of Iterated J2;
A5: dom f = the carrier of Iterated J2 by A1,A2,A3,A4,FUNCT_2:def 1
.= dom g by FUNCT_2:def 1;
for x being object st x in dom f holds f.x = g.x
proof
let x be object;
assume x in dom f;
then x in the carrier of Iterated J1;
then x in [:the carrier of N1, the carrier of product J1:]
by A3,YELLOW_3:def 2;
then consider x1 being Element of N1,
x2 being Element of product J1 such that
A6: x = [x1,x2] by DOMAIN_1:1;
reconsider y1 = x1 as Element of N2 by A1;
reconsider y2 = x2 as Element of product J2 by A1,A2;
thus f.x = (the mapping of Iterated J1).(x1,x2) by A6
.= (the mapping of J1.x1).(x2.x1) by YELLOW_6:def 13
.= (the mapping of J2.y1).(y2.y1) by A2
.= (the mapping of Iterated J2).(y1,y2) by YELLOW_6:def 13
.= g.x by A6;
end;
then f = g by A5,FUNCT_1:2;
hence thesis by A1,A2,A3,A4;
end;
Lm18: for R1,R2 being non empty reflexive RelStr, X being non empty set
st the RelStr of R1 = the RelStr of R2
for N1 being net of R1, N2 being net of R2 st N1 = N2
for J1 being net_set of the carrier of N1,R1
holds J1 is net_set of the carrier of N2,R2
proof
let R1,R2 be non empty reflexive RelStr, X be non empty set such that
A1: the RelStr of R1 = the RelStr of R2;
let N1 be net of R1, N2 be net of R2 such that
A2: N1 = N2;
let J1 be net_set of the carrier of N1,R1;
reconsider J2 = J1 as ManySortedSet of the carrier of N2 by A2;
for i being set st i in rng J2 holds i is net of R2
proof
let i be set;
assume i in rng J2;
then reconsider N = i as net of R1 by YELLOW_6:def 12;
N is NetStr over R2 by A1;
hence thesis;
end;
hence thesis by YELLOW_6:def 12;
end;
Lm19: for R1,R2 being complete LATTICE st the RelStr of R1 = the RelStr of R2
holds Scott-Convergence R1 c= Scott-Convergence R2
proof
let R1,R2 be complete LATTICE such that
A1: the RelStr of R1 = the RelStr of R2;
A2: Scott-Convergence R1 c= [:NetUniv R1,the carrier of R1:]
by YELLOW_6:def 18;
for e being object st e in Scott-Convergence R1
holds e in Scott-Convergence R2
proof
let e be object;
assume
A3: e in Scott-Convergence R1;
then consider N1 being Element of NetUniv R1,
p1 being Element of R1 such that
A4: e = [N1,p1] by A2,DOMAIN_1:1;
A5: N1 in NetUniv R1;
A6: ex N being strict net of R1 st ( N1 = N)&( the carrier of N
in the_universe_of the carrier of R1) by YELLOW_6:def 11;
then reconsider N2 = N1 as strict net of R2 by A1,Lm4;
reconsider N1 as strict net of R1 by A6;
reconsider p2 = p1 as Element of R2 by A1;
A7: N2 in NetUniv R2 by A1,A5,Lm5;
A8: lim_inf N1 = lim_inf N2 by A1,Lm16;
p1 is_S-limit_of N1 by A3,A4,Def8;
then p1 <= lim_inf N1;
then p2 <= lim_inf N2 by A1,A8,Lm1;
then p2 is_S-limit_of N2;
hence thesis by A4,A7,Def8;
end;
hence thesis;
end;
Lm20: for R1,R2 being complete LATTICE st the RelStr of R1 = the RelStr of R2
holds Scott-Convergence R1 = Scott-Convergence R2
by Lm19;
Lm21: for R1,R2 being complete LATTICE st the RelStr of R1 = the RelStr of R2
holds sigma R1 = sigma R2
proof
let R1,R2 be complete LATTICE;
assume
A1: the RelStr of R1 = the RelStr of R2;
set T1 = ConvergenceSpace Scott-Convergence R1,
T2 = ConvergenceSpace Scott-Convergence R2;
A2: the topology of T1 = { V where V is Subset of R1:
for p being Element of R1 st p in V
for N being net of R1 st [N,p] in Scott-Convergence R1
holds N is_eventually_in V} by YELLOW_6:def 24;
A3: the topology of T2 = { V where V is Subset of R2:
for p being Element of R2 st p in V
for N being net of R2 st [N,p] in Scott-Convergence R2
holds N is_eventually_in V} by YELLOW_6:def 24;
the topology of T1 = the topology of T2
proof
thus the topology of T1 c= the topology of T2
proof
let e be object;
assume e in the topology of T1;
then consider V1 being Subset of R1 such that
A4: e = V1 and
A5: for p being Element of R1 st p in V1
for N being net of R1 st [N,p] in Scott-Convergence R1
holds N is_eventually_in V1 by A2;
reconsider V2 = V1 as Subset of R2 by A1;
for p being Element of R2 st p in V2
for N being net of R2 st [N,p] in Scott-Convergence R2
holds N is_eventually_in V2
proof
let p2 be Element of R2 such that
A6: p2 in V2;
reconsider p1 = p2 as Element of R1 by A1;
let N2 be net of R2;
reconsider N1 = N2 as net of R1 by A1;
assume [N2,p2] in Scott-Convergence R2;
then [N1,p1] in Scott-Convergence R1 by A1,Lm20;
hence thesis by A5,A6,Lm6;
end;
hence thesis by A3,A4;
end;
let e be object;
assume e in the topology of T2;
then consider V1 being Subset of R2 such that
A7: e = V1 and
A8: for p being Element of R2 st p in V1
for N being net of R2 st [N,p] in Scott-Convergence R2
holds N is_eventually_in V1 by A3;
reconsider V2 = V1 as Subset of R1 by A1;
for p being Element of R1 st p in V2
for N being net of R1 st [N,p] in Scott-Convergence R1
holds N is_eventually_in V2
proof
let p2 be Element of R1 such that
A9: p2 in V2;
reconsider p1 = p2 as Element of R2 by A1;
let N2 be net of R1;
reconsider N1 = N2 as net of R2 by A1;
assume [N2,p2] in Scott-Convergence R1;
then [N1,p1] in Scott-Convergence R2 by A1,Lm20;
hence thesis by A8,A9,Lm6;
end;
hence thesis by A2,A7;
end;
hence thesis;
end;
Lm22: for R1,R2 being LATTICE
st the RelStr of R1 = the RelStr of R2 & R1 is complete holds R2 is complete
proof
let R1,R2 be LATTICE such that
A1: the RelStr of R1 = the RelStr of R2 and
A2: R1 is complete;
let X be set;
consider a1 being Element of R1 such that
A3: X is_<=_than a1 and
A4: for b being Element of R1 st X is_<=_than b holds a1 <= b
by A2;
reconsider a2 = a1 as Element of R2 by A1;
take a2;
thus X is_<=_than a2 by A1,A3,Lm10;
let b2 be Element of R2;
reconsider b1 = b2 as Element of R1 by A1;
assume X is_<=_than b2;
then X is_<=_than b1 by A1,Lm10;
hence a2 <= b2 by A1,A4,Lm1;
end;
Lm23: for R1,R2 being complete LATTICE
st the RelStr of R1 = the RelStr of R2 & R1 is continuous
holds R2 is continuous
proof
let R1,R2 be complete LATTICE such that
A1: the RelStr of R1 = the RelStr of R2;
assume
A2: R1 is continuous;
thus
A3: for x being Element of R2 holds waybelow x is non empty directed;
thus R2 is up-complete;
for x,y being Element of R2 st not x <= y
ex u being Element of R2 st u << x & not u <= y
proof
let x2,y2 be Element of R2;
reconsider x1=x2, y1=y2 as Element of R1 by A1;
assume not x2 <= y2;
then not x1 <= y1 by A1,Lm1;
then consider u1 be Element of R1 such that
A4: u1 << x1 and
A5: not u1 <= y1 by A2,WAYBEL_3:24;
reconsider u2 = u1 as Element of R2 by A1;
take u2;
thus u2 << x2 by A1,A4,Lm15;
thus thesis by A1,A5,Lm1;
end;
hence thesis by A3,WAYBEL_3:24;
end;
registration
let R be continuous complete LATTICE;
:: 1.6. Proposition (ii)
cluster Scott-Convergence R -> topological;
coherence
proof
set C = Scott-Convergence R;
thus C is (CONSTANTS) (SUBNETS);
thus C is (DIVERGENCE)
proof
let X be net of R, p be Element of R such that
A1: X in NetUniv R and
A2: not [X,p] in C;
A3: for x being Element of R holds waybelow x is non empty directed;
reconsider p9 = p as Element of R;
consider N being strict net of R such that
A4: N = X and the carrier of N in the_universe_of the carrier of R
by A1,YELLOW_6:def 11;
not p is_S-limit_of N by A1,A2,A4,Def8;
then not p <= lim_inf X by A4;
then consider u being Element of R such that
A5: u << p9 and
A6: not u <= lim_inf X by A3,WAYBEL_3:24;
set A = { a where a is Element of R : not a >= u};
X is_often_in A
proof
let i be Element of X;
set B = { X.j where j is Element of X: j >= i};
set C = the set of all "/\"({X.k where k is Element of X:
k >= j},R) where j is Element of X;
"/\"(B,R) in C;
then "/\"(B,R) <= lim_inf X by YELLOW_2:22;
then not u <= "/\"(B,R) by A6,YELLOW_0:def 2;
then not u is_<=_than B by YELLOW_0:33;
then consider b being Element of R such that
A7: b in B and
A8: not u <= b;
consider j being Element of X such that
A9: b = X.j and
A10: j >= i by A7;
take j;
thus i <= j by A10;
thus thesis by A8,A9;
end;
then reconsider Y = X"A as subnet of X by YELLOW_6:22;
take Y;
reconsider UN = the_universe_of the carrier of R as universal set;
A11: ex N being strict net of R st X = N &
the carrier of N in UN by A1,YELLOW_6:def 11;
X"A is SubRelStr of X by YELLOW_6:def 6;
then the carrier of X"A c= the carrier of X by YELLOW_0:def 13;
then the carrier of Y in UN by A11,CLASSES1:def 1;
hence Y in NetUniv R by YELLOW_6:def 11;
let Z be subnet of Y;
assume
A12: [Z,p] in C;
C c= [:NetUniv R,the carrier of R:] by YELLOW_6:def 18;
then
A13: Z in NetUniv R by A12,ZFMISC_1:87;
then consider ZZ being strict net of R such that
A14: ZZ = Z and the carrier of ZZ in UN by YELLOW_6:def 11;
deffunc F(Element of Z)
= "/\"({Z.i where i is Element of Z: i >= $1},R);
set D = {F(j) where j is Element of Z: P[j]};
D is Subset of R from DOMAIN_1:sch 8;
then reconsider D as Subset of R;
reconsider D as non empty directed Subset of R by Th30;
p is_S-limit_of ZZ by A12,A13,A14,Def8;
then p <= lim_inf Z by A14;
then consider d being Element of R such that
A15: d in D and
A16: u <= d by A5;
consider j being Element of Z such that
A17: d = "/\"({Z.k where k is Element of Z: k >= j},R) by A15;
reconsider j9 = j as Element of Z;
consider i being Element of Z such that
A18: i >= j9 and i >= j9 by YELLOW_6:def 3;
consider f being Function of Z, Y such that
A19: the mapping of Z = (the mapping of Y)*f and
for m being Element of Y ex n being Element of Z st
for p being Element of Z st n <= p holds m <= f.p by YELLOW_6:def 9;
Z.i in {Z.k where k is Element of Z: k >= j} by A18;
then
A20: d <= Z.i by A17,YELLOW_2:22;
Y.(f.i) = Z.i by A19,FUNCT_2:15;
then Z.i in A by Th35;
then ex a being Element of R st a = Z.i & not a >= u;
hence contradiction by A16,A20,YELLOW_0:def 2;
end;
thus C is (ITERATED_LIMITS)
proof
let X be net of R, p be Element of R such that
A21: [X,p] in C;
let J be net_set of the carrier of X, R such that
A22: for i being Element of X holds [J.i,X.i] in C;
A23: C c= [:NetUniv R,the carrier of R:] by YELLOW_6:def 18;
then
A24: X in NetUniv R by A21,ZFMISC_1:87;
for i being Element of X holds J.i in NetUniv R
proof
let i be Element of X;
[J.i,X.i] in C by A22;
hence thesis by A23,ZFMISC_1:87;
end;
then
A25: Iterated J in NetUniv R by A24,YELLOW_6:25;
reconsider p9 = p as Element of R;
set q = lim_inf Iterated J;
q is_>=_than waybelow p9
proof
let u be Element of R;
assume u in waybelow p9;
then
A26: u << p9 by WAYBEL_3:7;
set T = TopRelStr(#the carrier of R,the InternalRel of R, sigma R#);
A27: the RelStr of T = the RelStr of R;
A28: the carrier of R = the carrier of ConvergenceSpace C
by YELLOW_6:def 24;
then reconsider T as TopLattice by A27,Lm3,Lm9;
reconsider T as complete TopLattice by A27,Lm22;
reconsider T as continuous complete TopLattice by A27,Lm23;
the topology of T = sigma T by A27,Lm21;
then reconsider T as continuous complete Scott TopLattice by Th37;
:: we now move all to T setting
reconsider XX = X as net of T;
reconsider JJ = J as net_set of the carrier of XX,T by A27,Lm18;
reconsider uu = u, qq = q, pp = p9 as Element of T;
set N = Iterated JJ;
set CC = Convergence T;
CC = Convergence ConvergenceSpace C by A28,Lm8;
then
A29: C c= CC by YELLOW_6:40;
A30: uu << pp by A26,A27,Lm15;
A31: qq = lim_inf N by A27,Lm16,Lm17;
for i being Element of XX holds [JJ.i,XX.i] in CC
proof
let i be Element of XX;
reconsider ii = i as Element of X;
[J.ii,X.ii] in C by A22;
hence thesis by A29;
end;
then [N,pp] in CC by A21,A29,YELLOW_6:def 23;
then
A32: pp in Lim N by YELLOW_6:def 19;
pp in wayabove uu by A30;
then wayabove uu is a_neighborhood of pp by Th36,CONNSP_2:3;
then
A33: N is_eventually_in wayabove uu by A32,YELLOW_6:def 15;
wayabove uu c= uparrow uu by WAYBEL_3:11;
then N is_eventually_in uparrow uu by A33,WAYBEL_0:8;
hence u <= q by A27,A31,Lm1,Th18;
end;
then sup waybelow p9 <= q by YELLOW_0:32;
then p <= q by WAYBEL_3:def 5;
then p is_S-limit_of Iterated J;
hence thesis by A25,Def8;
end;
end;
end;
theorem :: Corrollary to Proposition 1.6 (p.103)
for T be continuous complete Scott TopLattice, x be Element of T,
N be net of T st N in NetUniv T holds x is_S-limit_of N iff x in Lim N
proof
let T be continuous complete Scott TopLattice, x be Element of T,
N be net of T such that
A1: N in NetUniv T;
A2: Convergence ConvergenceSpace Scott-Convergence T
= Scott-Convergence T by YELLOW_6:44;
consider M being strict net of T such that
A3: M = N and
the carrier of M in the_universe_of the carrier of T by A1,YELLOW_6:def 11;
the TopStruct of T = ConvergenceSpace Scott-Convergence T by Th32;
then
A4: Convergence T = Convergence ConvergenceSpace Scott-Convergence T by Lm8;
thus x is_S-limit_of N implies x in Lim N
proof
assume x is_S-limit_of N;
then [N,x] in Convergence T by A1,A2,A3,A4,Def8;
hence thesis by YELLOW_6:def 19;
end;
assume x in Lim N;
then [M,x] in Scott-Convergence T by A1,A2,A3,A4,YELLOW_6:def 19;
hence thesis by A1,A3,Def8;
end;
theorem Th39: :: 1.7. Lemma
for L being complete non empty Poset
st Scott-Convergence L is (ITERATED_LIMITS) holds L is continuous
proof
let L be complete non empty Poset such that
A1: Scott-Convergence L is (ITERATED_LIMITS);
set C = Scott-Convergence L;
now
let I be non empty set such that
A2: I in the_universe_of the carrier of L;
let K be non-empty ManySortedSet of I such that
A3: for j being Element of I holds K.j in the_universe_of the carrier of L;
let F be DoubleIndexedSet of K, L such that
A4: for j being Element of I holds rng(F.j) is directed;
set x = Inf Sups F;
A5: x >= Sup Infs Frege F by WAYBEL_5:16;
[:I,I:] c= [:I,I:];
then reconsider r = [:I,I:] as Relation of I;
dom F = I by PARTFUN1:def 2;
then reconsider f = Sups F as Function of I, the carrier of L;
set X = NetStr(#I,r,f#);
A6: for i,j being Element of X holds i <= j
proof
let i,j be Element of X;
[i,j] in the InternalRel of X by ZFMISC_1:87;
hence thesis by ORDERS_2:def 5;
end;
A7: X is transitive
by A6;
X is directed
proof
let x,y be Element of X;
take x;
thus thesis by A6;
end;
then reconsider X = NetStr(#I,r,f#) as strict net of L by A7;
deffunc F(Element of I) = Net-Str(K.$1,F.$1);
consider J being ManySortedSet of I such that
A8: for i being Element of I holds J.i = F(i) from PBOOLE:sch 5;
for i being set st i in the carrier of X holds J.i is net of L
proof
let i be set;
assume i in the carrier of X;
then reconsider i9 = i as Element of I;
reconsider rFi = rng(F.i9) as Subset of L;
A9: rFi is directed by A4;
J.i9 = Net-Str(K.i9,F.i9) by A8;
hence thesis by A9,Th20;
end;
then reconsider J as net_set of the carrier of X, L by YELLOW_6:24;
A10: for j be set st j in I
ex R being 1-sorted st R = J.j & K.j = the carrier of R
proof
let i be set;
assume i in I;
then reconsider i9 = i as Element of I;
take R = Net-Str(K.i9,F.i9);
thus R = J.i by A8;
thus thesis by Def10;
end;
A11: doms F = K by YELLOW_7:45
.= Carrier J by A10,PRALG_1:def 15;
A12: dom Frege F = product doms F by PARTFUN1:def 2;
then
A13: dom Infs Frege F = product doms F by FUNCT_2:def 1;
A14: for i being Element of X holds J.i in NetUniv L
proof
let i be Element of X;
reconsider i9 = i as Element of I;
A15: J.i = Net-Str(K.i9,F.i9) by A8;
then reconsider Ji = J.i as strict net of L;
K.i9 in the_universe_of the carrier of L by A3;
then the carrier of Ji in the_universe_of the carrier of L by A15,Def10;
hence thesis by YELLOW_6:def 11;
end;
A16: for i being Element of X holds [J.i,X.i] in C
proof
let i be Element of X;
reconsider i9 = i as Element of I;
A17: J.i = Net-Str(K.i9,F.i9) by A8;
then reconsider Ji = J.i as monotone reflexive net of L;
A18: J.i in NetUniv L by A14;
i in I;
then i9 in dom F by PARTFUN1:def 2;
then X.i = Sup(F.i9) by WAYBEL_5:def 1
.= Sup the mapping of Ji by A17,Def10
.= sup Ji by WAYBEL_2:def 1
.= lim_inf Ji by Th22;
then X.i is_S-limit_of J.i;
hence thesis by A17,A18,Def8;
end;
A19: X in NetUniv L by A2,YELLOW_6:def 11;
then
A20: Iterated J in NetUniv L by A14,YELLOW_6:25;
deffunc I(Element of Iterated J) =
{(Iterated J).p where p is Element of Iterated J :p >= $1};
the carrier of Iterated J = [:the carrier of X, product Carrier J:]
by YELLOW_6:26;
then reconsider G = the mapping of Iterated J as
Function of [:the carrier of X, product doms F:], the carrier of L by A11;
deffunc I(Element of X, Element of product doms F) =
{G.(i,$2) where i is Element of X :i >= $1};
deffunc F(Element of product doms F) = "/\"(rng((Frege F).$1),L);
deffunc F(Element of X, Element of product doms F) = "/\"(I($1,$2),L);
set D = the set of all "/\"(I(j),L) where j is Element of Iterated J;
set D9 = {F(i,g) where i is Element of X,
g is Element of product doms F: P[g]};
set E9 = {F(g) where g is Element of product doms F : P[g]};
A21: for i being Element of X, g being Element of product doms F
holds F(g) = F(i,g)
proof
let j be Element of X, g be Element of product doms F;
for y being object holds y in I(j,g) iff
ex x being object st x in dom((Frege F).g) & y = ((Frege F).g).x
proof
let y be object;
g in product Carrier J by A11;
then
A22: g in the carrier of product J by YELLOW_1:def 4;
hereby
assume y in I(j,g);
then consider i being Element of X such that
A23: y =G.(i,g) and i >= j;
reconsider x = i as object;
take x;
reconsider i9 = i as Element of I;
A24: i in I;
then
A25: i9 in dom F by PARTFUN1:def 2;
thus x in dom((Frege F).g) by A24,PARTFUN1:def 2;
thus ((Frege F).g).x = F.i9.(g.i) by A12,A25,WAYBEL_5:9
.= (the mapping of Net-Str(K.i9,F.i9)).(g.i) by Def10
.= (the mapping of J.i).(g.i) by A8
.= y by A22,A23,YELLOW_6:def 13;
end;
given x being object such that
A26: x in dom((Frege F).g) and
A27: y = ((Frege F).g).x;
A28: x in dom F by A12,A26,WAYBEL_5:8;
reconsider i9 = x as Element of I by A26;
reconsider i = i9 as Element of X;
A29: i >= j by A6;
y = (F.x).(g.x) by A12,A27,A28,WAYBEL_5:9
.= (the mapping of Net-Str(K.i9,F.i9)).(g.i) by Def10
.= (the mapping of J.i).(g.i) by A8
.= G.(i,g) by A22,YELLOW_6:def 13;
hence thesis by A29;
end;
hence thesis by FUNCT_1:def 3;
end;
A30: D = D9
proof
A31: the carrier of Iterated J = [:the carrier of X, product Carrier J:]
by YELLOW_6:26;
A32: for p being Element of Iterated J, i being Element of X,
g being Element of product doms F st p = [i,g]
holds "/\"(I(p),L) = "/\"(I(i,g),L)
proof
let p be Element of Iterated J, i be Element of X,
g be Element of product doms F such that
A33: p = [i,g];
A34: the RelStr of Iterated J= the RelStr of [:X, product J:]
by YELLOW_6:def 13;
reconsider g9 = g as Element of product J by A11,YELLOW_1:def 4;
g9 in the carrier of product J;
then
A35: g9 in product Carrier J by YELLOW_1:def 4;
reconsider i9 = i as Element of X;
for i be object st i in the carrier of X
ex R being RelStr, xi,yi being Element of R
st R = J.i & xi = g9.i & yi = g9.i & xi <= yi
proof
let i be object;
assume i in the carrier of X;
then reconsider ii = i as Element of X;
reconsider i9 = ii as Element of I;
A36: J.i = Net-Str(K.i9,F.i9) by A8;
set R = Net-Str(K.i9,F.i9);
g9.ii in the carrier of R by A36;
then reconsider x = g9.i as Element of R;
take R,x,x;
x <= x;
hence thesis by A8;
end;
then
A37: g9 <= g9 by A35,YELLOW_1:def 4;
I(i,g) c= I(p)
proof
let u be object;
assume u in I(i,g);
then consider j being Element of X such that
A38: u = (the mapping of Iterated J).(j,g) and
A39: j >= i;
reconsider j9 = j as Element of X;
reconsider q = [j,g] as Element of Iterated J by A11,YELLOW_6:26;
[j9,g9] >= [i9,g9] by A37,A39,YELLOW_3:11;
then
A40: q >= p by A33,A34,Lm1;
u = (Iterated J).q by A38;
hence thesis by A40;
end;
then
A41: "/\"(I(p),L) <= "/\"(I(i,g),L) by WAYBEL_7:1;
defpred P[Element of X] means $1 >= i;
deffunc F(Element of X) = G.($1,g);
{F(k) where k is Element of X: P[k]}
is Subset of L from DOMAIN_1:sch 8;
then reconsider A = I(i,g) as Subset of L;
defpred P[Element of Iterated J] means $1 >= p;
deffunc F(Element of Iterated J) = (Iterated J).$1;
{F(z) where z is Element of Iterated J: P[z]}
is Subset of L from DOMAIN_1:sch 8;
then reconsider B = I(p) as Subset of L;
B is_coarser_than A
proof
let b be Element of L;
assume b in B;
then consider q being Element of Iterated J such that
A42: b = (Iterated J).q and
A43: p <= q;
consider k being Element of X,
f being Element of product Carrier J such that
A44: q = [k,f] by A31,DOMAIN_1:1;
reconsider k9 = k as Element of X;
set a = (the mapping of Iterated J).(k,g);
a = G.(k,g);
then reconsider a as Element of L;
take a;
reconsider f9 = f as Element of product J by YELLOW_1:def 4;
A45: [k9,f9] >= [i9,g9] by A33,A34,A43,A44,Lm1;
then i <= k by YELLOW_3:11;
hence a in A;
reconsider k9 = k as Element of I;
set N = Net-Str(K.k9,F.k9);
A46: J.k = N by A8;
reconsider g9k =g9.k, f9k = f9.k as Element of N by A8;
A47: b = N.(f9k) by A42,A44,A46,YELLOW_6:27;
reconsider kg = [k,g] as Element of Iterated J by A11,YELLOW_6:26;
A48: a = (Iterated J).kg .= N.(g9k) by A46,YELLOW_6:27;
g9 <= f9 by A45,YELLOW_3:11;
then g9.k <= f9.k by WAYBEL_3:28;
hence a <= b by A46,A47,A48,Def10;
end;
then "/\"(I(i,g),L) <= "/\"(I(p),L) by Th1;
hence thesis by A41,YELLOW_0:def 3;
end;
thus D c= D9
proof
let e be object;
assume e in D;
then consider p being Element of Iterated J such that
A49: e = "/\"(I(p),L);
consider j being Element of X,
g being Element of product doms F such that
A50: p = [j,g] by A11,A31,DOMAIN_1:1;
e = "/\"(I(j,g),L) by A32,A49,A50;
hence thesis;
end;
let e be object;
assume e in D9;
then consider i being Element of X,
g being Element of product doms F such that
A51: e = "/\"(I(i,g),L);
reconsider j = [i,g] as Element of Iterated J by A11,YELLOW_6:26;
e = "/\"(I(j),L) by A32,A51;
hence thesis;
end;
A52: E9 = D9 from Irrel(A21); :: UWAGA!!! wrazliwy na strony rownosci
for y being object holds y in E9 iff
ex x being object st x in dom(Infs Frege F) & y = (Infs Frege F).x
proof
let y be object;
thus y in E9 implies
ex x being object st x in dom(Infs Frege F) & y = (Infs Frege F).x
proof
assume y in E9;
then consider g being Element of product doms F such that
A53: y = "/\"(rng((Frege F).g),L);
take g;
thus
A54: g in dom(Infs Frege F) by A13;
thus y = //\((Frege F).g, L) by A53,YELLOW_2:def 6
.= (Infs Frege F).g by A54,WAYBEL_5:def 2;
end;
given x being object such that
A55: x in dom(Infs Frege F) and
A56: y = (Infs Frege F).x;
reconsider x as Element of product doms F by A55,PARTFUN1:def 2;
y = //\((Frege F).x, L) by A55,A56,WAYBEL_5:def 2
.= "/\"(rng((Frege F).x),L) by YELLOW_2:def 6;
hence thesis;
end;
then rng Infs Frege F = E9 by FUNCT_1:def 3;
then
A57: Sup Infs Frege F = lim_inf Iterated J by A30,A52,YELLOW_2:def 5;
reconsider x9 = x as Element of L;
set X1 = the set of all x where j9 is Element of X;
set X2 = the set of all "/\"({X.i where i is Element of X:i >= j},L)
where j is Element of X;
A58: X2 = X1
proof
A59: for j being Element of X holds
x = "/\"({X.i where i is Element of X:i >= j},L)
proof
let j be Element of X;
set X3 = {X.i where i is Element of X:i >= j};
for e being object holds e in X3 iff
ex u being object st u in dom Sups F & e = (Sups F).u
proof
let e be object;
hereby
assume e in X3;
then consider i being Element of X such that
A60: e = X.i and i >= j;
reconsider u = i as object;
take u;
u in I;
hence u in dom Sups F by FUNCT_2:def 1;
thus e = (Sups F).u by A60;
end;
given u being object such that
A61: u in dom Sups F and
A62: e = (Sups F).u;
reconsider i = u as Element of X by A61,FUNCT_2:def 1;
A63: i >= j by A6;
e = X.i by A62;
hence thesis by A63;
end;
then rng Sups F = X3 by FUNCT_1:def 3;
hence thesis by YELLOW_2:def 6;
end;
thus X2 c= X1
proof
let u be object;
assume u in X2;
then ex j being Element of X st ( u = "/\"({X.i where i is
Element of X:i >= j},L));
then u = x by A59;
hence thesis;
end;
let u be object;
set j = the Element of X;
assume u in X1;
then ex j being Element of X st u = x;
then u = "/\"({X.i where i is Element of X:i >= j},L) by A59;
hence thesis;
end;
now
let u be object;
u in X1 iff ex j9 being Element of X st u = x;
then u in X1 iff u = x;
hence u in X1 iff u in {x} by TARSKI:def 1;
end;
then "\/"(X2,L) = sup {x9} by A58,TARSKI:2
.= x by YELLOW_0:39;
then x <= lim_inf X;
then x is_S-limit_of X;
then [X,x] in C by A19,Def8;
then [Iterated J,x] in C by A1,A16;
then x is_S-limit_of Iterated J by A20,Def8;
then x <= Sup Infs Frege F by A57;
hence x = Sup Infs Frege F by A5,ORDERS_2:2;
end;
hence thesis by WAYBEL_5:18;
end;
theorem :: 1.8 Theorem, p.104
for T being complete Scott TopLattice holds
T is continuous iff Convergence T = Scott-Convergence T
proof
let T be complete Scott TopLattice;
hereby
assume T is continuous;
then reconsider L = T as continuous complete Scott TopLattice;
the TopStruct of T = ConvergenceSpace Scott-Convergence T by Th32;
hence
Convergence T = Convergence ConvergenceSpace Scott-Convergence L by Lm8
.= Scott-Convergence T by YELLOW_6:44;
end;
thus thesis by Th39;
end;
theorem Th41: :: 1.9 Remark, p.104
for T being complete Scott TopLattice,
S being upper Subset of T st S is Open holds S is open
proof
let T be complete Scott TopLattice, S be upper Subset of T such that
A1: for x be Element of T st x in S ex y be Element of T st y in S & y << x;
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
A2: y in S and
A3: y << sup D by A1;
consider d being Element of T such that
A4: d in D and
A5: y <= d by A3;
d in S by A2,A5,WAYBEL_0:def 20;
hence thesis by A4,XBOOLE_0:3;
end;
hence thesis by Def4;
end;
theorem Th42:
for L being non empty RelStr, S being upper Subset of L,
x being Element of L st x in S holds uparrow x c= S
proof
let L be non empty RelStr, S be upper Subset of L, x be Element of L;
assume
A1: x in S;
let e be object;
assume
A2: e in uparrow x;
then reconsider y = e as Element of L;
x <= y by A2,WAYBEL_0:18;
hence thesis by A1,WAYBEL_0:def 20;
end;
theorem Th43:
for L being complete continuous Scott TopLattice,
p be Element of L, S be Subset of L st S is open & p in S
ex q being Element of L st q << p & q in S
proof
let L be complete continuous Scott TopLattice, p be Element of L;
let S be Subset of L such that
A1: S is open and
A2: p in S;
A3: S is inaccessible by A1,Def4;
sup waybelow p = p by WAYBEL_3:def 5;
then waybelow p meets S by A2,A3;
then (waybelow p) /\ S <> {};
then consider u being Element of L such that
A4: u in (waybelow p) /\ S by SUBSET_1:4;
reconsider u as Element of L;
take u;
u in waybelow p by A4,XBOOLE_0:def 4;
hence u << p by WAYBEL_3:7;
thus thesis by A4,XBOOLE_0:def 4;
end;
theorem Th44: :: 1.10. Propostion (i), p.104
for L being complete continuous Scott TopLattice, p be Element of L
holds { wayabove q where q is Element of L: q << p } is Basis of p
proof
let L be complete continuous Scott TopLattice, p be Element of L;
set X = { wayabove q where q is Element of L: q << p };
X c= bool the carrier of L
proof
let e be object;
assume e in X;
then ex q being Element of L st e = wayabove q & q << p;
hence thesis;
end;
then reconsider X as Subset-Family of L;
X is Basis of p
proof
A1: X is open
proof
let e be Subset of L;
assume e in X;
then consider q being Element of L such that
A2: e = wayabove q and q << p;
wayabove q is open by Th36;
hence thesis by A2;
end;
X is p-quasi_basis
proof
for Y being set st Y in X holds p in Y
proof
let e be set;
assume e in X;
then ex q being Element of L st e = wayabove q & q << p;
hence thesis;
end;
hence p in Intersect X by SETFAM_1:43;
let S be Subset of L such that
A3: S is open and
A4: p in S;
consider u being Element of L such that
A5: u << p and
A6: u in S by A3,A4,Th43;
take V = wayabove u;
thus V in X by A5;
A7: S is upper by A3,Def4;
A8: wayabove u c= uparrow u by WAYBEL_3:11;
uparrow u c= S by A6,A7,Th42;
hence thesis by A8;
end;
hence thesis by A1;
end;
hence thesis;
end;
theorem Th45:
for T being complete continuous Scott TopLattice holds
the set of all wayabove x where x is Element of T is Basis of T
proof
let T be complete continuous Scott TopLattice;
set B = the set of all wayabove x where x is Element of T;
A1: B c= the topology of T
proof
let e be object;
assume e in B;
then consider x being Element of T such that
A2: e = wayabove x;
wayabove x is open by Th36;
hence thesis by A2;
end;
then reconsider P = B as Subset-Family of T by XBOOLE_1:1;
for x being Point of T ex B being Basis of x st B c= P
proof
let x be Point of T;
reconsider p = x as Element of T;
reconsider A =
{ wayabove q where q is Element of T: q << p } as Basis of x by Th44;
take A;
let u be object;
assume u in A;
then ex q being Element of T st u = wayabove q & q << p;
hence thesis;
end;
hence thesis by A1,YELLOW_8:14;
end;
theorem :: 1.10. Propostion (ii), p.104
for T being complete continuous Scott TopLattice, S being upper Subset of T
holds S is open iff S is Open
proof
let T be complete continuous Scott TopLattice, S be upper Subset of T;
thus S is open implies S is Open
proof
assume
A1: S is open;
let x be Element of T;
assume x in S;
then ex y be Element of T st y << x & y in S by A1,Th43;
hence thesis;
end;
thus thesis by Th41;
end;
theorem :: 1.10. Propostion (iii), p.104
for T being complete continuous Scott TopLattice, p being Element of T
holds Int uparrow p = wayabove p
proof
let T be complete continuous Scott TopLattice, p be Element of T;
thus Int uparrow p c= wayabove p
proof
let y be object;
assume
A1: y in Int uparrow p;
then reconsider q = y as Element of T;
reconsider S = Int uparrow p as Subset of T;
consider u being Element of T such that
A2: u << q and
A3: u in S by A1,Th43;
S c= uparrow p by TOPS_1:16;
then p <= u by A3,WAYBEL_0:18;
then p << q by A2,WAYBEL_3:2;
hence thesis;
end;
wayabove p c= uparrow p by WAYBEL_3:11;
hence thesis by Th36,TOPS_1:24;
end;
theorem :: 1.10. Propostion (iv), p.104
for T being complete continuous Scott TopLattice, S being Subset of T
holds Int S = union{wayabove x where x is Element of T: wayabove x c= S}
proof
let T be complete continuous Scott TopLattice, S be Subset of T;
set B = the set of all wayabove x where x is Element of T;
set I = { G where G is Subset of T: G in B & G c= S },
P = {wayabove x where x is Element of T: wayabove x c= S};
A1: I = P
proof
thus I c= P
proof
let e be object;
assume e in I;
then consider G being Subset of T such that
A2: e = G and
A3: G in B and
A4: G c= S;
ex x being Element of T st G = wayabove x by A3;
hence thesis by A2,A4;
end;
let e be object;
assume e in P;
then consider x being Element of T such that
A5: e = wayabove x and
A6: wayabove x c= S;
wayabove x in B;
hence thesis by A5,A6;
end;
B is Basis of T by Th45;
hence thesis by A1,YELLOW_8:11;
end;