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


begin

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 :
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 TopRelStr ;
existence
ex b1 being TopLattice st
( b1 is Scott & b1 is up-complete & b1 is strict )
proof end;
end;

definition
let T be non empty TopSpace-like reflexive 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 :
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
cluster non empty trivial TopSpace-like reflexive -> non empty TopSpace-like reflexive upper TopRelStr ;
coherence
for b1 being non empty TopSpace-like reflexive TopRelStr st b1 is trivial holds
b1 is upper
proof end;
end;

registration
cluster non empty trivial TopSpace-like reflexive transitive antisymmetric with_suprema with_infima up-complete strict 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 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 :: 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 ;

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

registration
let R be non empty reflexive transitive antisymmetric up-complete RelStr ;
cluster non empty correct reflexive transitive antisymmetric up-complete Scott TopAugmentation of R;
existence
ex b1 being TopAugmentation of R st
( b1 is Scott & b1 is TopSpace-like )
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 non empty correct reflexive transitive antisymmetric up-complete strict Scott TopAugmentation of R;
existence
ex b1 being TopAugmentation of R st
( b1 is strict & b1 is Scott & b1 is TopSpace-like )
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
for b1 being TopAugmentation of R holds b1 is up-complete ;
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
for b1 being Subset of T st b1 is lower holds
b1 is property(S)
proof end;
end;

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

theorem Th23: :: WAYBEL32:23
for R being complete connected 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 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 } ) )
proof end;

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

registration
cluster non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima 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 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;

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
ex b1 being non empty strict NetStr of S st
( RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of b1 = f )
proof end;
uniqueness
for b1, b2 being non empty strict NetStr of S st RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of b1 = f & RelStr(# the carrier of b2, the InternalRel of b2 #) = RelStr(# the carrier of R, the InternalRel of R #) & 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 of S holds
( b4 = R *' f iff ( RelStr(# the carrier of b4, the InternalRel of b4 #) = RelStr(# the carrier of R, the InternalRel of R #) & 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;
cluster R *' f -> non empty transitive strict ;
coherence
R *' f is transitive
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
R *' f is directed
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
ex b1 being strict prenet of R ex f being Function of N,R st
( b1 = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) )
proof end;
uniqueness
for b1, b2 being strict prenet of R st ex f being Function of N,R st
( b1 = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) ) & ex f being Function of N,R st
( b2 = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) ) holds
b1 = b2
proof end;
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 & ( 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
proof end;
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
proof end;
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 :: WAYBEL32:27
canceled;

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;