:: On the Order-consistent Topology of Complete and Uncomplete
:: Lattices
:: by Ewa Gr\c{a}dzka
::
:: Received May 23, 2000
:: Copyright (c) 2000-2018 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, WAYBEL_9, WAYBEL_0, SUBSET_1, CANTOR_1, WAYBEL11,
STRUCT_0, REWRITE1, PRELAMB, YELLOW_9, PRE_TOPC, RELAT_2, ORDINAL2,
CONNSP_2, ZFMISC_1, TARSKI, SETFAM_1, XXREAL_0, RLVECT_3, WAYBEL19,
RCOMP_1, FINSET_1, YELLOW_2, RELAT_1, TOPS_1, LATTICE3, YELLOW_0,
FUNCT_1, ORDERS_2, LATTICES, SEQM_3, YELLOW_6, CARD_FIL, EQREL_1, PROB_1,
T_0TOPSP, ARYTM_3, WAYBEL_7, WAYBEL32, CARD_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FINSET_1,
SETFAM_1, FUNCT_2, DOMAIN_1, STRUCT_0, ORDERS_2, LATTICE3, PRE_TOPC,
TOPS_1, CONNSP_2, T_0TOPSP, YELLOW_0, WAYBEL_0, CANTOR_1, YELLOW_2,
WAYBEL_2, YELLOW_6, WAYBEL_9, RELSET_1, WAYBEL11, WAYBEL19, YELLOW_9;
constructors DOMAIN_1, TOPS_1, TOPS_2, CONNSP_2, LATTICE3, CANTOR_1, WAYBEL_1,
WAYBEL11, YELLOW_9, RELSET_1, WAYBEL_2;
registrations SUBSET_1, FUNCT_1, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0,
WAYBEL_3, YELLOW_6, WAYBEL11, YELLOW_9, WAYBEL21, YELLOW14, WAYBEL29,
TOPS_1, CARD_1, ORDINAL1, RELSET_1;
requirements SUBSET, BOOLE, NUMERALS;
begin
definition
let T be non empty TopRelStr;
attr T is upper means
:: WAYBEL32:def 1
the set of all (downarrow x)` where x is Element of T is prebasis of T;
end;
registration
cluster Scott up-complete strict for TopLattice;
end;
definition
let T be TopSpace-like non empty reflexive TopRelStr;
attr T is order_consistent means
:: 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
for V being a_neighborhood of x holds N is_eventually_in V;
end;
registration
cluster -> upper for 1-element reflexive TopSpace-like TopRelStr;
end;
registration
cluster upper trivial up-complete strict for TopLattice;
end;
theorem :: WAYBEL32:1
for T being upper up-complete non empty TopPoset
for A being Subset of T st A is open holds A is upper;
theorem :: WAYBEL32:2
for T being up-complete non empty TopPoset holds
T is upper implies T is order_consistent;
theorem :: WAYBEL32:3
for R being up-complete non empty reflexive transitive antisymmetric
RelStr ex T being TopAugmentation of R st T is Scott;
theorem :: WAYBEL32:4
for R being up-complete non empty Poset
for T being TopAugmentation of R holds T is Scott implies T is correct;
registration
let R be up-complete non empty reflexive transitive antisymmetric RelStr;
cluster Scott -> correct for TopAugmentation of R;
end;
registration
let R be up-complete non empty reflexive transitive antisymmetric RelStr;
cluster Scott correct for TopAugmentation of R;
end;
theorem :: WAYBEL32:5 :: Remark 1.4 (ii)
for T being Scott up-complete non empty reflexive transitive antisymmetric
TopRelStr, x being Element of T holds Cl {x} = downarrow x;
theorem :: WAYBEL32:6
for T being up-complete Scott non empty TopPoset holds
T is order_consistent;
theorem :: WAYBEL32:7
for R being /\-complete Semilattice, Z be net of R, D be Subset of R st
D = the set of all "/\"({Z.k where k is Element of Z: k >= j},R)
where j is Element of Z holds D is non empty directed;
theorem :: WAYBEL32:8
for R being /\-complete Semilattice, S being Subset of R,
a being Element of R holds a in S implies "/\"(S,R) <= a;
theorem :: WAYBEL32:9
for R being /\-complete Semilattice, N being monotone reflexive net of R
holds lim_inf N = sup N;
theorem :: 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 upper;
theorem :: WAYBEL32:11
for R being /\-complete up-complete Semilattice,
T being TopAugmentation of R st the topology of T = sigma R holds T is Scott;
registration
let R be /\-complete up-complete Semilattice;
cluster strict Scott correct for TopAugmentation of R;
end;
theorem :: WAYBEL32:12
for S being up-complete /\-complete Semilattice,
T being Scott TopAugmentation of S holds sigma S = the topology of T;
theorem :: WAYBEL32:13 :: Remark 1.4 (iii)
for T being Scott up-complete non empty reflexive transitive antisymmetric
TopRelStr holds T is T_0-TopSpace;
registration
let R be up-complete non empty reflexive transitive antisymmetric RelStr;
cluster -> up-complete for TopAugmentation of R;
end;
theorem :: WAYBEL32:14
for R being up-complete non empty reflexive transitive antisymmetric
RelStr for T being Scott TopAugmentation of R, x being Element of T,
A being upper Subset of T st not x in A
holds (downarrow x)` is a_neighborhood of A;
theorem :: WAYBEL32:15 ::Remark 1.4 (iv)
for R being up-complete non empty reflexive transitive antisymmetric
TopRelStr for T being Scott TopAugmentation of R, 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;
theorem :: WAYBEL32:16 ::Remark 1.4 (v)
for T being Scott up-complete non empty reflexive transitive antisymmetric
TopRelStr, S being Subset of T holds S is open iff S is upper property(S);
theorem :: WAYBEL32:17
for R being up-complete non empty reflexive transitive antisymmetric
TopRelStr, S being non empty directed Subset of R,
a being Element of R holds a in S implies a <= "\/"(S, R);
::Remark 1.4 (vi)
registration
let T be up-complete non empty reflexive transitive antisymmetric
TopRelStr;
cluster lower -> property(S) for Subset of T;
end;
theorem :: WAYBEL32:18
for T being finite up-complete non empty Poset,
S being Subset of T holds S is inaccessible;
theorem :: WAYBEL32:19
for R being complete connected LATTICE,
T being Scott TopAugmentation of R, x being Element of T holds
(downarrow x)` is open;
theorem :: WAYBEL32:20
for R being complete connected LATTICE,
T being Scott TopAugmentation of R, S being Subset of T holds
S is open iff S = the carrier of T or S in the set of all (downarrow x)`
where x is Element of T;
registration
let R be up-complete non empty Poset;
cluster order_consistent for correct TopAugmentation of R;
end;
registration
cluster order_consistent complete for TopLattice;
end;
theorem :: WAYBEL32:21
for R being non empty TopRelStr for A being Subset of R holds
(for x being Element of R holds downarrow x = Cl {x}) implies
(A is open implies A is upper);
theorem :: WAYBEL32:22
for R being non empty TopRelStr for A being Subset of R holds
(for x being Element of R holds downarrow x = Cl {x}) implies
for A being Subset of R st A is closed holds A is lower;
definition
let S be non empty 1-sorted, R be non empty RelStr,
f be Function of the carrier of R,the carrier of S;
func R*'f -> strict non empty NetStr over S means
:: WAYBEL32:def 3
the RelStr of it = the RelStr of R & the mapping of it = f;
end;
registration
let S be non empty 1-sorted, R be non empty transitive RelStr,
f be Function of the carrier of R,the carrier of S;
cluster R*'f -> transitive;
end;
registration
let S be non empty 1-sorted, R be non empty directed RelStr,
f be Function of the carrier of R,the carrier of S;
cluster R*'f -> directed;
end;
definition
let R be non empty RelStr, N be prenet of R;
func inf_net N -> strict prenet of R means
:: 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);
end;
registration
let R be non empty RelStr, N be net of R;
cluster inf_net N -> transitive;
end;
registration
let R be non empty RelStr, N be net of R;
cluster inf_net N -> directed;
end;
registration
let R be /\-complete non empty reflexive antisymmetric RelStr,
N be net of R;
cluster inf_net N -> monotone;
end;
registration
let R be /\-complete non empty reflexive antisymmetric RelStr,
N be net of R;
cluster inf_net N -> eventually-directed;
end;
theorem :: WAYBEL32:23
for R being non empty RelStr, N being net of R
holds rng the mapping of (inf_net N) =
the set of all "/\"({N.i where i is Element of N: i >= j},R) where
j is Element of N;
theorem :: WAYBEL32:24
for R being up-complete /\-complete LATTICE, N being net of R holds
sup inf_net N = lim_inf N;
theorem :: WAYBEL32:25
for R being up-complete /\-complete LATTICE, N being net of R,
i being Element of N holds sup inf_net N = lim_inf (N|i);
theorem :: WAYBEL32:26
for R being /\-complete Semilattice, N being net of R,
V being upper Subset of R holds
inf_net N is_eventually_in V implies N is_eventually_in V;
theorem :: WAYBEL32:27
for R being /\-complete Semilattice, N being net of R,
V being lower Subset of R holds
N is_eventually_in V implies inf_net N is_eventually_in V;
theorem :: WAYBEL32:28
for R being order_consistent up-complete /\-complete non empty TopLattice
for N being net of R, x being Element of R holds
x <= lim_inf N implies x is_a_cluster_point_of N;
theorem :: WAYBEL32:29
for R being order_consistent up-complete /\-complete non empty TopLattice
for N being eventually-directed net of R, x being Element of R holds
x <= lim_inf N iff x is_a_cluster_point_of N;