Volume 12, 2000

University of Bialystok

Copyright (c) 2000 Association of Mizar Users

### The abstract of the Mizar article:

### On the Order-consistent Topology of Complete and Uncomplete Lattices

**by****Ewa Gradzka**- Received May 23, 2000
- MML identifier: WAYBEL32

- [ Mizar article, MML identifier index ]

environ vocabulary WAYBEL_9, WAYBEL_0, CANTOR_1, WAYBEL11, BHSP_3, PRELAMB, YELLOW_9, PRE_TOPC, RELAT_2, ORDINAL2, CONNSP_2, REALSET1, SETFAM_1, BOOLE, WAYBEL19, TARSKI, FINSET_1, SUBSET_1, YELLOW_2, RELAT_1, TOPS_1, QUANTAL1, LATTICE3, YELLOW_0, FUNCT_1, ORDERS_1, LATTICES, SEQM_3, YELLOW_6, PROB_1, T_0TOPSP, FUNCT_3, WAYBEL21, CAT_1, ARYTM_3, WAYBEL_7, WAYBEL32, RLVECT_3; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FINSET_1, STRUCT_0, REALSET1, FUNCT_2, ORDERS_1, LATTICE3, PRE_TOPC, TOPS_1, TOPS_2, CONNSP_2, T_0TOPSP, GROUP_1, YELLOW_0, WAYBEL_0, CANTOR_1, YELLOW_2, WAYBEL_2, YELLOW_6, WAYBEL_9, RELSET_1, WAYBEL11, WAYBEL19, YELLOW_9, WAYBEL21; constructors WAYBEL_1, CANTOR_1, TOPS_1, TOPS_2, WAYBEL_3, TSP_1, WAYBEL11, YELLOW_9, GROUP_1, TOLER_1, WAYBEL_5, WAYBEL21, BORSUK_1, MEMBERED, PARTFUN1; clusters STRUCT_0, LATTICE3, WAYBEL_0, FINSET_1, YELLOW_6, WAYBEL_3, WAYBEL11, WAYBEL21, YELLOW_9, RELSET_1, SUBSET_1, YELLOW14, WAYBEL29, MEMBERED, ZFMISC_1, FUNCT_2, PARTFUN1; requirements SUBSET, BOOLE; begin definition let T be non empty TopRelStr; attr T is upper means :: WAYBEL32:def 1 {(downarrow x)` where x is Element of T: not contradiction} is prebasis of T; end; definition cluster Scott up-complete strict 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; definition cluster trivial -> upper (non empty reflexive TopSpace-like TopRelStr); end; definition cluster upper trivial up-complete strict 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; canceled 4; theorem :: WAYBEL32:7 for R being up-complete (non empty reflexive transitive antisymmetric RelStr) ex T being TopAugmentation of R st T is Scott; theorem :: WAYBEL32:8 for R being up-complete (non empty Poset) for T being TopAugmentation of R holds T is Scott implies T is correct; definition let R be up-complete (non empty reflexive transitive antisymmetric RelStr); cluster Scott -> correct TopAugmentation of R; end; definition let R be up-complete (non empty reflexive transitive antisymmetric RelStr); cluster Scott correct TopAugmentation of R; end; theorem :: WAYBEL32:9 :: 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:10 for T being up-complete Scott (non empty TopPoset) holds T is order_consistent; theorem :: WAYBEL32:11 for R being /\-complete Semilattice, Z be net of R, D be Subset of R st D = {"/\"({Z.k where k is Element of Z: k >= j},R) where j is Element of Z: not contradiction} holds D is non empty directed; theorem :: WAYBEL32:12 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:13 for R being /\-complete Semilattice, N being monotone reflexive net of R holds lim_inf N = sup N; theorem :: 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 upper; theorem :: WAYBEL32:15 for R being /\-complete up-complete Semilattice, T being TopAugmentation of R st the topology of T = sigma R holds T is Scott; definition let R be /\-complete up-complete Semilattice; cluster strict Scott correct TopAugmentation of R; end; theorem :: WAYBEL32:16 for S being up-complete /\-complete Semilattice, T being Scott TopAugmentation of S holds sigma S = the topology of T; theorem :: WAYBEL32:17 :: Remark 1.4 (iii) for T being Scott up-complete (non empty reflexive transitive antisymmetric TopRelStr) holds T is T_0-TopSpace; definition let R be up-complete (non empty reflexive transitive antisymmetric RelStr); cluster -> up-complete TopAugmentation of R; end; theorem :: WAYBEL32:18 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:19 ::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:20 ::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:21 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) definition let T be up-complete (non empty reflexive transitive antisymmetric TopRelStr); cluster lower -> property(S) Subset of T; end; theorem :: WAYBEL32:22 for T being finite up-complete (non empty Poset), S being Subset of T holds S is inaccessible; theorem :: WAYBEL32:23 for R being complete connected LATTICE, T being Scott TopAugmentation of R, x being Element of T holds (downarrow x)` is open; theorem :: WAYBEL32:24 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 {(downarrow x)` where x is Element of T: not contradiction}; definition let R be up-complete (non empty Poset); cluster order_consistent (correct TopAugmentation of R); end; definition cluster order_consistent complete TopLattice; end; theorem :: WAYBEL32:25 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:26 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; theorem :: WAYBEL32:27 for T being up-complete /\-complete LATTICE, N being net of T for i being Element of N holds lim_inf (N|i) = lim_inf N; 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; definition 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; definition 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 map 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; definition let R be non empty RelStr, N be net of R; cluster inf_net N -> transitive; end; definition let R be non empty RelStr, N be net of R; cluster inf_net N -> directed; end; definition let R be /\-complete (non empty reflexive antisymmetric RelStr), N be net of R; cluster inf_net N -> monotone; end; definition let R be /\-complete (non empty reflexive antisymmetric RelStr), N be net of R; cluster inf_net N -> eventually-directed; end; theorem :: WAYBEL32:28 for R being non empty RelStr, 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: not contradiction}; theorem :: WAYBEL32:29 for R being up-complete /\-complete LATTICE, N being net of R holds sup inf_net N = lim_inf N; theorem :: WAYBEL32:30 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:31 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:32 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:33 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:34 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;

Back to top