let R be /\-complete Semilattice; for S being Subset of R holds
( S in the topology of (ConvergenceSpace (Scott-Convergence R)) iff ( S is inaccessible & S is upper ) )
set SC = Scott-Convergence R;
set T = ConvergenceSpace (Scott-Convergence R);
A1:
the topology of (ConvergenceSpace (Scott-Convergence R)) = { V where V is Subset of R : for p being Element of R st p in V holds
for N being net of R st [N,p] in Scott-Convergence R holds
N is_eventually_in V }
by YELLOW_6:def 24;
let S be Subset of R; ( S in the topology of (ConvergenceSpace (Scott-Convergence R)) iff ( S is inaccessible & S is upper ) )
hereby ( S is inaccessible & S is upper implies S in the topology of (ConvergenceSpace (Scott-Convergence R)) )
assume
S in the
topology of
(ConvergenceSpace (Scott-Convergence R))
;
( S is inaccessible & S is upper )then A2:
ex
V being
Subset of
R st
(
S = V & ( for
p being
Element of
R st
p in V holds
for
N being
net of
R st
[N,p] in Scott-Convergence R holds
N is_eventually_in V ) )
by A1;
thus
S is
inaccessible
S is upper proof
let D be non
empty directed Subset of
R;
WAYBEL11:def 1 ( not "\/" (D,R) in S or not D misses S )
assume A3:
sup D in S
;
not D misses S
A4:
dom (id D) = D
by RELAT_1:45;
A5:
rng (id D) = D
by RELAT_1:45;
then reconsider f =
id D as
Function of
D, the
carrier of
R by A4, FUNCT_2:def 1, RELSET_1:4;
reconsider N =
Net-Str (
D,
f) as
reflexive strict monotone net of
R by A5, WAYBEL11:20;
A6:
N in NetUniv R
by WAYBEL11:21;
lim_inf N =
sup N
by Th9
.=
Sup
by WAYBEL_2:def 1
.=
"\/" (
(rng the mapping of N),
R)
by YELLOW_2:def 5
.=
"\/" (
(rng f),
R)
by WAYBEL11:def 10
.=
sup D
by RELAT_1:45
;
then
sup D is_S-limit_of N
;
then
[N,(sup D)] in Scott-Convergence R
by A6, WAYBEL11:def 8;
then
N is_eventually_in S
by A2, A3;
then consider i0 being
Element of
N such that A7:
for
j being
Element of
N st
i0 <= j holds
N . j in S
;
consider j0 being
Element of
N such that A8:
j0 >= i0
and
j0 >= i0
by YELLOW_6:def 3;
A9:
N . j0 in S
by A7, A8;
A10:
D = the
carrier of
N
by WAYBEL11:def 10;
N . j0 =
(id D) . j0
by WAYBEL11:def 10
.=
j0
by A10
;
hence
not
D misses S
by A9, A10, XBOOLE_0:3;
verum
end; thus
S is
upper
verum
end;
assume that
A14:
S is inaccessible
and
A15:
S is upper
; S in the topology of (ConvergenceSpace (Scott-Convergence R))
for p being Element of R st p in S holds
for N being net of R st [N,p] in Scott-Convergence R holds
N is_eventually_in S
proof
let p be
Element of
R;
( p in S implies for N being net of R st [N,p] in Scott-Convergence R holds
N is_eventually_in S )
assume A16:
p in S
;
for N being net of R st [N,p] in Scott-Convergence R holds
N is_eventually_in S
reconsider p9 =
p as
Element of
R ;
let N be
net of
R;
( [N,p] in Scott-Convergence R implies N is_eventually_in S )
assume A17:
[N,p] in Scott-Convergence R
;
N is_eventually_in S
Scott-Convergence R c= [:(NetUniv R), the carrier of R:]
by YELLOW_6:def 18;
then A18:
N in NetUniv R
by A17, ZFMISC_1:87;
then
ex
N9 being
strict net of
R st
(
N9 = N & the
carrier of
N9 in the_universe_of the
carrier of
R )
by YELLOW_6:def 11;
then
p is_S-limit_of N
by A17, A18, WAYBEL11:def 8;
then A19:
p9 <= lim_inf N
;
deffunc H1(
Element of
N)
-> Element of the
carrier of
R =
"/\" (
{ (N . i) where i is Element of N : i >= $1 } ,
R);
defpred S1[
set ]
means verum;
set X =
{ H1(j) where j is Element of N : S1[j] } ;
{ H1(j) where j is Element of N : S1[j] } is
Subset of
R
from DOMAIN_1:sch 8();
then reconsider D =
{ H1(j) where j is Element of N : S1[j] } as
Subset of
R ;
reconsider D =
D as non
empty directed Subset of
R by Th7;
sup D in S
by A15, A16, A19;
then
D meets S
by A14;
then
D /\ S <> {}
;
then consider d being
Element of
R such that A20:
d in D /\ S
by SUBSET_1:4;
reconsider d =
d as
Element of
R ;
d in D
by A20, XBOOLE_0:def 4;
then consider j being
Element of
N such that A21:
d = "/\" (
{ (N . i) where i is Element of N : i >= j } ,
R)
;
defpred S2[
Element of
N]
means $1
>= j;
deffunc H2(
Element of
N)
-> Element of the
carrier of
R =
N . $1;
{ H2(i) where i is Element of N : S2[i] } is
Subset of
R
from DOMAIN_1:sch 8();
then reconsider Y =
{ (N . i) where i is Element of N : i >= j } as
Subset of
R ;
reconsider j =
j as
Element of
N ;
take
j
;
WAYBEL_0:def 11 for b1 being Element of the carrier of N holds
( not j <= b1 or N . b1 in S )
let i0 be
Element of
N;
( not j <= i0 or N . i0 in S )
A22:
d in S
by A20, XBOOLE_0:def 4;
assume
j <= i0
;
N . i0 in S
then
N . i0 in Y
;
then
d <= N . i0
by A21, Th8;
hence
N . i0 in S
by A15, A22;
verum
end;
hence
S in the topology of (ConvergenceSpace (Scott-Convergence R))
by A1; verum