:: WAYBEL32 semantic presentation

definition

let T be non empty TopRelStr ;
attr T is upper means :Def1: :: WAYBEL32:def 1
{ ((downarrow x) ` ) where x is Element of T : verum } is prebasis of T;

end;

:: deftheorem Def1 defines upper WAYBEL32:def 1 :

registration

cluster up-complete strict Scott TopRelStr ;
existence

proof end;

end;

definition

let T be non empty reflexive TopSpace-like TopRelStr ;
attr T is order_consistent means :Def2: :: WAYBEL32:def 2
for x being Element of T holds
( downarrow x = Cl {x} & ( for N being eventually-directed net of T st x = sup N holds
for V being a_neighborhood of x holds N is_eventually_in V ) );

end;

:: deftheorem Def2 defines order_consistent WAYBEL32:def 2 :

registration

cluster non empty reflexive TopSpace-like trivial -> non empty reflexive TopSpace-like upper TopRelStr ;
coherence

proof end;

end;

registration

cluster up-complete strict trivial upper TopRelStr ;
existence

proof end;

end;

theorem Th1: :: WAYBEL32:1

for T being non empty up-complete upper TopPoset
for A being Subset of T st A is open holds
A is upper

proof end;

theorem :: WAYBEL32:2

for T being non empty up-complete TopPoset st T is upper holds
T is order_consistent

proof end;

theorem :: WAYBEL32:3

canceled;

theorem :: WAYBEL32:4

canceled;

theorem :: WAYBEL32:5

canceled;

theorem :: WAYBEL32:6

canceled;

theorem Th7: :: WAYBEL32:7

for R being non empty reflexive transitive antisymmetric up-complete RelStr ex T being TopAugmentation of R st T is Scott

proof end;

theorem Th8: :: WAYBEL32:8

for R being non empty up-complete Poset
for T being TopAugmentation of R st T is Scott holds
T is TopSpace-like

proof end;

registration

let R be non empty reflexive transitive antisymmetric up-complete RelStr ;
cluster Scott -> correct TopAugmentation of R;
coherence by Th8;

end;

registration

let R be non empty reflexive transitive antisymmetric up-complete RelStr ;
cluster correct Scott TopAugmentation of R;
existence

proof end;

end;

theorem Th9: :: WAYBEL32:9

for T being non empty reflexive transitive antisymmetric up-complete Scott TopRelStr
for x being Element of T holds Cl {x} = downarrow x

proof end;

theorem Th10: :: WAYBEL32:10

for T being non empty up-complete Scott TopPoset holds T is order_consistent

proof end;

theorem Th11: :: WAYBEL32:11

for R being /\-complete Semilattice
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 Th12: :: WAYBEL32:12

for R being /\-complete Semilattice
for S being Subset of R
for a being Element of R st a in S holds
"/\" S,R <= a

proof end;

theorem Th13: :: WAYBEL32:13

for R being /\-complete Semilattice
for N being reflexive monotone net of R holds lim_inf N = sup N

proof end;

theorem Th14: :: WAYBEL32:14

for R being /\-complete Semilattice
for S being Subset of R holds
( S in the topology of (ConvergenceSpace (Scott-Convergence R)) iff ( S is inaccessible_by_directed_joins & S is upper ) )

proof end;

theorem Th15: :: WAYBEL32:15

for R being up-complete /\-complete Semilattice
for T being TopAugmentation of R st the topology of T = sigma R holds
T is Scott

proof end;

registration

let R be up-complete /\-complete Semilattice;
cluster correct strict Scott TopAugmentation of R;
existence

proof end;

end;

theorem :: WAYBEL32:16

for S being up-complete /\-complete Semilattice
for T being Scott TopAugmentation of S holds sigma S = the topology of T

proof end;

theorem :: WAYBEL32:17

for T being non empty reflexive transitive antisymmetric up-complete Scott TopRelStr holds T is T_0-TopSpace

proof end;

registration

let R be non empty reflexive transitive antisymmetric up-complete RelStr ;
cluster -> up-complete TopAugmentation of R;
coherence ;

end;

theorem Th18: :: WAYBEL32:18

for R being non empty reflexive transitive antisymmetric up-complete RelStr
for T being Scott TopAugmentation of R
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 :: WAYBEL32:19

for R being non empty reflexive transitive antisymmetric up-complete TopRelStr
for T being Scott TopAugmentation of R
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 :: WAYBEL32:20

for T being non empty reflexive transitive antisymmetric up-complete Scott TopRelStr
for S being Subset of T holds
( S is open iff ( S is upper & S is property(S) ) )

proof end;

theorem Th21: :: WAYBEL32:21

for R being non empty reflexive transitive antisymmetric up-complete TopRelStr
for S being non empty directed Subset of R
for a being Element of R st a in S holds
a <= "\/" S,R

proof end;

registration

let T be non empty reflexive transitive antisymmetric up-complete TopRelStr ;
cluster lower -> property(S) Element of bool the carrier of T;
coherence

proof end;

end;

theorem :: WAYBEL32:22

for T being non empty up-complete finite Poset
for S being Subset of T holds S is inaccessible_by_directed_joins

proof end;

theorem Th23: :: WAYBEL32:23

for R being connected complete LATTICE
for T being Scott TopAugmentation of R
for x being Element of T holds (downarrow x) ` is open

proof end;

theorem :: WAYBEL32:24

for R being connected complete LATTICE
for T being Scott TopAugmentation of R
for S being Subset of T holds
( S is open iff ( S = the carrier of T or S in { ((downarrow x) ` ) where x is Element of T : verum } ) )

proof end;

registration

let R be non empty up-complete Poset;
cluster up-complete correct order_consistent TopAugmentation of R;
correctness

proof end;

end;

registration

cluster complete order_consistent TopRelStr ;
correctness

proof end;

end;

theorem Th25: :: WAYBEL32:25

for R being non empty TopRelStr
for A being Subset of R st ( for x being Element of R holds downarrow x = Cl {x} ) & A is open holds
A is upper

proof end;

theorem :: WAYBEL32:26

for R being non empty TopRelStr
for A being Subset of R st ( for x being Element of R holds downarrow x = Cl {x} ) holds
for A being Subset of R st A is closed holds
A is lower

proof end;

theorem Th27: :: WAYBEL32:27

for T being up-complete /\-complete LATTICE
for N being net of T
for i being Element of N holds lim_inf (N | i) = lim_inf N

proof end;

definition

let S be non empty 1-sorted ;
let R be non empty RelStr ;
let f be Function of the carrier of R,the carrier of S;
func R *' f -> non empty strict NetStr of S means :Def3: :: WAYBEL32:def 3
( RelStr(# the carrier of it,the InternalRel of it #) = RelStr(# the carrier of R,the InternalRel of R #) & the mapping of it = f );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def3 defines *' WAYBEL32:def 3 :

registration

let S be non empty 1-sorted ;
let R be non empty transitive RelStr ;
let f be Function of the carrier of R,the carrier of S;
cluster R *' f -> non empty transitive strict ;
coherence

proof end;

end;

registration

let S be non empty 1-sorted ;
let R be non empty directed RelStr ;
let f be Function of the carrier of R,the carrier of S;
cluster R *' f -> non empty strict directed ;
coherence

proof end;

end;

definition

let R be non empty RelStr ;
let N be prenet of R;
func inf_net N -> strict prenet of R means :Def4: :: WAYBEL32:def 4
ex f being Function of N,R st
( it = N *' f & ( for i being Element of N holds f . i = "/\" { (N . k) where k is Element of N : k >= i } ,R ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines inf_net WAYBEL32:def 4 :

registration

let R be non empty RelStr ;
let N be net of R;
cluster inf_net N -> transitive strict ;
coherence

proof end;

end;

registration

let R be non empty RelStr ;
let N be net of R;
cluster inf_net N -> transitive strict ;
coherence ;

end;

registration

let R be non empty reflexive antisymmetric /\-complete RelStr ;
let N be net of R;
cluster inf_net N -> transitive strict monotone ;
coherence

proof end;

end;

registration

let R be non empty reflexive antisymmetric /\-complete RelStr ;
let N be net of R;
cluster inf_net N -> transitive strict monotone eventually-directed ;
coherence ;

end;

theorem Th28: :: WAYBEL32:28

for R being non empty RelStr
for N being net of R holds rng the mapping of (inf_net N) = { ("/\" { (N . i) where i is Element of N : i >= j } ,R) where j is Element of N : verum }

proof end;

theorem Th29: :: WAYBEL32:29

for R being up-complete /\-complete LATTICE
for N being net of R holds sup (inf_net N) = lim_inf N

proof end;

theorem :: WAYBEL32:30

for R being up-complete /\-complete LATTICE
for N being net of R
for i being Element of N holds sup (inf_net N) = lim_inf (N | i)

proof end;

theorem Th31: :: WAYBEL32:31

for R being /\-complete Semilattice
for N being net of R
for V being upper Subset of R st inf_net N is_eventually_in V holds
N is_eventually_in V

proof end;

theorem :: WAYBEL32:32

for R being /\-complete Semilattice
for N being net of R
for V being lower Subset of R st N is_eventually_in V holds
inf_net N is_eventually_in V

proof end;

theorem Th33: :: WAYBEL32:33

for R being non empty up-complete /\-complete order_consistent TopLattice
for N being net of R
for x being Element of R st x <= lim_inf N holds
x is_a_cluster_point_of N

proof end;

theorem :: WAYBEL32:34

for R being non empty up-complete /\-complete order_consistent TopLattice
for N being eventually-directed net of R
for x being Element of R holds
( x <= lim_inf N iff x is_a_cluster_point_of N )

proof end;