:: Scott Topology
:: by Andrzej Trybulec
::
:: Received January 29, 1997
:: Copyright (c) 1997-2011 Association of Mizar Users


begin

Lm1: for R, S being RelStr
for p, q being Element of R
for p9, q9 being Element of S st p = p9 & q = q9 & RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of S, the InternalRel of S #) & p <= q holds
p9 <= q9
proof end;

scheme :: WAYBEL11:sch 1
Irrel{ F1() -> non empty set , F2() -> non empty set , P1[ set ], F3( set ) -> set , F4( set , set ) -> set } :
{ F3(u) where u is Element of F1() : P1[u] } = { F4(i,v) where i is Element of F2(), v is Element of F1() : P1[v] }
provided
A1: for i being Element of F2()
for u being Element of F1() holds F3(u) = F4(i,u)
proof end;

theorem Th1: :: WAYBEL11:1
for L being complete LATTICE
for X, Y being Subset of L st Y is_coarser_than X holds
"/\" (X,L) <= "/\" (Y,L)
proof end;

theorem Th2: :: WAYBEL11:2
for L being complete LATTICE
for X, Y being Subset of L st X is_finer_than Y holds
"\/" (X,L) <= "\/" (Y,L)
proof end;

theorem :: WAYBEL11:3
for T being RelStr
for A being upper Subset of T
for B being directed Subset of T holds A /\ B is directed
proof end;

registration
let T be non empty reflexive RelStr ;
cluster non empty finite directed Element of bool the carrier of T;
existence
ex b1 being Subset of T st
( not b1 is empty & b1 is directed & b1 is finite )
proof end;
end;

theorem Th4: :: WAYBEL11:4
for T being with_suprema Poset
for D being non empty finite directed Subset of T holds sup D in D
proof end;

registration
cluster non empty trivial finite strict reflexive transitive antisymmetric with_suprema with_infima RelStr ;
existence
ex b1 being RelStr st
( b1 is trivial & b1 is reflexive & b1 is transitive & not b1 is empty & b1 is antisymmetric & b1 is with_suprema & b1 is with_infima & b1 is finite & b1 is strict )
proof end;
end;

registration
let T be finite 1-sorted ;
cluster -> finite Element of bool the carrier of T;
coherence
for b1 being Subset of T holds b1 is finite
;
end;

registration
let R be RelStr ;
cluster empty -> lower upper Element of bool the carrier of R;
coherence
for b1 being Subset of R st b1 is empty holds
( b1 is lower & b1 is upper )
proof end;
end;

registration
let R be non empty trivial RelStr ;
cluster -> upper Element of bool the carrier of R;
coherence
for b1 being Subset of R holds b1 is upper
proof end;
end;

theorem Th5: :: WAYBEL11:5
for T being non empty RelStr
for x being Element of T
for A being upper Subset of T st not x in A holds
A misses downarrow x
proof end;

theorem Th6: :: WAYBEL11:6
for T being non empty RelStr
for x being Element of T
for A being lower Subset of T st x in A holds
downarrow x c= A
proof end;

begin

definition
let T be non empty reflexive RelStr ;
let S be Subset of T;
attr S is inaccessible_by_directed_joins means :Def1: :: WAYBEL11:def 1
for D being non empty directed Subset of T st sup D in S holds
D meets S;
attr S is closed_under_directed_sups means :Def2: :: WAYBEL11:def 2
for D being non empty directed Subset of T st D c= S holds
sup D in S;
attr S is property(S) means :Def3: :: WAYBEL11:def 3
for D being non empty directed Subset of T st sup D in S holds
ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in S ) );
end;

:: deftheorem Def1 defines inaccessible_by_directed_joins WAYBEL11:def 1 :
for T being non empty reflexive RelStr
for S being Subset of T holds
( S is inaccessible_by_directed_joins iff for D being non empty directed Subset of T st sup D in S holds
D meets S );

:: deftheorem Def2 defines closed_under_directed_sups WAYBEL11:def 2 :
for T being non empty reflexive RelStr
for S being Subset of T holds
( S is closed_under_directed_sups iff for D being non empty directed Subset of T st D c= S holds
sup D in S );

:: deftheorem Def3 defines property(S) WAYBEL11:def 3 :
for T being non empty reflexive RelStr
for S being Subset of T holds
( S is property(S) iff for D being non empty directed Subset of T st sup D in S holds
ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in S ) ) );

