:: Introduction to Meet-Continuous Topological Lattices :: by Artur Korni{\l}owicz :: :: Received November 3, 1998 :: Copyright (c) 1998-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 STRUCT_0, XBOOLE_0, ZFMISC_1, ORDERS_2, WAYBEL_9, PRE_TOPC, FINSET_1, SUBSET_1, RCOMP_1, TARSKI, NATTRA_1, CARD_5, RELAT_2, FUNCT_1, WAYBEL_0, RELAT_1, SEQM_3, XXREAL_0, YELLOW_2, YELLOW_1, CARD_FIL, ORDINAL2, WELLORD1, WAYBEL_1, FUNCT_2, REWRITE1, LATTICES, YELLOW_0, LATTICE3, TDLAT_3, RLVECT_3, SETFAM_1, YELLOW_8, TOPS_1, CONNSP_2, PRELAMB, CANTOR_1, WAYBEL_2, YELLOW13, CARD_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, TOPS_2, FUNCT_1, RELSET_1, BINOP_1, FUNCT_2, FINSET_1, SETFAM_1, DOMAIN_1, STRUCT_0, ORDERS_2, PRE_TOPC, TOPS_1, COMPTS_1, TDLAT_2, TDLAT_3, LATTICE3, CANTOR_1, CONNSP_2, BORSUK_1, YELLOW_0, WAYBEL_0, YELLOW_1, ORDERS_3, WAYBEL_1, YELLOW_2, YELLOW_3, WAYBEL_2, YELLOW_8, WAYBEL_9; constructors SETFAM_1, TOPS_1, BORSUK_1, URYSOHN1, LATTICE3, TDLAT_2, TDLAT_3, T_0TOPSP, CANTOR_1, ORDERS_3, WAYBEL_1, WAYBEL_9, YELLOW_8, COMPTS_1, TOPS_2, WAYBEL_2; registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1, LATTICE3, YELLOW_0, TDLAT_3, TEX_1, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, WAYBEL_3, YELLOW_9, YELLOW11, YELLOW12, RELAT_1; requirements SUBSET, BOOLE; begin :: Preliminaries theorem :: YELLOW13:1 for T being T_1 non empty TopSpace, A being finite Subset of T holds A is closed; registration let T be T_1 non empty TopSpace; cluster finite -> closed for Subset of T; end; registration let T be compact TopStruct; cluster [#]T -> compact; end; registration cluster finite T_1 -> discrete for non empty TopSpace; end; registration cluster finite -> compact for TopSpace; end; theorem :: YELLOW13:2 for T being discrete non empty TopSpace holds T is normal; theorem :: YELLOW13:3 for T being discrete non empty TopSpace holds T is regular; theorem :: YELLOW13:4 for T being discrete non empty TopSpace holds T is T_2; theorem :: YELLOW13:5 for T being discrete non empty TopSpace holds T is T_1; registration cluster discrete non empty -> normal regular T_2 T_1 for TopSpace; end; registration cluster T_4 -> regular for non empty TopSpace; end; registration cluster T_3 -> T_2 for TopSpace; end; theorem :: YELLOW13:6 for S being reflexive RelStr, T being reflexive transitive RelStr , f being Function of S, T, X being Subset of S holds downarrow (f.:X) c= downarrow (f.:downarrow X); theorem :: YELLOW13:7 for S being reflexive RelStr, T being reflexive transitive RelStr, f being Function of S, T, X being Subset of S st f is monotone holds downarrow (f .:X) = downarrow (f.:downarrow X); theorem :: YELLOW13:8 for N being non empty Poset holds IdsMap N is one-to-one; registration let N be non empty Poset; cluster IdsMap N -> one-to-one; end; theorem :: YELLOW13:9 for N being finite LATTICE holds SupMap N is one-to-one; registration let N be finite LATTICE; cluster SupMap N -> one-to-one; end; theorem :: YELLOW13:10 for N being finite LATTICE holds N, InclPoset Ids N are_isomorphic; theorem :: YELLOW13:11 for N being complete non empty Poset, x being Element of N, X being non empty Subset of N holds x"/\" preserves_inf_of X; theorem :: YELLOW13:12 for N being complete non empty Poset, x being Element of N holds x"/\" is meet-preserving; registration let N be complete non empty Poset, x be Element of N; cluster x"/\" -> meet-preserving; end; begin :: On the basis of topological spaces theorem :: YELLOW13:13 for T being anti-discrete non empty TopStruct, p being Point of T holds {the carrier of T} is Basis of p; theorem :: YELLOW13:14 for T being anti-discrete non empty TopStruct, p being Point of T, D being Basis of p holds D = {the carrier of T}; theorem :: YELLOW13:15 for T being non empty TopSpace, P being Basis of T, p being Point of T holds {A where A is Subset of T: A in P & p in A} is Basis of p; theorem :: YELLOW13:16 for T being non empty TopStruct, A being Subset of T, p being Point of T holds p in Cl A iff for K being Basis of p, Q being Subset of T st Q in K holds A meets Q; theorem :: YELLOW13:17 for T being non empty TopStruct, A being Subset of T, p being Point of T holds p in Cl A iff ex K being Basis of p st for Q being Subset of T st Q in K holds A meets Q; definition let T be TopStruct, p be Point of T; mode basis of p -> Subset-Family of T means :: YELLOW13:def 1 for A being Subset of T st p in Int A ex P being Subset of T st P in it & p in Int P & P c= A; end; definition let T be non empty TopSpace, p be Point of T; redefine mode basis of p means :: YELLOW13:def 2 for A being a_neighborhood of p ex P being a_neighborhood of p st P in it & P c= A; end; theorem :: YELLOW13:18 for T being TopStruct, p being Point of T holds bool the carrier of T is basis of p; theorem :: YELLOW13:19 for T being non empty TopSpace, p being Point of T, P being basis of p holds P is non empty; registration let T be non empty TopSpace, p be Point of T; cluster -> non empty for basis of p; end; registration let T be TopStruct, p be Point of T; cluster non empty for basis of p; end; definition let T be TopStruct, p be Point of T, P be basis of p; attr P is correct means :: YELLOW13:def 3 for A being Subset of T holds A in P iff p in Int A; end; registration let T be TopStruct, p be Point of T; cluster correct for basis of p; end; theorem :: YELLOW13:20 for T being TopStruct, p being Point of T holds {A where A is Subset of T: p in Int A} is correct basis of p; registration let T be non empty TopSpace, p be Point of T; cluster non empty correct for basis of p; end; theorem :: YELLOW13:21 for T being anti-discrete non empty TopStruct, p being Point of T holds {the carrier of T} is correct basis of p; theorem :: YELLOW13:22 for T being anti-discrete non empty TopStruct, p being Point of T, D being correct basis of p holds D = {the carrier of T}; theorem :: YELLOW13:23 for T being non empty TopSpace, p being Point of T, P being Basis of p holds P is basis of p; definition let T be TopStruct; mode basis of T -> Subset-Family of T means :: YELLOW13:def 4 for p being Point of T holds it is basis of p; end; theorem :: YELLOW13:24 for T being TopStruct holds bool the carrier of T is basis of T; theorem :: YELLOW13:25 for T being non empty TopSpace, P being basis of T holds P is non empty; registration let T be non empty TopSpace; cluster -> non empty for basis of T; end; registration let T be TopStruct; cluster non empty for basis of T; end; theorem :: YELLOW13:26 for T being non empty TopSpace, P being basis of T holds the topology of T c= UniCl Int P; theorem :: YELLOW13:27 for T being TopSpace, P being Basis of T holds P is basis of T; definition let T be non empty TopSpace-like TopRelStr; attr T is topological_semilattice means :: YELLOW13:def 5 for f being Function of [:T,T qua TopSpace:], T st f = inf_op T holds f is continuous; end; registration cluster reflexive -> topological_semilattice for 1-element TopSpace-like TopRelStr; end; theorem :: YELLOW13:28 for T being topological_semilattice non empty TopSpace-like TopRelStr, x being Element of T holds x"/\" is continuous; registration let T be topological_semilatticenon empty TopSpace-like TopRelStr, x be Element of T; cluster x"/\" -> continuous; end;