:: WAYBEL32 semantic presentation

definition
let c1 be non empty TopRelStr ;
attr a1 is upper means :Def1: :: WAYBEL32:def 1
{ ((downarrow b1) ` ) where B is Element of a1 : verum } is prebasis of a1;
end;

:: deftheorem Def1 defines upper WAYBEL32:def 1 :
for b1 being non empty TopRelStr holds
( b1 is upper iff { ((downarrow b2) ` ) where B is Element of b1 : verum } is prebasis of b1 );

registration
cluster up-complete strict Scott TopRelStr ;
existence
ex b1 being TopLattice st
( b1 is Scott & b1 is up-complete & b1 is strict )
proof end;
end;

definition
let c1 be non empty reflexive TopSpace-like TopRelStr ;
attr a1 is order_consistent means :Def2: :: WAYBEL32:def 2
for b1 being Element of a1 holds
( downarrow b1 = Cl {b1} & ( for b2 being eventually-directed net of a1 st b1 = sup b2 holds
for b3 being a_neighborhood of b1 holds b2 is_eventually_in b3 ) );
end;

:: deftheorem Def2 defines order_consistent WAYBEL32:def 2 :
for b1 being non empty reflexive TopSpace-like TopRelStr holds
( b1 is order_consistent iff for b2 being Element of b1 holds
( downarrow b2 = Cl {b2} & ( for b3 being eventually-directed net of b1 st b2 = sup b3 holds
for b4 being a_neighborhood of b2 holds b3 is_eventually_in b4 ) ) );

registration
cluster non empty reflexive TopSpace-like trivial -> non empty reflexive TopSpace-like upper TopRelStr ;
coherence
for b1 being non empty reflexive TopSpace-like TopRelStr st b1 is trivial holds
b1 is upper
proof end;
end;

registration
cluster up-complete strict trivial upper TopRelStr ;
existence
ex b1 being TopLattice st
( b1 is upper & b1 is trivial & b1 is up-complete & b1 is strict )
proof end;
end;

theorem Th1: :: WAYBEL32:1
for b1 being non empty up-complete upper TopPoset
for b2 being Subset of b1 st b2 is open holds
b2 is upper
proof end;

theorem Th2: :: WAYBEL32:2
for b1 being non empty up-complete TopPoset st b1 is upper holds
b1 is order_consistent
proof end;

theorem Th3: :: WAYBEL32:3
canceled;

theorem Th4: :: WAYBEL32:4
canceled;

theorem Th5: :: WAYBEL32:5
canceled;

theorem Th6: :: WAYBEL32:6
canceled;

theorem Th7: :: WAYBEL32:7
for b1 being non empty reflexive transitive antisymmetric up-complete RelStr ex b2 being TopAugmentation of b1 st b2 is Scott
proof end;

theorem Th8: :: WAYBEL32:8
for b1 being non empty up-complete Poset
for b2 being TopAugmentation of b1 st b2 is Scott holds
b2 is TopSpace-like
proof end;

registration
let c1 be non empty reflexive transitive antisymmetric up-complete RelStr ;
cluster Scott -> correct TopAugmentation of a1;
coherence
for b1 being TopAugmentation of c1 st b1 is Scott holds
b1 is TopSpace-like by Th8;
end;

registration
let c1 be non empty reflexive transitive antisymmetric up-complete RelStr ;
cluster correct Scott TopAugmentation of a1;
existence
ex b1 being TopAugmentation of c1 st
( b1 is Scott & b1 is TopSpace-like )
proof end;
end;

theorem Th9: :: WAYBEL32:9
for b1 being non empty reflexive transitive antisymmetric up-complete Scott TopRelStr
for b2 being Element of b1 holds Cl {b2} = downarrow b2
proof end;

theorem Th10: :: WAYBEL32:10
for b1 being non empty up-complete Scott TopPoset holds b1 is order_consistent
proof end;

