:: On the Order-consistent Topology of Complete and Uncomplete Lattices
:: by Ewa Gr\c{a}dzka
::
:: Received May 23, 2000
:: Copyright (c) 2000-2012 Association of Mizar Users


begin

definition
let T be non empty TopRelStr ;
attrT 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_:_
 for T being non empty TopRelStr holds
( T is upper iff  {  ((downarrow x) `) where x is Element of T : verum  }  is prebasis of T );

registration
cluster non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima up-complete strict Scott for TopRelStr ;
existence
 ex b1 being TopLattice st
( b1 is Scott & b1 is up-complete & b1 is strict )
proofend;
end;

definition
let T be non empty TopSpace-like reflexive TopRelStr ;
attrT 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_:_
 for T being non empty TopSpace-like reflexive TopRelStr holds
( T is order_consistent iff 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 ) ) );

registration
cluster1 -element TopSpace-like reflexive  -> 1 -element TopSpace-like reflexive upper for TopRelStr ;
coherence
 for b1 being 1 -element TopSpace-like reflexive TopRelStr holds b1 is upper
proofend;
end;

registration
cluster non empty trivial TopSpace-like reflexive transitive antisymmetric with_suprema with_infima up-complete strict upper for TopRelStr ;
existence
 ex b1 being TopLattice st
( b1 is upper & b1 is trivial & b1 is up-complete & b1 is strict )
proofend;
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
proofend;

theorem :: WAYBEL32:2
for T being non empty up-complete TopPoset st T is upper holds
T is order_consistent
proofend;

theorem Th3: :: WAYBEL32:3
for R being non empty reflexive transitive antisymmetric up-complete RelStr ex T being TopAugmentation of R st T is Scott
proofend;

theorem :: WAYBEL32:4
for R being non empty up-complete Poset
for T being TopAugmentation of R st T is Scott holds
T is correct ;

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

registration
let R be non empty reflexive transitive antisymmetric up-complete RelStr ;
cluster non empty correct reflexive transitive antisymmetric up-complete Scott for TopAugmentation of R;
existence
 ex b1 being TopAugmentation of R st
( b1 is Scott & b1 is correct )
proofend;
end;

theorem Th5: :: WAYBEL32:5
for T being non empty reflexive transitive antisymmetric up-complete Scott TopRelStr
for x being Element of T holds Cl {x} = downarrow x
proofend;

theorem Th6: :: WAYBEL32:6
for T being non empty up-complete Scott TopPoset holds T is order_consistent
proofend;

theorem Th7: :: WAYBEL32:7
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 )
proofend;

theorem Th8: :: WAYBEL32:8
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
proofend;

theorem Th9: :: WAYBEL32:9
for R being /\-complete Semilattice
for N being reflexive monotone net of R holds lim_inf N = sup N
proofend;

theorem Th10: :: WAYBEL32:10
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 &amp; S is upper ) )
proofend;

theorem Th11: :: WAYBEL32:11
for R being up-complete /\-complete Semilattice
for T being TopAugmentation of R st the topology of T = sigma R holds
T is Scott
proofend;

registration
let R be up-complete /\-complete Semilattice;
cluster non empty correct reflexive transitive antisymmetric up-complete strict Scott for TopAugmentation of R;
existence
 ex b1 being TopAugmentation of R st
( b1 is strict &amp; b1 is Scott &amp; b1 is correct )
proofend;
end;

theorem :: WAYBEL32:12
for S being up-complete /\-complete Semilattice
for T being Scott TopAugmentation of S holds sigma S = the topology of T
proofend;

theorem :: WAYBEL32:13
for T being non empty reflexive transitive antisymmetric up-complete Scott TopRelStr holds T is T_0-TopSpace
proofend;

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

theorem Th14: :: WAYBEL32:14
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
proofend;

theorem :: WAYBEL32:15
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 &amp; ( for X being Subset of T st X in F holds
X is a_neighborhood of S ) )
proofend;

theorem :: WAYBEL32:16
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 &amp; S is property(S) ) )
proofend;

theorem Th17: :: WAYBEL32:17
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)
proofend;

::Remark 1.4 (vi)
registration
let T be non empty reflexive transitive antisymmetric up-complete TopRelStr ;
cluster lower  ->  property(S) for Element of bool the carrier of T;
coherence
 for b1 being Subset of T st b1 is lower holds
b1 is property(S)
proofend;
end;

theorem :: WAYBEL32:18
for T being non empty finite up-complete Poset
for S being Subset of T holds S is inaccessible
proofend;

theorem Th19: :: WAYBEL32:19
for R being complete connected LATTICE
for T being Scott TopAugmentation of R
for x being Element of T holds (downarrow x) ` is open
proofend;

theorem :: WAYBEL32:20
for R being complete connected 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  }  ) )
proofend;

