let T be complete TopLattice; :: thesis: ( 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_by_directed_joins & S is upper ) ) )
set SC = Scott-Convergence T;
assume
TopStruct(# the carrier of T,the topology of T #) = ConvergenceSpace (Scott-Convergence T)
; :: thesis: for S being Subset of T holds
( S is open iff ( S is inaccessible_by_directed_joins & 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 27;
let S be Subset of T; :: thesis: ( S is open iff ( S is inaccessible_by_directed_joins & S is upper ) )
hereby :: thesis: ( S is inaccessible_by_directed_joins & S is upper implies S is open )
assume
S is
open
;
:: thesis: ( S is inaccessible_by_directed_joins & S is upper )then
S in the
topology of
T
by PRE_TOPC:def 5;
then consider V being
Subset of
T such that A2:
S = V
and A3:
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_by_directed_joins
:: thesis: S is upper proof
let D be non
empty directed Subset of
T;
:: according to WAYBEL11:def 1 :: thesis: ( sup D in S implies D meets S )
assume A4:
sup D in S
;
:: thesis: D meets S
A5:
(
dom (id D) = D &
rng (id D) = D )
by RELAT_1:71;
then reconsider f =
id D as
Function of
D,the
carrier of
T by RELSET_1:11;
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:71
;
then
sup D is_S-limit_of N
by Def7;
then
[N,(sup D)] in Scott-Convergence T
by A6, Def8;
then
N is_eventually_in S
by A2, A3, A4;
then consider i0 being
Element of
N such that A7:
for
j being
Element of
N st
i0 <= j holds
N . j in S
by WAYBEL_0:def 11;
consider j0 being
Element of
N such that A8:
j0 >= i0
and
j0 >= i0
by YELLOW_6:def 5;
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, FUNCT_1:35
;
hence
D meets S
by A9, A10, XBOOLE_0:3;
:: thesis: verum
end; thus
S is
upper
:: thesis: verum
end;
assume that
A14:
S is inaccessible_by_directed_joins
and
A15:
S is upper
; :: thesis: 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;
:: thesis: ( 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
;
:: thesis: for N being net of T st [N,p] in Scott-Convergence T holds
N is_eventually_in S
reconsider p' =
p as
Element of
T ;
let N be
net of
T;
:: thesis: ( [N,p] in Scott-Convergence T implies N is_eventually_in S )
assume A17:
[N,p] in Scott-Convergence T
;
:: thesis: N is_eventually_in S
Scott-Convergence T c= [:(NetUniv T),the carrier of T:]
by YELLOW_6:def 21;
then A18:
N in NetUniv T
by A17, ZFMISC_1:106;
then
ex
N' being
strict net of
T st
(
N' = N & the
carrier of
N' in the_universe_of the
carrier of
T )
by YELLOW_6:def 14;
then
p is_S-limit_of N
by A17, A18, Def8;
then A19:
p' <= lim_inf N
by Def7;
defpred S1[
set ]
means verum;
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, WAYBEL_0:def 20;
then
D meets S
by A14, Def1;
then
D /\ S <> {}
by XBOOLE_0:def 7;
then consider d being
Element of
T such that A20:
d in D /\ S
by SUBSET_1:10;
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
;
:: according to WAYBEL_0:def 11 :: thesis: for b1 being Element of the carrier of N holds
( not j <= b1 or N . b1 in S )
let i0 be
Element of
N;
:: thesis: ( not j <= i0 or N . i0 in S )
A22:
d in S
by A20, XBOOLE_0:def 4;
assume
j <= i0
;
:: thesis: 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:24;
hence
N . i0 in S
by A15, A22, WAYBEL_0:def 20;
:: thesis: verum
end;
then
S in the topology of T
by A1;
hence
S is open
by PRE_TOPC:def 5; :: thesis: verum