:: Meet Continuous Lattices Revisited :: by Artur Korni{\l}owicz :: :: Received January 6, 2000 :: Copyright (c) 2000-2021 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, TARSKI, SUBSET_1, RELAT_2, ORDERS_2, WAYBEL_0, YELLOW_1, CARD_FIL, STRUCT_0, ZFMISC_1, XXREAL_0, LATTICE3, ORDINAL2, YELLOW_0, LATTICES, WAYBEL_2, YELLOW_9, WAYBEL11, REWRITE1, WAYBEL_9, PRE_TOPC, PROB_1, WAYBEL19, PRELAMB, ORDINAL1, SETFAM_1, CANTOR_1, DIRAF, RCOMP_1, FINSET_1, RLVECT_3, COMPTS_1, YELLOW_8, TOPS_1, WAYBEL29, YELLOW13, FUNCT_1, WAYBEL21, RELAT_1, PARTFUN1, MCART_1, TOPS_2, WAYBEL_3, TDLAT_3, CONNSP_2, EQREL_1, WAYBEL_8, WAYBEL_6, WAYBEL30, CARD_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, BINOP_1, FUNCT_3, SETFAM_1, DOMAIN_1, CARD_1, STRUCT_0, FINSET_1, ORDERS_2, 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_8, WAYBEL_6, WAYBEL_8, WAYBEL_9, WAYBEL11, YELLOW_9, WAYBEL19, WAYBEL21, YELLOW13, WAYBEL29; constructors TOPS_1, TOPS_2, TDLAT_3, CANTOR_1, ORDERS_3, WAYBEL_1, YELLOW_4, WAYBEL_6, WAYBEL_8, YELLOW_8, WAYBEL19, WAYBEL21, YELLOW13, WAYBEL29, COMPTS_1, WAYBEL_2; registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, STRUCT_0, TOPS_1, BORSUK_1, LATTICE3, YELLOW_0, TEX_1, WAYBEL_0, YELLOW_1, YELLOW_2, YELLOW_3, YELLOW_4, WAYBEL_2, WAYBEL_3, WAYBEL_4, YELLOW_6, WAYBEL_8, WAYBEL10, WAYBEL11, WAYBEL14, YELLOW_9, YELLOW12, WAYBEL19, YELLOW13, PRE_TOPC, CARD_1; requirements BOOLE, SUBSET; begin theorem :: WAYBEL30:1 for x being set, D being non empty set holds x /\ union D = union the set of all x /\ d where d is Element of D; 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 registration 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 the set of all x /\ d where d is Element of D; :: Exercise 4.8 (i), p. 33 registration let R be Semilattice; cluster InclPoset Ids R -> satisfying_MC; end; registration let R be 1-element RelStr; cluster -> trivial for 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; registration let A be complete LATTICE; cluster lambda A -> non empty; end; registration let S be Scott complete TopLattice; cluster InclPoset sigma S -> complete non trivial; end; registration 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; registration cluster TopSpace-like -> Scott for reflexive 1-element TopRelStr; end; registration cluster trivial -> Lawson for complete TopLattice; end; registration cluster strict continuous lower-bounded meet-continuous Scott for complete TopLattice; end; registration cluster strict continuous compact Hausdorff Lawson for complete TopLattice; end; scheme :: WAYBEL30:sch 1 EmptySch { A() -> Scott TopLattice, X() -> set, F(set) -> set }: { F(w) where w is Element of A(): w in {} } = {}; theorem :: WAYBEL30:13 for N being meet-continuous LATTICE, A being Subset of N st A is property(S) holds uparrow A is property(S); registration 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; registration 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; registration 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; registration cluster continuous Lawson -> Hausdorff for complete TopLattice; cluster meet-continuous Lawson Hausdorff -> continuous for 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; registration cluster with_open_semilattices -> with_small_semilattices for non empty TopSpace-like TopRelStr; cluster with_compact_semilattices -> with_small_semilattices for non empty TopSpace-like TopRelStr; cluster anti-discrete -> with_small_semilattices with_open_semilattices for non empty TopRelStr; cluster reflexive TopSpace-like -> with_compact_semilattices for 1-element TopRelStr; end; registration cluster strict trivial lower for 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 ; registration cluster continuous -> with_open_semilattices for Lawson complete TopLattice; end; registration 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 ; registration let N be meet-continuous algebraic Lawson complete TopLattice; cluster InclPoset sigma N -> algebraic; end;