let L be complete LATTICE; for S being Subset of L holds
( S in the topology of (ConvergenceSpace (Scott-Convergence L)) iff ( S is inaccessible & S is upper ) )
set SC = Scott-Convergence L;
set T = ConvergenceSpace (Scott-Convergence L);
A1:
the topology of (ConvergenceSpace (Scott-Convergence L)) = { V where V is Subset of L : for p being Element of L st p in V holds
for N being net of L st [N,p] in Scott-Convergence L holds
N is_eventually_in V }
by YELLOW_6:def 24;
let S be Subset of L; ( S in the topology of (ConvergenceSpace (Scott-Convergence L)) iff ( S is inaccessible & S is upper ) )
hereby ( S is inaccessible & S is upper implies S in the topology of (ConvergenceSpace (Scott-Convergence L)) )
assume
S in the
topology of
(ConvergenceSpace (Scott-Convergence L))
;
( S is inaccessible & S is upper )then A2:
ex
V being
Subset of
L st
(
S = V & ( for
p being
Element of
L st
p in V holds
for
N being
net of
L st
[N,p] in Scott-Convergence L holds
N is_eventually_in V ) )
by A1;
thus
S is
inaccessible
S is upper proof
let D be non
empty directed Subset of
L;
WAYBEL11:def 1 ( sup D in S implies D meets S )
assume A3:
sup D in S
;
D meets 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
reflexive strict monotone net of
L by A5, Th20;
A6:
N in NetUniv L
by Th21;
lim_inf N =
sup N
by Th22
.=
Sup
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 Scott-Convergence L
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
D meets 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 L))
for p being Element of L st p in S holds
for N being net of L st [N,p] in Scott-Convergence L holds
N is_eventually_in S
proof
let p be
Element of
L;
( p in S implies for N being net of L st [N,p] in Scott-Convergence L holds
N is_eventually_in S )
assume A16:
p in S
;
for N being net of L st [N,p] in Scott-Convergence L holds
N is_eventually_in S
reconsider p9 =
p as
Element of
L ;
let N be
net of
L;
( [N,p] in Scott-Convergence L implies N is_eventually_in S )
assume A17:
[N,p] in Scott-Convergence L
;
N is_eventually_in S
Scott-Convergence L 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 H1(
Element of
N)
-> Element of the
carrier of
L =
"/\" (
{ (N . i) where i is Element of N : i >= $1 } ,
L);
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
L
from DOMAIN_1:sch 8();
then reconsider D =
{ H1(j) where j is Element of N : S1[j] } as
Subset of
L ;
reconsider D =
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 =
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 =
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 { (N . i) where i is Element of N : i >= j }
;
then
d <= N . i0
by A21, YELLOW_2:22;
hence
N . i0 in S
by A15, A22;
verum
end;
hence
S in the topology of (ConvergenceSpace (Scott-Convergence L))
by A1; verum