:: WAYBEL11 semantic presentation

Lm1: for R, S being RelStr
for p, q being Element of R
for p', q' being Element of S st p = p' & q = q' & RelStr(# the carrier of R,the InternalRel of R #) = RelStr(# the carrier of S,the InternalRel of S #) & p <= q holds
p' <= q'

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

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 strict reflexive transitive antisymmetric with_suprema with_infima finite trivial RelStr ;
existence

proof end;

end;

registration

cluster strict non empty finite 1-sorted ;
existence

proof end;

end;

registration

let T be finite 1-sorted ;
cluster -> finite Element of bool the carrier of T;
coherence

proof end;

end;

registration

let R be RelStr ;
cluster {} R -> lower upper ;
coherence

proof end;

end;

registration

let R be non empty trivial RelStr ;
cluster -> upper Element of bool the carrier of R;
coherence

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 :

:: deftheorem Def2 defines closed_under_directed_sups WAYBEL11:def 2 :

:: deftheorem Def3 defines property(S) WAYBEL11:def 3 :

notation

let T be non empty reflexive RelStr ;
let S be Subset of T;
synonym inaccessible S for inaccessible_by_directed_joins S;
synonym directly_closed S for closed_under_directed_sups S;
synonym S has_the_property_(S) for property(S) S;

end;

registration

let T be non empty reflexive RelStr ;
cluster {} T -> lower upper directly_closed property(S) ;
coherence

proof end;

end;

registration

let T be non empty reflexive RelStr ;
cluster directly_closed property(S) Element of bool the carrier of T;
existence

proof end;

end;

registration

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

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 :

registration

let T be non empty reflexive transitive antisymmetric with_suprema finite RelStr ;
cluster -> finite inaccessible Element of bool the carrier of T;
coherence

proof end;

end;

definition

let T be non empty reflexive transitive antisymmetric with_suprema finite 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

proof end;

end;

:: deftheorem defines Scott WAYBEL11:def 5 :

registration

cluster non empty complete strict trivial Scott TopRelStr ;
existence

proof end;

end;

registration

let T be non empty reflexive RelStr ;
cluster [#] T -> inaccessible directly_closed ;
coherence

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

proof end;

end;

registration

let T be non empty reflexive RelStr ;
let S be inaccessible Subset of T;
cluster S ` -> directly_closed ;
coherence

proof end;

end;

registration

let T be non empty reflexive RelStr ;
let S be directly_closed Subset of T;
cluster S ` -> inaccessible ;
coherence

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

proof end;

end;

Lm2: for T being non empty reflexive TopRelStr holds [#] T has_the_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 has_the_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 ;

end;

:: deftheorem defines lim_inf WAYBEL11:def 6 :

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 :

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

proof end;

uniqueness

proof end;

end;

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

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

proof end;

end;

:: deftheorem Def9 defines monotone WAYBEL11:def 9 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines Net-Str WAYBEL11:def 10 :

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

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 monotone ;
coherence

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 monotone ;
coherence

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 reflexive strict monotone NetStr of R;
existence

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

proof end;

uniqueness ;

end;

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

registration

let S be non empty 1-sorted ;
let e be Element of S;
cluster Net-Str e -> non empty strict ;
coherence

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 -> non empty reflexive transitive antisymmetric strict directed ;
coherence

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

proof end;

end;

registration

let R be complete LATTICE;
cluster Scott-Convergence R -> (CONSTANTS) (SUBNETS) ;
coherence

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 by YELLOW_6:def 27;

end;

:: deftheorem defines sigma WAYBEL11:def 12 :

theorem Th36: :: WAYBEL11:36

for L being continuous complete 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 st the carrier of T1 = the carrier of T2 holds
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 D' being Subset of R2 st D = D' & D is directed holds
D' 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 p', q' being Element of R2 st p = p' & q = q' holds
p' << q'

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 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
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 continuous complete LATTICE;
cluster Scott-Convergence R -> (CONSTANTS) (SUBNETS) topological ;
coherence

proof end;

end;

theorem :: WAYBEL11:38

for T being continuous complete 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 continuous complete 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 continuous complete Scott TopLattice
for p being Element of L holds { (wayabove q) where q is Element of L : q << p } is Basis of p

proof end;

theorem Th45: :: WAYBEL11:45

for T being continuous complete Scott TopLattice holds { (wayabove x) where x is Element of T : verum } is Basis of T

proof end;

theorem :: WAYBEL11:46

for T being continuous complete 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 continuous complete Scott TopLattice
for p being Element of T holds Int (uparrow p) = wayabove p

proof end;

theorem :: WAYBEL11:48

for T being continuous complete 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;