set C = Scott-Convergence R;
thus
( Scott-Convergence R is (CONSTANTS) & Scott-Convergence R is (SUBNETS) )
; YELLOW_6:def 25 ( Scott-Convergence R is (DIVERGENCE) & Scott-Convergence R is (ITERATED_LIMITS) )
thus
Scott-Convergence R is (DIVERGENCE)
Scott-Convergence R is (ITERATED_LIMITS) proof
let X be
net of
R;
YELLOW_6:def 22 for b1 being Element of the carrier of R holds
( not X in NetUniv R or [X,b1] in Scott-Convergence R or ex b2 being subnet of X st
( b2 in NetUniv R & ( for b3 being subnet of b2 holds not [b3,b1] in Scott-Convergence R ) ) )let p be
Element of
R;
( not X in NetUniv R or [X,p] in Scott-Convergence R or ex b1 being subnet of X st
( b1 in NetUniv R & ( for b2 being subnet of b1 holds not [b2,p] in Scott-Convergence R ) ) )
assume that A1:
X in NetUniv R
and A2:
not
[X,p] in Scott-Convergence R
;
ex b1 being subnet of X st
( b1 in NetUniv R & ( for b2 being subnet of b1 holds not [b2,p] in Scott-Convergence R ) )
A3:
for
x being
Element of
R holds
( not
waybelow x is
empty &
waybelow x is
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 where a is Element of R : not a >= u }
then reconsider Y =
X " { a where a is Element of R : not a >= u } as
subnet of
X by YELLOW_6:22;
take
Y
;
( Y in NetUniv R & ( for b1 being subnet of Y holds not [b1,p] in Scott-Convergence R ) )
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 where a is Element of R : not a >= u } is
SubRelStr of
X
by YELLOW_6:def 6;
then
the
carrier of
(X " { a where a is Element of R : not a >= u } ) 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;
for b1 being subnet of Y holds not [b1,p] in Scott-Convergence R
let Z be
subnet of
Y;
not [Z,p] in Scott-Convergence R
assume A12:
[Z,p] in Scott-Convergence R
;
contradiction
Scott-Convergence R 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 H1(
Element of
Z)
-> Element of the
carrier of
R =
"/\" (
{ (Z . i) where i is Element of Z : i >= R } ,
R);
set D =
{ H1(j) where j is Element of Z : S1[j] } ;
{ H1(j) where j is Element of Z : S1[j] } is
Subset of
R
from DOMAIN_1:sch 8();
then reconsider D =
{ H1(j) where j is Element of Z : S1[j] } as
Subset of
R ;
reconsider D =
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 where a is Element of R : not a >= u }
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;
verum
end;
thus
Scott-Convergence R is (ITERATED_LIMITS)
verumproof
let X be
net of
R;
YELLOW_6:def 23 for b1 being Element of the carrier of R holds
( not [X,b1] in Scott-Convergence R or for b2 being net_set of the carrier of X,R holds
( ex b3 being Element of the carrier of X st not [(b2 . b3),(X . b3)] in Scott-Convergence R or [(Iterated b2),b1] in Scott-Convergence R ) )let p be
Element of
R;
( not [X,p] in Scott-Convergence R or for b1 being net_set of the carrier of X,R holds
( ex b2 being Element of the carrier of X st not [(b1 . b2),(X . b2)] in Scott-Convergence R or [(Iterated b1),p] in Scott-Convergence R ) )
assume A21:
[X,p] in Scott-Convergence R
;
for b1 being net_set of the carrier of X,R holds
( ex b2 being Element of the carrier of X st not [(b1 . b2),(X . b2)] in Scott-Convergence R or [(Iterated b1),p] in Scott-Convergence R )
let J be
net_set of the
carrier of
X,
R;
( ex b1 being Element of the carrier of X st not [(J . b1),(X . b1)] in Scott-Convergence R or [(Iterated J),p] in Scott-Convergence R )
assume A22:
for
i being
Element of
X holds
[(J . i),(X . i)] in Scott-Convergence R
;
[(Iterated J),p] in Scott-Convergence R
A23:
Scott-Convergence R 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
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);
lim_inf (Iterated J) is_>=_than waybelow p9
proof
let u be
Element of
R;
LATTICE3:def 9 ( not u in waybelow p9 or u <= lim_inf (Iterated J) )
assume
u in waybelow p9
;
u <= lim_inf (Iterated J)
then A26:
u << p9
by WAYBEL_3:7;
set T =
TopRelStr(# the
carrier of
R, the
InternalRel of
R,
(sigma R) #);
A27:
RelStr(# the
carrier of
TopRelStr(# the
carrier of
R, the
InternalRel of
R,
(sigma R) #), the
InternalRel of
TopRelStr(# the
carrier of
R, the
InternalRel of
R,
(sigma R) #) #)
= RelStr(# the
carrier of
R, the
InternalRel of
R #)
;
A28:
the
carrier of
R = the
carrier of
(ConvergenceSpace (Scott-Convergence R))
by YELLOW_6:def 24;
then reconsider T =
TopRelStr(# the
carrier of
R, the
InternalRel of
R,
(sigma R) #) as
TopLattice by A27, Lm3, Lm9;
reconsider T =
T as
complete TopLattice by A27, Lm22;
reconsider T =
T as
complete continuous TopLattice by A27, Lm23;
the
topology of
T = sigma T
by A27, Lm21;
then reconsider T =
T as
complete continuous Scott TopLattice by Th37;
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 =
lim_inf (Iterated J),
pp =
p9 as
Element of
T ;
set N =
Iterated JJ;
set CC =
Convergence T;
Convergence T = Convergence (ConvergenceSpace (Scott-Convergence R))
by A28, Lm8;
then A29:
Scott-Convergence R c= Convergence T
by YELLOW_6:40;
A30:
uu << pp
by A26, A27, Lm15;
A31:
qq = lim_inf (Iterated JJ)
by A27, Lm16, Lm17;
for
i being
Element of
XX holds
[(JJ . i),(XX . i)] in Convergence T
then
[(Iterated JJ),pp] in Convergence T
by A21, A29, YELLOW_6:def 23;
then A32:
pp in Lim (Iterated JJ)
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:
Iterated JJ is_eventually_in wayabove uu
by A32, YELLOW_6:def 15;
wayabove uu c= uparrow uu
by WAYBEL_3:11;
then
Iterated JJ is_eventually_in uparrow uu
by A33, WAYBEL_0:8;
hence
u <= lim_inf (Iterated J)
by A27, A31, Lm1, Th18;
verum
end;
then
sup (waybelow p9) <= lim_inf (Iterated J)
by YELLOW_0:32;
then
p <= lim_inf (Iterated J)
by WAYBEL_3:def 5;
then
p is_S-limit_of Iterated J
;
hence
[(Iterated J),p] in Scott-Convergence R
by A25, Def8;
verum
end;