:: by Andrzej Trybulec

::

:: Received January 29, 1997

:: Copyright (c) 1997-2016 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_{1}() -> non empty set , F_{2}() -> non empty set , P_{1}[ set ], F_{3}( set ) -> set , F_{4}( set , set ) -> set } :

Irrel{ F

{ F_{3}(u) where u is Element of F_{1}() : P_{1}[u] } = { F_{4}(i,v) where i is Element of F_{2}(), v is Element of F_{1}() : P_{1}[v] }

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

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)

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

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 ;

existence

ex b_{1} being Subset of T st

( not b_{1} is empty & b_{1} is directed & b_{1} is finite )

end;
existence

ex b

( not b

proof end;

registration

ex b_{1} being RelStr st

( b_{1} is reflexive & b_{1} is transitive & b_{1} is 1 -element & b_{1} is antisymmetric & b_{1} is with_suprema & b_{1} is with_infima & b_{1} is finite & b_{1} is strict )
end;

cluster finite 1 -element strict reflexive transitive antisymmetric with_suprema with_infima for RelStr ;

existence ex b

( b

proof end;

registration
end;

registration

let R be RelStr ;

coherence

for b_{1} being Subset of R st b_{1} is empty holds

( b_{1} is lower & b_{1} is upper )
;

end;
coherence

for b

( b

registration
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

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

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;

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

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;

for D being non empty directed Subset of T st D c= S holds

sup D in S;

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

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

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

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;
let S be Subset of T;

synonym inaccessible S for inaccessible_by_directed_joins ;

synonym directly_closed S for closed_under_directed_sups ;

registration

let T be non empty reflexive RelStr ;

coherence

for b_{1} being Subset of T st b_{1} is empty holds

( b_{1} is property(S) & b_{1} is directly_closed )
;

end;
coherence

for b

( b

registration

let T be non empty reflexive RelStr ;

existence

ex b_{1} being Subset of T st

( b_{1} is property(S) & b_{1} is directly_closed )

end;
existence

ex b

( b

proof end;

registration

let T be non empty reflexive RelStr ;

let S be property(S) Subset of T;

coherence

S ` is closed_under_directed_sups

end;
let S be property(S) Subset of T;

coherence

S ` is closed_under_directed_sups

proof end;

definition

let T be non empty reflexive TopRelStr ;

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

for S being Subset of T holds

( S is open iff ( S is inaccessible & S is upper ) );

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

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 ;

coherence

for b_{1} being Subset of T holds b_{1} is inaccessible

end;
coherence

for b

proof end;

definition

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

( T is Scott iff for S being Subset of T holds

( S is open iff S is upper ) ) ;

end;
redefine attr T is Scott means :: WAYBEL11:def 5

for S being Subset of T holds

( S is open iff S is upper );

compatibility for S being Subset of T holds

( S is open iff S is upper );

( T is Scott iff for S being Subset of T holds

( S is open iff S is upper ) ) ;

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

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

ex b_{1} being TopLattice st

( b_{1} is complete & b_{1} is strict & b_{1} is 1 -element & b_{1} is Scott )
end;

cluster non empty 1 -element TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete strict Scott for TopRelStr ;

existence ex b

( b

proof end;

registration

let T be non empty reflexive RelStr ;

coherence

( [#] T is closed_under_directed_sups & [#] T is inaccessible_by_directed_joins )

end;
coherence

( [#] T is closed_under_directed_sups & [#] T is inaccessible_by_directed_joins )

proof end;

registration

let T be non empty reflexive RelStr ;

existence

ex b_{1} being Subset of T st

( b_{1} is directly_closed & b_{1} is lower & b_{1} is inaccessible & b_{1} is upper )

end;
existence

ex b

( b

proof end;

registration

let T be non empty reflexive RelStr ;

let S be inaccessible Subset of T;

coherence

S ` is closed_under_directed_sups

end;
let S be inaccessible Subset of T;

coherence

S ` is closed_under_directed_sups

proof end;

registration

let T be non empty reflexive RelStr ;

let S be directly_closed Subset of T;

coherence

S ` is inaccessible_by_directed_joins

end;
let S be directly_closed Subset of T;

coherence

S ` is inaccessible_by_directed_joins

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

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

for x being Element of T holds downarrow x is directly_closed

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;

for x being Element of T holds downarrow x is closed by Th8, Th7;

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

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

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

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;

coherence

for b_{1} being Subset of T st b_{1} is lower holds

b_{1} is property(S)

end;
coherence

for b

b

proof 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

T is TopSpace-like

proof end;

definition

let R be non empty RelStr ;

let N be net of R;

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;
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 "\/" ( { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } ,R);

coherence

"\/" ( { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } ,R) is Element of R;

;

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

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

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

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 ;

ex b_{1} 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_{1} iff p is_S-limit_of N )

for b_{1}, b_{2} 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_{1} 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_{2} iff p is_S-limit_of N ) ) holds

b_{1} = b_{2}

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

ex b

for N being strict net of R st N in NetUniv R holds

for p being Element of R holds

( [N,p] in b

proof end;

uniqueness for b

for p being Element of R holds

( [N,p] in b

for p being Element of R holds

( [N,p] in b

b

proof end;

:: deftheorem Def8 defines Scott-Convergence WAYBEL11:def 8 :

for R being non empty reflexive RelStr

for b_{2} being Convergence-Class of R holds

( b_{2} = 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_{2} iff p is_S-limit_of N ) );

for R being non empty reflexive RelStr

for b

( b

for p being Element of R holds

( [N,p] in b

:: 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

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

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;

( N is monotone iff for i, j being Element of N st i <= j holds

N . i <= N . j )

end;
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 for i, j being Element of N st i <= j holds

N . i <= N . j;

( N is monotone iff for i, j being Element of N st i <= j holds

N . i <= N . j )

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

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;

ex b_{1} being non empty strict NetStr over R st

( the carrier of b_{1} = S & the mapping of b_{1} = f & ( for i, j being Element of b_{1} holds

( i <= j iff b_{1} . i <= b_{1} . j ) ) )

for b_{1}, b_{2} being non empty strict NetStr over R st the carrier of b_{1} = S & the mapping of b_{1} = f & ( for i, j being Element of b_{1} holds

( i <= j iff b_{1} . i <= b_{1} . j ) ) & the carrier of b_{2} = S & the mapping of b_{2} = f & ( for i, j being Element of b_{2} holds

( i <= j iff b_{2} . i <= b_{2} . j ) ) holds

b_{1} = b_{2}

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

ex b

( the carrier of b

( i <= j iff b

proof end;

uniqueness for b

( i <= j iff b

( i <= j iff b

b

proof 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_{4} being non empty strict NetStr over R holds

( b_{4} = Net-Str (S,f) iff ( the carrier of b_{4} = S & the mapping of b_{4} = f & ( for i, j being Element of b_{4} holds

( i <= j iff b_{4} . i <= b_{4} . j ) ) ) );

for R being non empty RelStr

for S being non empty set

for f being Function of S, the carrier of R

for b

( b

( i <= j iff b

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 }

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

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;

coherence

Net-Str (S,f) is monotone

end;
let S be non empty set ;

let f be Function of S, the carrier of R;

coherence

Net-Str (S,f) is monotone

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

coherence

Net-Str (S,f) is transitive

end;
let S be non empty set ;

let f be Function of S, the carrier of R;

coherence

Net-Str (S,f) is transitive

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

coherence

Net-Str (S,f) is reflexive

end;
let S be non empty set ;

let f be Function of S, the carrier of R;

coherence

Net-Str (S,f) is reflexive

proof 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

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;

existence

ex b_{1} being net of R st

( b_{1} is monotone & b_{1} is reflexive & b_{1} is strict )

end;
existence

ex b

( b

proof end;

defpred S

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;

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;

ex b_{1} being strict NetStr over S st

( the carrier of b_{1} = {e} & the InternalRel of b_{1} = {[e,e]} & the mapping of b_{1} = id {e} )

for b_{1}, b_{2} being strict NetStr over S st the carrier of b_{1} = {e} & the InternalRel of b_{1} = {[e,e]} & the mapping of b_{1} = id {e} & the carrier of b_{2} = {e} & the InternalRel of b_{2} = {[e,e]} & the mapping of b_{2} = id {e} holds

b_{1} = b_{2}
;

end;
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 ( the carrier of it = {e} & the InternalRel of it = {[e,e]} & the mapping of it = id {e} );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def11 defines Net-Str WAYBEL11:def 11 :

for S being non empty 1-sorted

for e being Element of S

for b_{3} being strict NetStr over S holds

( b_{3} = Net-Str e iff ( the carrier of b_{3} = {e} & the InternalRel of b_{3} = {[e,e]} & the mapping of b_{3} = id {e} ) );

for S being non empty 1-sorted

for e being Element of S

for b

( b

registration
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

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

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;

coherence

( Net-Str e is reflexive & Net-Str e is transitive & Net-Str e is directed & Net-Str e is antisymmetric )

end;
let e be Element of S;

coherence

( Net-Str e is reflexive & Net-Str e is transitive & Net-Str e is directed & Net-Str e is antisymmetric )

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

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)

for e being Element of S holds e = lim_inf (Net-Str e)

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 )

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

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

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;

T is Scott by Th33;

registration
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

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 ;

the topology of (ConvergenceSpace (Scott-Convergence L)) is Subset-Family of L by YELLOW_6:def 24;

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

the topology of (ConvergenceSpace (Scott-Convergence L)) is Subset-Family of L by YELLOW_6:def 24;

:: deftheorem defines sigma WAYBEL11:def 12 :

for L being non empty reflexive RelStr holds sigma L = the topology of (ConvergenceSpace (Scott-Convergence L));

for L being non empty reflexive RelStr holds sigma L = the topology of (ConvergenceSpace (Scott-Convergence L));

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

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

L is continuous

proof end;

theorem :: WAYBEL11:40

for T being complete Scott TopLattice holds

( T is continuous iff Convergence T = Scott-Convergence T )

( T is continuous iff Convergence T = Scott-Convergence T )

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

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 )

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

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 )

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

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 }

for S being Subset of T holds Int S = union { (wayabove x) where x is Element of T : wayabove x c= S }

proof end;