registration
let R be non empty up-complete Poset;
cluster non empty correct reflexive transitive antisymmetric up-complete order_consistent for TopAugmentation of R;
correctness
existence
ex b1 being correct TopAugmentation of R st b1 is order_consistent ;
proofend;
end;

registration
cluster non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete order_consistent for TopRelStr ;
correctness
existence
ex b1 being TopLattice st
( b1 is order_consistent &amp; b1 is complete );
proofend;
end;

theorem Th21: :: WAYBEL32:21
for R being non empty TopRelStr
for A being Subset of R st ( for x being Element of R holds downarrow x = Cl {x} ) &amp; A is open holds
A is upper
proofend;

theorem :: WAYBEL32:22
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
proofend;

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;
funcR *' f ->  non empty strict NetStr over S means :Def3: :: WAYBEL32:def 3
( RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of R, the InternalRel of R #) &amp; the mapping of it = f );
existence
 ex b1 being non empty strict NetStr over S st
( RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of R, the InternalRel of R #) &amp; the mapping of b1 = f )
proofend;
uniqueness
 for b1, b2 being non empty strict NetStr over S st RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of R, the InternalRel of R #) &amp; the mapping of b1 = f &amp; RelStr(# the carrier of b2, the InternalRel of b2 #) = RelStr(# the carrier of R, the InternalRel of R #) &amp; the mapping of b2 = f holds
b1 = b2 ;
end;

:: deftheorem Def3 defines *' WAYBEL32:def_3_:_
 for S being non empty 1-sorted
for R being non empty RelStr
for f being Function of the carrier of R, the carrier of S
for b4 being non empty strict NetStr over S holds
( b4 = R *' f iff ( RelStr(# the carrier of b4, the InternalRel of b4 #) = RelStr(# the carrier of R, the InternalRel of R #) &amp; the mapping of b4 = f ) );

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;
clusterR *' f ->  non empty transitive strict ;
coherence
 R *' f is transitive
proofend;
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;
clusterR *' f ->  non empty strict directed ;
coherence
 R *' f is directed
proofend;
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 &amp; ( for i being Element of N holds f . i = "/\" ( {  (N . k) where k is Element of N : k >= i  }  ,R) ) );
existence
 ex b1 being strict prenet of R ex f being Function of N,R st
( b1 = N *' f &amp; ( for i being Element of N holds f . i = "/\" ( {  (N . k) where k is Element of N : k >= i  }  ,R) ) )
proofend;
uniqueness
 for b1, b2 being strict prenet of R st ex f being Function of N,R st
( b1 = N *' f &amp; ( for i being Element of N holds f . i = "/\" ( {  (N . k) where k is Element of N : k >= i  }  ,R) ) ) &amp; ex f being Function of N,R st
( b2 = N *' f &amp; ( for i being Element of N holds f . i = "/\" ( {  (N . k) where k is Element of N : k >= i  }  ,R) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines inf_net WAYBEL32:def_4_:_
 for R being non empty RelStr
for N being prenet of R
for b3 being strict prenet of R holds
( b3 = inf_net N iff ex f being Function of N,R st
( b3 = N *' f &amp; ( for i being Element of N holds f . i = "/\" ( {  (N . k) where k is Element of N : k >= i  }  ,R) ) ) );

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

registration
let R be non empty RelStr ;
let N be net of R;
cluster inf_net N ->  strict ;
coherence
 inf_net N is directed ;
end;

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

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

theorem Th23: :: WAYBEL32:23
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  }
proofend;

theorem Th24: :: WAYBEL32:24
for R being up-complete /\-complete LATTICE
for N being net of R holds sup (inf_net N) = lim_inf N
proofend;

theorem :: WAYBEL32:25
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)
proofend;

theorem Th26: :: WAYBEL32:26
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
proofend;

theorem :: WAYBEL32:27
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
proofend;

theorem Th28: :: WAYBEL32:28
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
proofend;

theorem :: WAYBEL32:29
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 )
proofend;