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

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{ F₁() -> non empty set , F₂() -> non empty set , P₁[ set ], F₃( set ) -> set , F₄( set , set ) -> set } :

{ F₃(u) where u is Element of F₁() : P₁[u] } = { F₄(i,v) where i is Element of F₂(), v is Element of F₁() : P₁[v] }

provided

A1: for i being Element of F₂()
for u being Element of F₁() holds F₃(u) = F₄(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 for Element of bool the carrier of T;

existence
ex b₁ being Subset of T st
( not b₁ is empty & b₁ is directed & b₁ 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 finite 1 -element strict reflexive transitive antisymmetric with_suprema with_infima for RelStr ;

existence
ex b₁ being RelStr st
( b₁ is reflexive & b₁ is transitive & b₁ is 1 -element & b₁ is antisymmetric & b₁ is with_suprema & b₁ is with_infima & b₁ is finite & b₁ is strict )

proof end;

end;

registration

let T be finite 1-sorted ;

cluster -> finite for Element of bool the carrier of T;

coherence
for b₁ being Subset of T holds b₁ is finite ;

end;

registration

let R be RelStr ;

cluster empty -> lower upper for Element of bool the carrier of R;

coherence
for b₁ being Subset of R st b₁ is empty holds
( b₁ is lower & b₁ is upper ) ;

end;

registration

let R be 1 -element RelStr ;

cluster -> upper for Element of bool the carrier of R;

coherence
for b₁ being Subset of R holds b₁ 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;

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) for Element of bool the carrier of T;

coherence
for b₁ being Subset of T st b₁ is empty holds
( b₁ is property(S) & b₁ is directly_closed ) ;

end;

registration

let T be non empty reflexive RelStr ;

cluster directly_closed property(S) for Element of bool the carrier of T;

existence
ex b₁ being Subset of T st
( b₁ is property(S) & b₁ is directly_closed )

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 & 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 & S is upper ) ) );

registration

let T be non empty finite reflexive transitive antisymmetric with_suprema RelStr ;

cluster -> inaccessible for Element of bool the carrier of T;

coherence
for b₁ being Subset of T holds b₁ is inaccessible

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 ) ) ;

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 1 -element TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete strict Scott for TopRelStr ;

existence
ex b₁ being TopLattice st
( b₁ is complete & b₁ is strict & b₁ is 1 -element & b₁ 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 for Element of bool the carrier of T;

existence
ex b₁ being Subset of T st
( b₁ is directly_closed & b₁ is lower & b₁ is inaccessible & b₁ 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 directly_closed & 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 directly_closed

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 by Th8, Th7;

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) for Element of bool the carrier of T;

coherence
for b₁ being Subset of T st b₁ is lower holds
b₁ 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;

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 :: WAYBEL11:def 7
p <= lim_inf N;

end;

:: deftheorem 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 b₁ 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 b₁ iff p is_S-limit_of N )

proof end;

uniqueness
for b₁, b₂ 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 b₁ 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 b₂ iff p is_S-limit_of N ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines Scott-Convergence WAYBEL11:def 8 :
for R being non empty reflexive RelStr
for b₂ being Convergence-Class of R holds
( b₂ = 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 b₂ iff p is_S-limit_of N ) );

:: remarks, p.98

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 over 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 over 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 over 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 b₁ being non empty strict NetStr over R st
( the carrier of b₁ = S & the mapping of b₁ = f & ( for i, j being Element of b₁ holds
( i <= j iff b₁ . i <= b₁ . j ) ) )

proof end;

uniqueness
for b₁, b₂ being non empty strict NetStr over R st the carrier of b₁ = S & the mapping of b₁ = f & ( for i, j being Element of b₁ holds
( i <= j iff b₁ . i <= b₁ . j ) ) & the carrier of b₂ = S & the mapping of b₂ = f & ( for i, j being Element of b₂ holds
( i <= j iff b₂ . i <= b₂ . j ) ) holds
b₁ = b₂

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 b₄ being non empty strict NetStr over R holds
( b₄ = Net-Str (S,f) iff ( the carrier of b₄ = S & the mapping of b₄ = f & ( for i, j being Element of b₄ holds
( i <= j iff b₄ . i <= b₄ . j ) ) ) );

theorem Th19: :: WAYBEL11:19

for L being non empty 1-sorted
for N being non empty NetStr over 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 for NetStr over R;

existence
ex b₁ being net of R st
( b₁ is monotone & b₁ is reflexive & b₁ is strict )

proof end;

end;

defpred S₁[ set ] means verum;

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 by Th23;

definition

let S be non empty 1-sorted ;
let e be Element of S;

func Net-Str e -> strict NetStr over 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 b₁ being strict NetStr over S st
( the carrier of b₁ = {e} & the InternalRel of b₁ = {[e,e]} & the mapping of b₁ = id {e} )

proof end;

uniqueness
for b₁, b₂ being strict NetStr over S st the carrier of b₁ = {e} & the InternalRel of b₁ = {[e,e]} & the mapping of b₁ = id {e} & the carrier of b₂ = {e} & the InternalRel of b₂ = {[e,e]} & the mapping of b₂ = id {e} holds
b₁ = b₂ ;

end;

:: deftheorem Def11 defines Net-Str WAYBEL11:def 11 :
for S being non empty 1-sorted
for e being Element of S
for b₃ being strict NetStr over S holds
( b₃ = Net-Str e iff ( the carrier of b₃ = {e} & the InternalRel of b₃ = {[e,e]} & the mapping of b₃ = 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 & 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 & 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 by Th33;

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 24;

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
;

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
by Lm1;

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
by Lm1;

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
by Lm19;

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;