theorem Th11: :: WAYBEL32:11
for b1 being /\-complete Semilattice
for b2 being net of b1
for b3 being Subset of b1 st b3 = { ("/\" { (b2 . b5) where B is Element of b2 : b5 >= b4 } ,b1) where B is Element of b2 : verum } holds
( not b3 is empty & b3 is directed )
proof end;

theorem Th12: :: WAYBEL32:12
for b1 being /\-complete Semilattice
for b2 being Subset of b1
for b3 being Element of b1 st b3 in b2 holds
"/\" b2,b1 <= b3
proof end;

theorem Th13: :: WAYBEL32:13
for b1 being /\-complete Semilattice
for b2 being reflexive monotone net of b1 holds lim_inf b2 = sup b2
proof end;

theorem Th14: :: WAYBEL32:14
for b1 being /\-complete Semilattice
for b2 being Subset of b1 holds
( b2 in the topology of (ConvergenceSpace (Scott-Convergence b1)) iff ( b2 is inaccessible_by_directed_joins & b2 is upper ) )
proof end;

theorem Th15: :: WAYBEL32:15
for b1 being up-complete /\-complete Semilattice
for b2 being TopAugmentation of b1 st the topology of b2 = sigma b1 holds
b2 is Scott
proof end;

registration
let c1 be up-complete /\-complete Semilattice;
cluster correct strict Scott TopAugmentation of a1;
existence
ex b1 being TopAugmentation of c1 st
( b1 is strict & b1 is Scott & b1 is TopSpace-like )
proof end;
end;

theorem Th16: :: WAYBEL32:16
for b1 being up-complete /\-complete Semilattice
for b2 being Scott TopAugmentation of b1 holds sigma b1 = the topology of b2
proof end;

theorem Th17: :: WAYBEL32:17
for b1 being non empty reflexive transitive antisymmetric up-complete Scott TopRelStr holds b1 is T_0-TopSpace
proof end;

registration
let c1 be non empty reflexive transitive antisymmetric up-complete RelStr ;
cluster -> up-complete TopAugmentation of a1;
coherence
for b1 being TopAugmentation of c1 holds b1 is up-complete ;
end;

theorem Th18: :: WAYBEL32:18
for b1 being non empty reflexive transitive antisymmetric up-complete RelStr
for b2 being Scott TopAugmentation of b1
for b3 being Element of b2
for b4 being upper Subset of b2 st not b3 in b4 holds
(downarrow b3) ` is a_neighborhood of b4
proof end;

theorem Th19: :: WAYBEL32:19
for b1 being non empty reflexive transitive antisymmetric up-complete TopRelStr
for b2 being Scott TopAugmentation of b1
for b3 being upper Subset of b2 ex b4 being Subset-Family of b2 st
( b3 = meet b4 & ( for b5 being Subset of b2 st b5 in b4 holds
b5 is a_neighborhood of b3 ) )
proof end;

theorem Th20: :: WAYBEL32:20
for b1 being non empty reflexive transitive antisymmetric up-complete Scott TopRelStr
for b2 being Subset of b1 holds
( b2 is open iff ( b2 is upper & b2 is property(S) ) )
proof end;

theorem Th21: :: WAYBEL32:21
for b1 being non empty reflexive transitive antisymmetric up-complete TopRelStr
for b2 being non empty directed Subset of b1
for b3 being Element of b1 st b3 in b2 holds
b3 <= "\/" b2,b1
proof end;

registration
let c1 be non empty reflexive transitive antisymmetric up-complete TopRelStr ;
cluster lower -> property(S) Element of bool the carrier of a1;
coherence
for b1 being Subset of c1 st b1 is lower holds
b1 is property(S)
proof end;
end;

theorem Th22: :: WAYBEL32:22
for b1 being non empty up-complete finite Poset
for b2 being Subset of b1 holds b2 is inaccessible_by_directed_joins
proof end;

theorem Th23: :: WAYBEL32:23
for b1 being connected complete LATTICE
for b2 being Scott TopAugmentation of b1
for b3 being Element of b2 holds (downarrow b3) ` is open
proof end;

theorem Th24: :: WAYBEL32:24
for b1 being connected complete LATTICE
for b2 being Scott TopAugmentation of b1
for b3 being Subset of b2 holds
( b3 is open iff ( b3 = the carrier of b2 or b3 in { ((downarrow b4) ` ) where B is Element of b2 : verum } ) )
proof end;

registration
let c1 be non empty up-complete Poset;
cluster up-complete correct order_consistent TopAugmentation of a1;
correctness
existence
ex b1 being correct TopAugmentation of c1 st b1 is order_consistent;
proof end;
end;

registration
cluster complete order_consistent TopRelStr ;
correctness
existence
ex b1 being TopLattice st
( b1 is order_consistent & b1 is complete );
proof end;
end;

theorem Th25: :: WAYBEL32:25
for b1 being non empty TopRelStr
for b2 being Subset of b1 st ( for b3 being Element of b1 holds downarrow b3 = Cl {b3} ) & b2 is open holds
b2 is upper
proof end;

theorem Th26: :: WAYBEL32:26
for b1 being non empty TopRelStr
for b2 being Subset of b1 st ( for b3 being Element of b1 holds downarrow b3 = Cl {b3} ) holds
for b3 being Subset of b1 st b3 is closed holds
b3 is lower
proof end;

theorem Th27: :: WAYBEL32:27
for b1 being up-complete /\-complete LATTICE
for b2 being net of b1
for b3 being Element of b2 holds lim_inf (b2 | b3) = lim_inf b2
proof end;

definition
let c1 be non empty 1-sorted ;
let c2 be non empty RelStr ;
let c3 be Function of the carrier of c2,the carrier of c1;
func c2 *' c3 -> non empty strict NetStr of a1 means :Def3: :: WAYBEL32:def 3
( RelStr(# the carrier of a4,the InternalRel of a4 #) = RelStr(# the carrier of a2,the InternalRel of a2 #) & the mapping of a4 = a3 );
existence
ex b1 being non empty strict NetStr of c1 st
( RelStr(# the carrier of b1,the InternalRel of b1 #) = RelStr(# the carrier of c2,the InternalRel of c2 #) & the mapping of b1 = c3 )
proof end;
uniqueness
for b1, b2 being non empty strict NetStr of c1 st RelStr(# the carrier of b1,the InternalRel of b1 #) = RelStr(# the carrier of c2,the InternalRel of c2 #) & the mapping of b1 = c3 & RelStr(# the carrier of b2,the InternalRel of b2 #) = RelStr(# the carrier of c2,the InternalRel of c2 #) & the mapping of b2 = c3 holds
b1 = b2 ;
end;

:: deftheorem Def3 defines *' WAYBEL32:def 3 :
for b1 being non empty 1-sorted
for b2 being non empty RelStr
for b3 being Function of the carrier of b2,the carrier of b1
for b4 being non empty strict NetStr of b1 holds
( b4 = b2 *' b3 iff ( RelStr(# the carrier of b4,the InternalRel of b4 #) = RelStr(# the carrier of b2,the InternalRel of b2 #) & the mapping of b4 = b3 ) );

registration
let c1 be non empty 1-sorted ;
let c2 be non empty transitive RelStr ;
let c3 be Function of the carrier of c2,the carrier of c1;
cluster a2 *' a3 -> non empty transitive strict ;
coherence
c2 *' c3 is transitive
proof end;
end;

registration
let c1 be non empty 1-sorted ;
let c2 be non empty directed RelStr ;
let c3 be Function of the carrier of c2,the carrier of c1;
cluster a2 *' a3 -> non empty strict directed ;
coherence
c2 *' c3 is directed
proof end;
end;

definition
let c1 be non empty RelStr ;
let c2 be prenet of c1;
func inf_net c2 -> strict prenet of a1 means :Def4: :: WAYBEL32:def 4
ex b1 being Function of a2,a1 st
( a3 = a2 *' b1 & ( for b2 being Element of a2 holds b1 . b2 = "/\" { (a2 . b3) where B is Element of a2 : b3 >= b2 } ,a1 ) );
existence
ex b1 being strict prenet of c1ex b2 being Function of c2,c1 st
( b1 = c2 *' b2 & ( for b3 being Element of c2 holds b2 . b3 = "/\" { (c2 . b4) where B is Element of c2 : b4 >= b3 } ,c1 ) )
proof end;
uniqueness
for b1, b2 being strict prenet of c1 st ex b3 being Function of c2,c1 st
( b1 = c2 *' b3 & ( for b4 being Element of c2 holds b3 . b4 = "/\" { (c2 . b5) where B is Element of c2 : b5 >= b4 } ,c1 ) ) & ex b3 being Function of c2,c1 st
( b2 = c2 *' b3 & ( for b4 being Element of c2 holds b3 . b4 = "/\" { (c2 . b5) where B is Element of c2 : b5 >= b4 } ,c1 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines inf_net WAYBEL32:def 4 :
for b1 being non empty RelStr
for b2 being prenet of b1
for b3 being strict prenet of b1 holds
( b3 = inf_net b2 iff ex b4 being Function of b2,b1 st
( b3 = b2 *' b4 & ( for b5 being Element of b2 holds b4 . b5 = "/\" { (b2 . b6) where B is Element of b2 : b6 >= b5 } ,b1 ) ) );

registration
let c1 be non empty RelStr ;
let c2 be net of c1;
cluster inf_net a2 -> transitive strict ;
coherence
inf_net c2 is transitive
proof end;
end;

registration
let c1 be non empty RelStr ;
let c2 be net of c1;
cluster inf_net a2 -> transitive strict ;
coherence
inf_net c2 is directed ;
end;

registration
let c1 be non empty reflexive antisymmetric /\-complete RelStr ;
let c2 be net of c1;
cluster inf_net a2 -> transitive strict monotone ;
coherence
inf_net c2 is monotone
proof end;
end;

registration
let c1 be non empty reflexive antisymmetric /\-complete RelStr ;
let c2 be net of c1;
cluster inf_net a2 -> transitive strict monotone eventually-directed ;
coherence
inf_net c2 is eventually-directed ;
end;

theorem Th28: :: WAYBEL32:28
for b1 being non empty RelStr
for b2 being net of b1 holds rng the mapping of (inf_net b2) = { ("/\" { (b2 . b4) where B is Element of b2 : b4 >= b3 } ,b1) where B is Element of b2 : verum }
proof end;

theorem Th29: :: WAYBEL32:29
for b1 being up-complete /\-complete LATTICE
for b2 being net of b1 holds sup (inf_net b2) = lim_inf b2
proof end;

theorem Th30: :: WAYBEL32:30
for b1 being up-complete /\-complete LATTICE
for b2 being net of b1
for b3 being Element of b2 holds sup (inf_net b2) = lim_inf (b2 | b3)
proof end;

theorem Th31: :: WAYBEL32:31
for b1 being /\-complete Semilattice
for b2 being net of b1
for b3 being upper Subset of b1 st inf_net b2 is_eventually_in b3 holds
b2 is_eventually_in b3
proof end;

theorem Th32: :: WAYBEL32:32
for b1 being /\-complete Semilattice
for b2 being net of b1
for b3 being lower Subset of b1 st b2 is_eventually_in b3 holds
inf_net b2 is_eventually_in b3
proof end;

theorem Th33: :: WAYBEL32:33
for b1 being non empty up-complete /\-complete order_consistent TopLattice
for b2 being net of b1
for b3 being Element of b1 st b3 <= lim_inf b2 holds
b3 is_a_cluster_point_of b2
proof end;

theorem Th34: :: WAYBEL32:34
for b1 being non empty up-complete /\-complete order_consistent TopLattice
for b2 being eventually-directed net of b1
for b3 being Element of b1 holds
( b3 <= lim_inf b2 iff b3 is_a_cluster_point_of b2 )
proof end;