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

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 for TopRelStr ;

existence
ex b₁ being TopLattice st
( b₁ is Scott & b₁ is up-complete & b₁ 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 1 -element TopSpace-like reflexive -> 1 -element TopSpace-like reflexive upper for TopRelStr ;

coherence
for b₁ being 1 -element TopSpace-like reflexive TopRelStr holds b₁ is upper

proof end;

end;

registration

cluster non empty trivial TopSpace-like reflexive transitive antisymmetric with_suprema with_infima up-complete strict upper for TopRelStr ;

existence
ex b₁ being TopLattice st
( b₁ is upper & b₁ is trivial & b₁ is up-complete & b₁ 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 Th3: :: WAYBEL32:3

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: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 b₁ being TopAugmentation of R st b₁ is Scott holds
b₁ 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 b₁ being TopAugmentation of R st
( b₁ is Scott & b₁ is correct )

proof end;

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

proof end;

theorem Th6: :: WAYBEL32:6

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

proof end;

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 )

proof end;

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

proof end;

theorem Th9: :: WAYBEL32:9

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

proof end;

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 & S is upper ) )

proof end;

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

proof end;

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 b₁ being TopAugmentation of R st
( b₁ is strict & b₁ is Scott & b₁ is correct )

proof end;

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

proof end;

theorem :: WAYBEL32:13

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 for TopAugmentation of R;

coherence
for b₁ being TopAugmentation of R holds b₁ 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

proof end;

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 & ( for X being Subset of T st X in F holds
X is a_neighborhood of S ) )

proof end;

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 & S is property(S) ) )

proof end;

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)

proof end;

::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 b₁ being Subset of T st b₁ is lower holds
b₁ is property(S)

proof end;

end;

theorem :: WAYBEL32:18

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

proof end;

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

proof end;

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 } ) )

proof end;

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 b₁ being correct TopAugmentation of R st b₁ is order_consistent ;

proof end;

end;

registration

cluster non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete order_consistent for TopRelStr ;

correctness
existence
ex b₁ being TopLattice st
( b₁ is order_consistent & b₁ is complete );

proof end;

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} ) & A is open holds
A is upper

proof end;

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

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 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 #) & the mapping of it = f );

existence
ex b₁ being non empty strict NetStr over S st
( RelStr(# the carrier of b₁, the InternalRel of b₁ #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of b₁ = f )

proof end;

uniqueness
for b₁, b₂ being non empty strict NetStr over S st RelStr(# the carrier of b₁, the InternalRel of b₁ #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of b₁ = f & RelStr(# the carrier of b₂, the InternalRel of b₂ #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of b₂ = f holds
b₁ = b₂ ;

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 b₄ being non empty strict NetStr over S holds
( b₄ = R *' f iff ( RelStr(# the carrier of b₄, the InternalRel of b₄ #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of b₄ = 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 b₁ being strict prenet of R ex f being Function of N,R st
( b₁ = 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 b₁, b₂ being strict prenet of R st ex f being Function of N,R st
( b₁ = 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
( b₂ = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines inf_net WAYBEL32:def 4 :
for R being non empty RelStr
for N being prenet of R
for b₃ being strict prenet of R holds
( b₃ = inf_net N iff ex f being Function of N,R st
( b₃ = 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 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 }

proof end;

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

proof end;

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)

proof end;

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

proof end;

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

proof end;

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

proof end;

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 )

proof end;