Volume 10, 1998

University of Bialystok

Copyright (c) 1998 Association of Mizar Users

### The abstract of the Mizar article:

### Introduction to Meet-Continuous Topological Lattices

**by****Artur Kornilowicz**- Received November 3, 1998
- MML identifier: YELLOW13

- [ Mizar article, MML identifier index ]

environ vocabulary FINSET_1, REALSET1, ORDERS_1, WAYBEL_9, URYSOHN1, PRE_TOPC, BOOLE, COMPTS_1, SUBSET_1, NATTRA_1, TSP_1, RELAT_2, WAYBEL_0, RELAT_1, SEQM_3, FUNCT_1, YELLOW_2, YELLOW_1, FILTER_2, ORDINAL2, YELLOW_0, WELLORD1, WAYBEL_1, SGRAPH1, BHSP_3, LATTICES, LATTICE3, TDLAT_3, CANTOR_1, SETFAM_1, RLVECT_3, TOPS_1, CONNSP_2, PRELAMB, TARSKI, WAYBEL_2, YELLOW13; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FINSET_1, STRUCT_0, ORDERS_1, PRE_TOPC, TOPS_1, GROUP_1, COMPTS_1, TDLAT_2, TDLAT_3, TSP_1, LATTICE3, CANTOR_1, REALSET1, BORSUK_1, URYSOHN1, YELLOW_0, WAYBEL_0, YELLOW_1, ORDERS_3, WAYBEL_1, YELLOW_2, YELLOW_3, WAYBEL_2, YELLOW_8, WAYBEL_9; constructors CANTOR_1, TOPS_1, TDLAT_2, TDLAT_3, TSP_1, URYSOHN1, YELLOW_8, WAYBEL_1, WAYBEL_3, YELLOW_9, ORDERS_3, GROUP_1, LATTICE3, XCMPLX_0, MEMBERED; clusters STRUCT_0, TOPS_1, FINSET_1, REALSET1, TDLAT_3, TEX_1, YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_0, WAYBEL_1, WAYBEL_3, YELLOW_8, YELLOW_9, WAYBEL11, WAYBEL12, YELLOW11, YELLOW12, BORSUK_1, RELSET_1, SUBSET_1, RLVECT_2, XREAL_0, MEMBERED, ZFMISC_1; requirements SUBSET, BOOLE; begin :: Preliminaries definition let S be finite 1-sorted; cluster the carrier of S -> finite; end; definition let S be trivial 1-sorted; cluster the carrier of S -> trivial; end; definition cluster trivial -> finite set; end; definition cluster trivial -> finite 1-sorted; end; definition cluster non trivial -> non empty 1-sorted; end; definition cluster strict non empty trivial 1-sorted; cluster strict non empty trivial RelStr; cluster strict non empty trivial TopRelStr; end; theorem :: YELLOW13:1 for T being being_T1 (non empty TopSpace), A being finite Subset of T holds A is closed; definition let T be being_T1 (non empty TopSpace); cluster finite -> closed Subset of T; end; definition let T be compact TopStruct; cluster [#]T -> compact; end; definition cluster strict non empty trivial TopSpace; end; definition cluster finite being_T1 -> discrete (non empty TopSpace); end; definition cluster finite -> compact TopSpace; end; theorem :: YELLOW13:2 for T being discrete non empty TopSpace holds T is_T4; theorem :: YELLOW13:3 for T being discrete non empty TopSpace holds T is_T3; theorem :: YELLOW13:4 for T being discrete non empty TopSpace holds T is_T2; theorem :: YELLOW13:5 for T being discrete non empty TopSpace holds T is_T1; definition cluster discrete non empty -> being_T4 being_T3 being_T2 being_T1 TopSpace; end; definition cluster being_T4 being_T1 -> being_T3 (non empty TopSpace); end; definition cluster being_T3 being_T1 -> being_T2 (non empty TopSpace); end; definition cluster being_T2 -> being_T1 TopSpace; end; definition cluster being_T1 -> T_0 TopSpace; end; theorem :: YELLOW13:6 for S being reflexive RelStr, T being reflexive transitive RelStr, f being map 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 map 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; definition 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; definition 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; definition 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; definition let T be non empty TopSpace, p be Point of T; cluster -> non empty basis of p; end; definition let T be TopStruct, p be Point of T; cluster non empty 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; definition let T be TopStruct, p be Point of T; cluster correct 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; definition let T be non empty TopSpace, p be Point of T; cluster non empty correct 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; definition let T be non empty TopSpace; cluster -> non empty basis of T; end; definition let T be TopStruct; cluster non empty 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 map of [:T,T qua TopSpace:], T st f = inf_op T holds f is continuous; end; definition cluster reflexive trivial -> topological_semilattice (non empty TopSpace-like TopRelStr); end; definition cluster reflexive trivial non empty 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; definition let T be topological_semilattice(non empty TopSpace-like TopRelStr), x be Element of T; cluster x"/\" -> continuous; end;

Back to top