Volume 12, 2000

University of Bialystok

Copyright (c) 2000 Association of Mizar Users

### The abstract of the Mizar article:

### Meet Continuous Lattices Revisited

**by****Artur Kornilowicz**- Received January 6, 2000
- MML identifier: WAYBEL30

- [ Mizar article, MML identifier index ]

environ vocabulary BOOLE, TARSKI, RELAT_2, ORDERS_1, QUANTAL1, YELLOW_1, WAYBEL_0, FILTER_2, LATTICE3, ORDINAL2, YELLOW_0, LATTICES, WAYBEL_2, REALSET1, YELLOW_9, WAYBEL11, BHSP_3, WAYBEL_9, PRE_TOPC, PROB_1, WAYBEL19, PRELAMB, CANTOR_1, SETFAM_1, DIRAF, SUBSET_1, FINSET_1, COMPTS_1, YELLOW_6, TOPS_1, WAYBEL29, YELLOW13, WAYBEL21, RELAT_1, PARTFUN1, FUNCT_3, FUNCT_1, TOPS_2, WAYBEL_3, RLVECT_3, TDLAT_3, CONNSP_2, FILTER_0, WAYBEL_8, WAYBEL_6, WAYBEL30; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELSET_1, FUNCT_1, FUNCT_2, FUNCT_3, STRUCT_0, FINSET_1, REALSET1, ORDERS_1, PRE_TOPC, TOPS_1, TOPS_2, COMPTS_1, CONNSP_2, TDLAT_3, LATTICE3, BORSUK_1, CANTOR_1, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_1, YELLOW_3, YELLOW_4, WAYBEL_2, WAYBEL_3, YELLOW_6, YELLOW_8, WAYBEL_6, WAYBEL_8, WAYBEL_9, WAYBEL11, YELLOW_9, WAYBEL19, WAYBEL21, YELLOW13, WAYBEL29; constructors CANTOR_1, GROUP_1, TOPS_1, TOPS_2, TDLAT_3, YELLOW_4, YELLOW_8, WAYBEL_1, WAYBEL_6, WAYBEL_8, WAYBEL19, ORDERS_3, URYSOHN1, WAYBEL21, YELLOW13, WAYBEL29, MEMBERED; clusters STRUCT_0, FINSET_1, BORSUK_1, SUBSET_1, TEX_1, TOPS_1, CANTOR_1, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_3, YELLOW_4, YELLOW_6, WAYBEL_0, WAYBEL_2, WAYBEL_3, WAYBEL_8, WAYBEL10, WAYBEL11, WAYBEL14, YELLOW_9, WAYBEL19, YELLOW12, WAYBEL_4, RELSET_1, YELLOW13, MEMBERED, ZFMISC_1; requirements BOOLE, SUBSET; begin theorem :: WAYBEL30:1 for x being set, D being non empty set holds x /\ union D = union {x /\ d where d is Element of D: not contradiction}; theorem :: WAYBEL30:2 for R being non empty reflexive transitive RelStr, D being non empty directed Subset of InclPoset Ids R holds union D is Ideal of R; :: Exercise 2.16 (i), p. 16 definition let R be non empty reflexive transitive RelStr; cluster InclPoset Ids R -> up-complete; end; theorem :: WAYBEL30:3 for R being non empty reflexive transitive RelStr, D being non empty directed Subset of InclPoset Ids R holds sup D = union D; theorem :: WAYBEL30:4 for R being Semilattice, D being non empty directed Subset of InclPoset Ids R, x being Element of InclPoset Ids R holds sup ({x} "/\" D) = union {x /\ d where d is Element of D: not contradiction} ; :: Exercise 4.8 (i), p. 33 definition let R be Semilattice; cluster InclPoset Ids R -> satisfying_MC; end; definition let R be non empty trivial RelStr; cluster -> trivial TopAugmentation of R; end; theorem :: WAYBEL30:5 for S being Scott complete TopLattice, T being complete LATTICE, A being Scott TopAugmentation of T st the RelStr of S = the RelStr of T holds the TopRelStr of A = the TopRelStr of S; theorem :: WAYBEL30:6 for N being Lawson complete TopLattice, T being complete LATTICE, A being Lawson correct TopAugmentation of T st the RelStr of N = the RelStr of T holds the TopRelStr of A = the TopRelStr of N; theorem :: WAYBEL30:7 for N being Lawson complete TopLattice for S being Scott TopAugmentation of N for A being Subset of N, J being Subset of S st A = J & J is closed holds A is closed; definition let A be complete LATTICE; cluster lambda A -> non empty; end; definition let S be Scott complete TopLattice; cluster InclPoset sigma S -> complete non trivial; end; definition let N be Lawson complete TopLattice; cluster InclPoset sigma N -> complete non trivial; cluster InclPoset lambda N -> complete non trivial; end; theorem :: WAYBEL30:8 for T being non empty reflexive RelStr holds sigma T c= {W\uparrow F where W, F is Subset of T: W in sigma T & F is finite} ; theorem :: WAYBEL30:9 for N being Lawson complete TopLattice holds lambda N = the topology of N; theorem :: WAYBEL30:10 for N being Lawson complete TopLattice holds sigma N c= lambda N; theorem :: WAYBEL30:11 for M, N being complete LATTICE st the RelStr of M = the RelStr of N holds lambda M = lambda N; theorem :: WAYBEL30:12 for N being Lawson complete TopLattice, X being Subset of N holds X in lambda N iff X is open; definition cluster trivial TopSpace-like -> Scott (reflexive non empty TopRelStr); end; definition cluster trivial -> Lawson (complete TopLattice); end; definition cluster strict continuous lower-bounded meet-continuous Scott (complete TopLattice); end; definition cluster strict continuous compact Hausdorff Lawson (complete TopLattice); end; theorem :: WAYBEL30:13 for N being meet-continuous LATTICE, A being Subset of N st A has_the_property_(S) holds uparrow A has_the_property_(S); definition let N be meet-continuous LATTICE, A be property(S) Subset of N; cluster uparrow A -> property(S); end; :: Proposition 2.1 (i), p. 153 theorem :: WAYBEL30:14 for N being meet-continuous Lawson (complete TopLattice), S being Scott TopAugmentation of N, A being Subset of N st A in lambda N holds uparrow A in sigma S; theorem :: WAYBEL30:15 for N being meet-continuous Lawson (complete TopLattice) for S being Scott TopAugmentation of N for A being Subset of N, J being Subset of S st A = J holds A is open implies uparrow J is open; theorem :: WAYBEL30:16 for N being meet-continuous Lawson (complete TopLattice) for S being Scott TopAugmentation of N for x being Point of S, y being Point of N for J being Basis of y st x = y holds {uparrow A where A is Subset of N: A in J} is Basis of x; :: Proposition 2.1 (ii), p. 153 theorem :: WAYBEL30:17 for N being meet-continuous Lawson (complete TopLattice) for S being Scott TopAugmentation of N for X being upper Subset of N, Y being Subset of S st X = Y holds Int X = Int Y; :: Proposition 2.1 (iii), p. 153 theorem :: WAYBEL30:18 for N being meet-continuous Lawson (complete TopLattice) for S being Scott TopAugmentation of N for X being lower Subset of N, Y being Subset of S st X = Y holds Cl X = Cl Y; theorem :: WAYBEL30:19 for M, N being complete LATTICE, LM being Lawson correct TopAugmentation of M, LN being Lawson correct TopAugmentation of N st InclPoset sigma N is continuous holds the topology of [:LM,LN qua TopSpace:] = lambda [:M,N:]; :: Proposition 2.2, p. 153 theorem :: WAYBEL30:20 for M, N being complete LATTICE, P being Lawson correct TopAugmentation of [:M,N:], Q being Lawson correct TopAugmentation of M, R being Lawson correct TopAugmentation of N st InclPoset sigma N is continuous holds the TopStruct of P = [:Q,R qua TopSpace:]; :: Theorem 2.3, p. 153, first conjunct theorem :: WAYBEL30:21 for N being meet-continuous Lawson (complete TopLattice), x being Element of N holds x"/\" is continuous; definition let N be meet-continuous Lawson (complete TopLattice), x be Element of N; cluster x"/\" -> continuous; end; :: Theorem 2.3, p. 153, second conjunct theorem :: WAYBEL30:22 for N being meet-continuous Lawson (complete TopLattice) st InclPoset sigma N is continuous holds N is topological_semilattice; :: Proposition 2.4, p. 153 theorem :: WAYBEL30:23 for N being meet-continuous Lawson (complete TopLattice) st InclPoset sigma N is continuous holds N is Hausdorff iff for X being Subset of [:N,N qua TopSpace:] st X = the InternalRel of N holds X is closed; :: Definition 2.5, p. 154 definition let N be non empty reflexive RelStr, X be Subset of N; func X^0 -> Subset of N equals :: WAYBEL30:def 1 { u where u is Element of N : for D being non empty directed Subset of N st u <= sup D holds X meets D }; end; definition let N be non empty reflexive antisymmetric RelStr, X be empty Subset of N; cluster X^0 -> empty; end; theorem :: WAYBEL30:24 for N being non empty reflexive RelStr, A, J being Subset of N st A c= J holds A^0 c= J^0; :: Remark 2.6 (i), p. 154 theorem :: WAYBEL30:25 for N being non empty reflexive RelStr, x being Element of N holds (uparrow x)^0 = wayabove x; :: Remark 2.6 (ii), p. 154 theorem :: WAYBEL30:26 for N being Scott TopLattice, X being upper Subset of N holds Int X c= X^0; :: Lemma 2.7 (i), p. 154 theorem :: WAYBEL30:27 for N being non empty reflexive RelStr, X, Y being Subset of N holds (X^0) \/ (Y^0) c= (X \/ Y)^0; :: Lemma 2.7 (ii), p. 154 theorem :: WAYBEL30:28 for N being meet-continuous LATTICE, X, Y being upper Subset of N holds (X^0) \/ (Y^0) = (X \/ Y)^0; :: Lemma 2.8, p. 154 theorem :: WAYBEL30:29 for S being meet-continuous Scott TopLattice, F being finite Subset of S holds Int uparrow F c= union { wayabove x where x is Element of S : x in F }; :: Theorem 2.9, p. 154 theorem :: WAYBEL30:30 for N being Lawson (complete TopLattice) holds N is continuous iff N is meet-continuous Hausdorff; definition cluster continuous Lawson -> Hausdorff (complete TopLattice); cluster meet-continuous Lawson Hausdorff -> continuous (complete TopLattice); end; :: Definition 2.10, p. 155 definition let N be non empty TopRelStr; attr N is with_small_semilattices means :: WAYBEL30:def 2 for x being Point of N ex J being basis of x st for A being Subset of N st A in J holds subrelstr A is meet-inheriting; attr N is with_compact_semilattices means :: WAYBEL30:def 3 for x being Point of N ex J being basis of x st for A being Subset of N st A in J holds subrelstr A is meet-inheriting & A is compact; attr N is with_open_semilattices means :: WAYBEL30:def 4 for x being Point of N ex J being Basis of x st for A being Subset of N st A in J holds subrelstr A is meet-inheriting; end; definition cluster with_open_semilattices -> with_small_semilattices (non empty TopSpace-like TopRelStr); cluster with_compact_semilattices -> with_small_semilattices (non empty TopSpace-like TopRelStr); cluster anti-discrete -> with_small_semilattices with_open_semilattices (non empty TopRelStr); cluster reflexive trivial TopSpace-like -> with_compact_semilattices (non empty TopRelStr); end; definition cluster strict trivial lower TopLattice; end; theorem :: WAYBEL30:31 for N being topological_semilattice (with_infima TopPoset), C being Subset of N st subrelstr C is meet-inheriting holds subrelstr Cl C is meet-inheriting; :: Theorem 2.11, p. 155 theorem :: WAYBEL30:32 for N being meet-continuous Lawson (complete TopLattice) for S being Scott TopAugmentation of N holds (for x being Point of S ex J being Basis of x st for W being Subset of S st W in J holds W is Filter of S) iff N is with_open_semilattices; :: Theorem 2.12, p. 155, r => l theorem :: WAYBEL30:33 for N being Lawson (complete TopLattice) for S being Scott TopAugmentation of N for x being Element of N holds {inf A where A is Subset of S : x in A & A in sigma S} c= {inf J where J is Subset of N : x in J & J in lambda N}; :: Theorem 2.12, p. 155 theorem :: WAYBEL30:34 for N being meet-continuous Lawson (complete TopLattice) for S being Scott TopAugmentation of N for x being Element of N holds {inf A where A is Subset of S : x in A & A in sigma S} = {inf J where J is Subset of N : x in J & J in lambda N}; :: Theorem 2.13, p. 155, 1 <=> 2 theorem :: WAYBEL30:35 for N being meet-continuous Lawson (complete TopLattice) holds N is continuous iff N is with_open_semilattices & InclPoset sigma N is continuous; definition cluster continuous -> with_open_semilattices (Lawson complete TopLattice); end; definition let N be continuous Lawson (complete TopLattice); cluster InclPoset sigma N -> continuous; end; :: Theorem 2.13, p. 155, 1 => 3 theorem :: WAYBEL30:36 for N being continuous Lawson (complete TopLattice) holds N is compact Hausdorff topological_semilattice with_open_semilattices; :: Theorem 2.13, p. 155, 3 => 3' theorem :: WAYBEL30:37 for N being Hausdorff topological_semilattice with_open_semilattices Lawson (complete TopLattice) holds N is with_compact_semilattices; :: Theorem 2.13, p. 155, 3' => 4 theorem :: WAYBEL30:38 for N being meet-continuous Hausdorff Lawson (complete TopLattice), x being Element of N holds x = "\/"({inf V where V is Subset of N: x in V & V in lambda N},N); :: Theorem 2.13, p. 155, 1 <=> 4 theorem :: WAYBEL30:39 for N being meet-continuous Lawson (complete TopLattice) holds N is continuous iff for x being Element of N holds x = "\/"({inf V where V is Subset of N: x in V & V in lambda N},N); :: Exercise 2.16, p. 156, 1 <=> 2 theorem :: WAYBEL30:40 for N being meet-continuous Lawson (complete TopLattice) holds N is algebraic iff N is with_open_semilattices & InclPoset sigma N is algebraic; definition let N be meet-continuous algebraic Lawson (complete TopLattice); cluster InclPoset sigma N -> algebraic; end;

Back to top