notation
let T be non empty reflexive RelStr ;
let S be Subset of T;
synonym inaccessible S for inaccessible_by_directed_joins ;
synonym directly_closed S for closed_under_directed_sups ;
end;

registration
let T be non empty reflexive RelStr ;
cluster empty -> directly_closed property(S) Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is empty holds
( b1 is property(S) & b1 is closed_under_directed_sups )
proof end;
end;

registration
let T be non empty reflexive RelStr ;
cluster directly_closed property(S) Element of bool the carrier of T;
existence
ex b1 being Subset of T st
( b1 is property(S) & b1 is closed_under_directed_sups )
proof end;
end;

registration
let T be non empty reflexive RelStr ;
let S be property(S) Subset of T;
cluster S ` -> directly_closed ;
coherence
S ` is closed_under_directed_sups
proof end;
end;

definition
let T be non empty reflexive TopRelStr ;
attr T is Scott means :Def4: :: WAYBEL11:def 4
for S being Subset of T holds
( S is open iff ( S is inaccessible_by_directed_joins & S is upper ) );
end;

:: deftheorem Def4 defines Scott WAYBEL11:def 4 :
for T being non empty reflexive TopRelStr holds
( T is Scott iff for S being Subset of T holds
( S is open iff ( S is inaccessible_by_directed_joins & S is upper ) ) );

registration
let T be non empty finite reflexive transitive antisymmetric with_suprema RelStr ;
cluster -> inaccessible Element of bool the carrier of T;
coherence
for b1 being Subset of T holds b1 is inaccessible_by_directed_joins
proof end;
end;

definition
let T be non empty finite reflexive transitive antisymmetric with_suprema TopRelStr ;
redefine attr T is Scott means :: WAYBEL11:def 5
for S being Subset of T holds
( S is open iff S is upper );
compatibility
( T is Scott iff for S being Subset of T holds
( S is open iff S is upper ) )
proof end;
end;

:: deftheorem defines Scott WAYBEL11:def 5 :
for T being non empty finite reflexive transitive antisymmetric with_suprema TopRelStr holds
( T is Scott iff for S being Subset of T holds
( S is open iff S is upper ) );

registration
cluster non empty trivial TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete strict Scott TopRelStr ;
existence
ex b1 being TopLattice st
( b1 is trivial & b1 is complete & b1 is strict & not b1 is empty & b1 is Scott )
proof end;
end;

