let T be complete TopLattice; ( TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T) implies for S being Subset of T holds
( S is open iff ( S is inaccessible & S is upper ) ) )
set SC = Scott-Convergence T;
assume
TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T)
; for S being Subset of T holds
( S is open iff ( S is inaccessible & S is upper ) )
then A1:
the topology of T = { V where V is Subset of T : for p being Element of T st p in V holds
for N being net of T st [N,p] in Scott-Convergence T holds
N is_eventually_in V }
by YELLOW_6:def 24;
let S be Subset of T; ( S is open iff ( S is inaccessible & S is upper ) )
hereby ( S is inaccessible & S is upper implies S is open )
assume
S is
open
;
( S is inaccessible & S is upper )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 holds
for
N being
net of
T st
[N,p] in Scott-Convergence T holds
N is_eventually_in V ) )
by A1;
thus
S is
inaccessible
S is upper proof
let D be non
empty directed Subset of
T;
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
T by A4, RELSET_1:4;
reconsider N =
Net-Str (
D,
f) as
reflexive strict monotone net of
T by A5, Th20;
A6:
N in NetUniv T
by Th21;
lim_inf N =
sup N
by Th22
.=
Sup
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 Scott-Convergence T
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 is open
for p being Element of T st p in S holds
for N being net of T st [N,p] in Scott-Convergence T holds
N is_eventually_in S
proof
let p be
Element of
T;
( p in S implies for N being net of T st [N,p] in Scott-Convergence T holds
N is_eventually_in S )
assume A16:
p in S
;
for N being net of T st [N,p] in Scott-Convergence T holds
N is_eventually_in S
reconsider p9 =
p as
Element of
T ;
let N be
net of
T;
( [N,p] in Scott-Convergence T implies N is_eventually_in S )
assume A17:
[N,p] in Scott-Convergence T
;
N is_eventually_in S
Scott-Convergence T 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 H1(
Element of
N)
-> Element of the
carrier of
T =
"/\" (
{ (N . i) where i is Element of N : i >= $1 } ,
T);
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
T
from DOMAIN_1:sch 8();
then reconsider D =
{ H1(j) where j is Element of N : S1[j] } as
Subset of
T ;
reconsider D =
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 =
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 =
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;
then
S in the topology of T
by A1;
hence
S is open
; verum