registration
let T be non empty reflexive RelStr ;
cluster [#] T -> inaccessible directly_closed ;
coherence
( [#] T is closed_under_directed_sups & [#] T is inaccessible_by_directed_joins )
proof end;
end;

registration
let T be non empty reflexive RelStr ;
cluster lower upper inaccessible directly_closed Element of bool the carrier of T;
existence
ex b1 being Subset of T st
( b1 is closed_under_directed_sups & b1 is lower & b1 is inaccessible_by_directed_joins & b1 is upper )
proof end;
end;

registration
let T be non empty reflexive RelStr ;
let S be inaccessible Subset of T;
cluster S ` -> directly_closed ;
coherence
S ` is closed_under_directed_sups
proof end;
end;

registration
let T be non empty reflexive RelStr ;
let S be directly_closed Subset of T;
cluster S ` -> inaccessible ;
coherence
S ` is inaccessible_by_directed_joins
proof end;
end;

theorem Th7: :: WAYBEL11:7
for T being non empty reflexive transitive up-complete Scott TopRelStr
for S being Subset of T holds
( S is closed iff ( S is closed_under_directed_sups & S is lower ) )
proof end;

theorem Th8: :: WAYBEL11:8
for T being non empty reflexive transitive antisymmetric up-complete TopRelStr
for x being Element of T holds downarrow x is closed_under_directed_sups
proof end;

theorem Th9: :: WAYBEL11:9
for T being complete Scott TopLattice
for x being Element of T holds Cl {x} = downarrow x
proof end;

theorem :: WAYBEL11:10
for T being complete Scott TopLattice holds T is T_0-TopSpace
proof end;

theorem Th11: :: WAYBEL11:11
for T being non empty reflexive transitive antisymmetric up-complete Scott TopRelStr
for x being Element of T holds downarrow x is closed
proof end;

theorem Th12: :: WAYBEL11:12
for T being up-complete Scott TopLattice
for x being Element of T holds (downarrow x) ` is open
proof end;

theorem Th13: :: WAYBEL11:13
for T being up-complete Scott TopLattice
for x being Element of T
for A being upper Subset of T st not x in A holds
(downarrow x) ` is a_neighborhood of A
proof end;

theorem :: WAYBEL11:14
for T being complete Scott TopLattice
for S being upper Subset of T ex F being Subset-Family of T st
( S = meet F & ( for X being Subset of T st X in F holds
X is a_neighborhood of S ) )
proof end;

theorem :: WAYBEL11:15
for T being Scott TopLattice
for S being Subset of T holds
( S is open iff ( S is upper & S is property(S) ) )
proof end;

registration
let T be complete TopLattice;
cluster lower -> property(S) Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is lower holds
b1 is property(S)
proof end;
end;

Lm2: for T being non empty reflexive TopRelStr holds [#] T is property(S)
proof end;

theorem :: WAYBEL11:16
for T being non empty reflexive transitive TopRelStr st the topology of T = { S where S is Subset of T : S is property(S) } holds
T is TopSpace-like
proof end;

begin

definition
let R be non empty RelStr ;
let N be net of R;
func lim_inf N -> Element of R equals :: WAYBEL11:def 6
"\/" ( { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } ,R);
correctness
coherence
"\/" ( { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } ,R) is Element of R
;
;
end;

:: deftheorem defines lim_inf WAYBEL11:def 6 :
for R being non empty RelStr
for N being net of R holds lim_inf N = "\/" ( { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } ,R);

definition
let R be non empty reflexive RelStr ;
let N be net of R;
let p be Element of R;
pred p is_S-limit_of N means :Def7: :: WAYBEL11:def 7
p <= lim_inf N;
end;

:: deftheorem Def7 defines is_S-limit_of WAYBEL11:def 7 :
for R being non empty reflexive RelStr
for N being net of R
for p being Element of R holds
( p is_S-limit_of N iff p <= lim_inf N );

definition
let R be non empty reflexive RelStr ;
func Scott-Convergence R -> Convergence-Class of R means :Def8: :: WAYBEL11:def 8
for N being strict net of R st N in NetUniv R holds
for p being Element of R holds
( [N,p] in it iff p is_S-limit_of N );
existence
ex b1 being Convergence-Class of R st
for N being strict net of R st N in NetUniv R holds
for p being Element of R holds
( [N,p] in b1 iff p is_S-limit_of N )
proof end;
uniqueness
for b1, b2 being Convergence-Class of R st ( for N being strict net of R st N in NetUniv R holds
for p being Element of R holds
( [N,p] in b1 iff p is_S-limit_of N ) ) & ( for N being strict net of R st N in NetUniv R holds
for p being Element of R holds
( [N,p] in b2 iff p is_S-limit_of N ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines Scott-Convergence WAYBEL11:def 8 :
for R being non empty reflexive RelStr
for b2 being Convergence-Class of R holds
( b2 = Scott-Convergence R iff for N being strict net of R st N in NetUniv R holds
for p being Element of R holds
( [N,p] in b2 iff p is_S-limit_of N ) );

theorem :: WAYBEL11:17
for R being complete LATTICE
for N being net of R
for p, q being Element of R st p is_S-limit_of N & N is_eventually_in downarrow q holds
p <= q
proof end;

theorem Th18: :: WAYBEL11:18
for R being complete LATTICE
for N being net of R
for p, q being Element of R st N is_eventually_in uparrow q holds
lim_inf N >= q
proof end;

definition
let R be non empty reflexive RelStr ;
let N be non empty NetStr of R;
redefine attr N is monotone means :Def9: :: WAYBEL11:def 9
for i, j being Element of N st i <= j holds
N . i <= N . j;
compatibility
( N is monotone iff for i, j being Element of N st i <= j holds
N . i <= N . j )
proof end;
end;

:: deftheorem Def9 defines monotone WAYBEL11:def 9 :
for R being non empty reflexive RelStr
for N being non empty NetStr of R holds
( N is monotone iff for i, j being Element of N st i <= j holds
N . i <= N . j );

definition
let R be non empty RelStr ;
let S be non empty set ;
let f be Function of S, the carrier of R;
func Net-Str (S,f) -> non empty strict NetStr of R means :Def10: :: WAYBEL11:def 10
( the carrier of it = S & the mapping of it = f & ( for i, j being Element of it holds
( i <= j iff it . i <= it . j ) ) );
existence
ex b1 being non empty strict NetStr of R st
( the carrier of b1 = S & the mapping of b1 = f & ( for i, j being Element of b1 holds
( i <= j iff b1 . i <= b1 . j ) ) )
proof end;
uniqueness
for b1, b2 being non empty strict NetStr of R st the carrier of b1 = S & the mapping of b1 = f & ( for i, j being Element of b1 holds
( i <= j iff b1 . i <= b1 . j ) ) & the carrier of b2 = S & the mapping of b2 = f & ( for i, j being Element of b2 holds
( i <= j iff b2 . i <= b2 . j ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines Net-Str WAYBEL11:def 10 :
for R being non empty RelStr
for S being non empty set
for f being Function of S, the carrier of R
for b4 being non empty strict NetStr of R holds
( b4 = Net-Str (S,f) iff ( the carrier of b4 = S & the mapping of b4 = f & ( for i, j being Element of b4 holds
( i <= j iff b4 . i <= b4 . j ) ) ) );

theorem Th19: :: WAYBEL11:19
for L being non empty 1-sorted
for N being non empty NetStr of L holds rng the mapping of N = { (N . i) where i is Element of N : verum }
proof end;

theorem Th20: :: WAYBEL11:20
for R being non empty RelStr
for S being non empty set
for f being Function of S, the carrier of R st rng f is directed holds
Net-Str (S,f) is directed
proof end;

registration
let R be non empty RelStr ;
let S be non empty set ;
let f be Function of S, the carrier of R;
cluster Net-Str (S,f) -> non empty strict monotone ;
coherence
Net-Str (S,f) is monotone
proof end;
end;

registration
let R be non empty transitive RelStr ;
let S be non empty set ;
let f be Function of S, the carrier of R;
cluster Net-Str (S,f) -> non empty transitive strict ;
coherence
Net-Str (S,f) is transitive
proof end;
end;

registration
let R be non empty reflexive RelStr ;
let S be non empty set ;
let f be Function of S, the carrier of R;
cluster Net-Str (S,f) -> non empty reflexive strict ;
coherence
Net-Str (S,f) is reflexive
proof end;
end;

theorem Th21: :: WAYBEL11:21
for R being non empty transitive RelStr
for S being non empty set
for f being Function of S, the carrier of R st S c= the carrier of R & Net-Str (S,f) is directed holds
Net-Str (S,f) in NetUniv R
proof end;

registration
let R be LATTICE;
cluster non empty reflexive transitive strict directed monotone NetStr of R;
existence
ex b1 being net of R st
( b1 is monotone & b1 is reflexive & b1 is strict )
proof end;
end;

theorem Th22: :: WAYBEL11:22
for R being complete LATTICE
for N being reflexive monotone net of R holds lim_inf N = sup N
proof end;

theorem Th23: :: WAYBEL11:23
for R being complete LATTICE
for N being constant net of R holds the_value_of N = lim_inf N
proof end;

theorem Th24: :: WAYBEL11:24
for R being complete LATTICE
for N being constant net of R holds the_value_of N is_S-limit_of N
proof end;

definition
let S be non empty 1-sorted ;
let e be Element of S;
func Net-Str e -> strict NetStr of S means :Def11: :: WAYBEL11:def 11
( the carrier of it = {e} & the InternalRel of it = {[e,e]} & the mapping of it = id {e} );
existence
ex b1 being strict NetStr of S st
( the carrier of b1 = {e} & the InternalRel of b1 = {[e,e]} & the mapping of b1 = id {e} )
proof end;
uniqueness
for b1, b2 being strict NetStr of S st the carrier of b1 = {e} & the InternalRel of b1 = {[e,e]} & the mapping of b1 = id {e} & the carrier of b2 = {e} & the InternalRel of b2 = {[e,e]} & the mapping of b2 = id {e} holds
b1 = b2
;
end;

:: deftheorem Def11 defines Net-Str WAYBEL11:def 11 :
for S being non empty 1-sorted
for e being Element of S
for b3 being strict NetStr of S holds
( b3 = Net-Str e iff ( the carrier of b3 = {e} & the InternalRel of b3 = {[e,e]} & the mapping of b3 = id {e} ) );

registration
let S be non empty 1-sorted ;
let e be Element of S;
cluster Net-Str e -> non empty strict ;
coherence
not Net-Str e is empty
proof end;
end;

theorem Th25: :: WAYBEL11:25
for S being non empty 1-sorted
for e being Element of S
for x being Element of (Net-Str e) holds x = e
proof end;

theorem Th26: :: WAYBEL11:26
for S being non empty 1-sorted
for e being Element of S
for x being Element of (Net-Str e) holds (Net-Str e) . x = e
proof end;

registration
let S be non empty 1-sorted ;
let e be Element of S;
cluster Net-Str e -> reflexive transitive antisymmetric strict directed ;
coherence
( Net-Str e is reflexive & Net-Str e is transitive & Net-Str e is directed & Net-Str e is antisymmetric )
proof end;
end;

theorem Th27: :: WAYBEL11:27
for S being non empty 1-sorted
for e being Element of S
for X being set holds
( Net-Str e is_eventually_in X iff e in X )
proof end;

theorem Th28: :: WAYBEL11:28
for S being non empty reflexive antisymmetric RelStr
for e being Element of S holds e = lim_inf (Net-Str e)
proof end;

theorem Th29: :: WAYBEL11:29
for S being non empty reflexive RelStr
for e being Element of S holds Net-Str e in NetUniv S
proof end;

theorem Th30: :: WAYBEL11:30
for R being complete LATTICE
for Z being net of R
for D being Subset of R st D = { ("/\" ( { (Z . k) where k is Element of Z : k >= j } ,R)) where j is Element of Z : verum } holds
( not D is empty & D is directed )
proof end;

theorem Th31: :: WAYBEL11:31
for L being complete LATTICE
for S being Subset of L holds
( S in the topology of (ConvergenceSpace (Scott-Convergence L)) iff ( S is inaccessible_by_directed_joins & S is upper ) )
proof end;

theorem Th32: :: WAYBEL11:32
for T being complete Scott TopLattice holds TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T)
proof end;

theorem Th33: :: WAYBEL11:33
for T being complete TopLattice st TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T) holds
for S being Subset of T holds
( S is open iff ( S is inaccessible_by_directed_joins & S is upper ) )
proof end;

theorem Th34: :: WAYBEL11:34
for T being complete TopLattice st TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T) holds
T is Scott
proof end;

registration
let R be complete LATTICE;
cluster Scott-Convergence R -> (CONSTANTS) ;
coherence
Scott-Convergence R is (CONSTANTS)
proof end;
end;

registration
let R be complete LATTICE;
cluster Scott-Convergence R -> (SUBNETS) ;
coherence
Scott-Convergence R is (SUBNETS)
proof end;
end;

theorem Th35: :: WAYBEL11:35
for S being non empty 1-sorted
for N being net of S
for X being set
for M being subnet of N st M = N " X holds
for i being Element of M holds M . i in X
proof end;

definition
let L be non empty reflexive RelStr ;
func sigma L -> Subset-Family of L equals :: WAYBEL11:def 12
the topology of (ConvergenceSpace (Scott-Convergence L));
coherence
the topology of (ConvergenceSpace (Scott-Convergence L)) is Subset-Family of L
by YELLOW_6:def 27;
end;

:: deftheorem defines sigma WAYBEL11:def 12 :
for L being non empty reflexive RelStr holds sigma L = the topology of (ConvergenceSpace (Scott-Convergence L));

theorem Th36: :: WAYBEL11:36
for L being complete continuous Scott TopLattice
for x being Element of L holds wayabove x is open
proof end;

theorem Th37: :: WAYBEL11:37
for T being complete TopLattice st the topology of T = sigma T holds
T is Scott
proof end;

Lm3: for T1, T2 being TopStruct st TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) & T1 is TopSpace-like holds
T2 is TopSpace-like
proof end;

Lm4: for S1, S2 being non empty 1-sorted st the carrier of S1 = the carrier of S2 holds
for N being strict net of S1 holds N is strict net of S2
;

Lm5: for S1, S2 being non empty 1-sorted st the carrier of S1 = the carrier of S2 holds
NetUniv S1 = NetUniv S2
proof end;

Lm6: for T1, T2 being non empty 1-sorted
for X being set
for N1 being net of T1
for N2 being net of T2 st N1 = N2 & N1 is_eventually_in X holds
N2 is_eventually_in X
proof end;

Lm7: for T1, T2 being non empty TopSpace st TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) holds
for N1 being net of T1
for N2 being net of T2 st N1 = N2 holds
for p1 being Point of T1
for p2 being Point of T2 st p1 = p2 & p1 in Lim N1 holds
p2 in Lim N2
proof end;

Lm8: for T1, T2 being non empty TopSpace st TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) holds
Convergence T1 = Convergence T2
proof end;

Lm9: for R1, R2 being non empty RelStr st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) & R1 is LATTICE holds
R2 is LATTICE
proof end;

Lm10: for R1, R2 being LATTICE
for X being set st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for p1 being Element of R1
for p2 being Element of R2 st p1 = p2 & X is_<=_than p1 holds
X is_<=_than p2
proof end;

Lm11: for R1, R2 being LATTICE
for X being set st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for p1 being Element of R1
for p2 being Element of R2 st p1 = p2 & X is_>=_than p1 holds
X is_>=_than p2
proof end;

Lm12: for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for D being set holds "\/" (D,R1) = "\/" (D,R2)
proof end;

Lm13: for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for D being set holds "/\" (D,R1) = "/\" (D,R2)
proof end;

Lm14: for R1, R2 being non empty reflexive RelStr st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for D being Subset of R1
for D9 being Subset of R2 st D = D9 & D is directed holds
D9 is directed
proof end;

Lm15: for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for p, q being Element of R1 st p << q holds
for p9, q9 being Element of R2 st p = p9 & q = q9 holds
p9 << q9
proof end;

Lm16: for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for N1 being net of R1
for N2 being net of R2 st N1 = N2 holds
lim_inf N1 = lim_inf N2
proof end;

Lm17: for R1, R2 being non empty reflexive RelStr
for X being non empty set
for N1 being net of R1
for N2 being net of R2 st N1 = N2 holds
for J1 being net_set of the carrier of N1,R1
for J2 being net_set of the carrier of N2,R2 st J1 = J2 holds
Iterated J1 = Iterated J2
proof end;

Lm18: for R1, R2 being non empty reflexive RelStr
for X being non empty set st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for N1 being net of R1
for N2 being net of R2 st N1 = N2 holds
for J1 being net_set of the carrier of N1,R1 holds J1 is net_set of the carrier of N2,R2
proof end;

Lm19: for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
Scott-Convergence R1 c= Scott-Convergence R2
proof end;

Lm20: for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
Scott-Convergence R1 = Scott-Convergence R2
proof end;

Lm21: for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
sigma R1 = sigma R2
proof end;

Lm22: for R1, R2 being LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) & R1 is complete holds
R2 is complete
proof end;

Lm23: for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) & R1 is continuous holds
R2 is continuous
proof end;

registration
let R be complete continuous LATTICE;
cluster Scott-Convergence R -> topological ;
coherence
Scott-Convergence R is topological
proof end;
end;

theorem :: WAYBEL11:38
for T being complete continuous Scott TopLattice
for x being Element of T
for N being net of T st N in NetUniv T holds
( x is_S-limit_of N iff x in Lim N )
proof end;

theorem Th39: :: WAYBEL11:39
for L being non empty complete Poset st Scott-Convergence L is (ITERATED_LIMITS) holds
L is continuous
proof end;

theorem :: WAYBEL11:40
for T being complete Scott TopLattice holds
( T is continuous iff Convergence T = Scott-Convergence T )
proof end;

theorem Th41: :: WAYBEL11:41
for T being complete Scott TopLattice
for S being upper Subset of T st S is Open holds
S is open
proof end;

theorem Th42: :: WAYBEL11:42
for L being non empty RelStr
for S being upper Subset of L
for x being Element of L st x in S holds
uparrow x c= S
proof end;

theorem Th43: :: WAYBEL11:43
for L being complete continuous Scott TopLattice
for p being Element of L
for S being Subset of L st S is open & p in S holds
ex q being Element of L st
( q << p & q in S )
proof end;

theorem Th44: :: WAYBEL11:44
for L being complete continuous Scott TopLattice
for p being Element of L holds { (wayabove q) where q is Element of L : q << p } is Basis of
proof end;

theorem Th45: :: WAYBEL11:45
for T being complete continuous Scott TopLattice holds { (wayabove x) where x is Element of T : verum } is Basis of T
proof end;

theorem :: WAYBEL11:46
for T being complete continuous Scott TopLattice
for S being upper Subset of T holds
( S is open iff S is Open )
proof end;

theorem :: WAYBEL11:47
for T being complete continuous Scott TopLattice
for p being Element of T holds Int (uparrow p) = wayabove p
proof end;

theorem :: WAYBEL11:48
for T being complete continuous Scott TopLattice
for S being Subset of T holds Int S = union { (wayabove x) where x is Element of T : wayabove x c= S }
proof end;