:: On Discrete and Almost Discrete Topological Spaces :: by Zbigniew Karno :: :: Received April 6, 1993 :: Copyright (c) 1993-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, PRE_TOPC, SUBSET_1, TMAP_1, RCOMP_1, TARSKI, STRUCT_0, TOPS_1, TOPS_3, ZFMISC_1, SETFAM_1, TDLAT_3, NATTRA_1, COMPTS_1, TEX_1, CARD_1; notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, SETFAM_1, DOMAIN_1, CARD_1, STRUCT_0, PRE_TOPC, TOPS_1, TMAP_1, TDLAT_3, TOPS_3, COMPTS_1; constructors SETFAM_1, DOMAIN_1, TOPS_1, COMPTS_1, PCOMPS_1, TDLAT_3, TMAP_1, TOPS_3; registrations XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, TOPS_1, TDLAT_3, TMAP_1, CARD_1; requirements BOOLE, SUBSET, NUMERALS; begin :: 1. Properties of Subsets of a Topological Space with Modified Topology. reserve X for non empty TopSpace, D for Subset of X; theorem :: TEX_1:1 for B being Subset of X, C being Subset of X modified_with_respect_to D st B = C holds B is open implies C is open; theorem :: TEX_1:2 for B being Subset of X, C being Subset of X modified_with_respect_to D st B = C holds B is closed implies C is closed; theorem :: TEX_1:3 for C being Subset of X modified_with_respect_to D` st C = D holds C is closed; theorem :: TEX_1:4 for C being Subset of X modified_with_respect_to D st C = D holds D is dense implies C is dense & C is open; theorem :: TEX_1:5 for C being Subset of X modified_with_respect_to D st D c= C holds D is dense implies C is everywhere_dense; theorem :: TEX_1:6 for C being Subset of X modified_with_respect_to D` st C = D holds D is boundary implies C is boundary & C is closed; theorem :: TEX_1:7 for C being Subset of X modified_with_respect_to D` st C c= D holds D is boundary implies C is nowhere_dense; begin :: 2. Trivial Topological Spaces. definition let Y be non empty 1-sorted; redefine attr Y is trivial means :: TEX_1:def 1 ex d being Element of Y st the carrier of Y = {d}; end; registration cluster 1-element strict for TopStruct; cluster non trivial strict for TopStruct; end; theorem :: TEX_1:8 for Y being 1-element TopStruct st the topology of Y is non empty holds Y is almost_discrete implies Y is TopSpace-like; registration cluster 1-element strict for TopSpace; end; registration cluster -> anti-discrete discrete for 1-element TopSpace; cluster discrete anti-discrete -> trivial for non empty TopSpace; end; registration cluster non trivial strict for TopSpace; end; registration cluster non discrete -> non trivial for non empty TopSpace; cluster non anti-discrete -> non trivial for non empty TopSpace; end; begin :: 3. Examples of Discrete and Anti-discrete Topological Spaces. definition let D be set; func cobool D -> Subset-Family of D equals :: TEX_1:def 2 {{},D}; end; registration let D be set; cluster cobool D -> non empty; end; definition let D be set; func ADTS(D) -> TopStruct equals :: TEX_1:def 3 TopStruct(#D,cobool D#); end; registration let D be set; cluster ADTS(D) -> strict anti-discrete TopSpace-like; end; registration let D be non empty set; cluster ADTS(D) -> non empty; end; theorem :: TEX_1:9 for X being anti-discrete non empty TopSpace for A being Subset of X holds (A is empty implies Cl A = {}) & (A is non empty implies Cl A = the carrier of X); theorem :: TEX_1:10 for X being anti-discrete non empty TopSpace for A being Subset of X holds (A <> the carrier of X implies Int A = {}) & (A = the carrier of X implies Int A = the carrier of X); theorem :: TEX_1:11 for X being non empty TopSpace holds (for A being Subset of X holds (A is non empty implies Cl A = the carrier of X)) implies X is anti-discrete; theorem :: TEX_1:12 for X being non empty TopSpace holds (for A being Subset of X holds (A <> the carrier of X implies Int A = {})) implies X is anti-discrete; theorem :: TEX_1:13 for X being anti-discrete non empty TopSpace for A being Subset of X holds (A <> {} implies A is dense) & (A <> the carrier of X implies A is boundary); theorem :: TEX_1:14 for X being non empty TopSpace holds (for A being Subset of X holds (A <> {} implies A is dense)) implies X is anti-discrete; theorem :: TEX_1:15 for X being non empty TopSpace holds (for A being Subset of X holds (A <> the carrier of X implies A is boundary)) implies X is anti-discrete; registration let D be set; cluster 1TopSp D -> discrete; end; theorem :: TEX_1:16 for X being discrete non empty TopSpace for A being Subset of X holds Cl A = A & Int A = A; theorem :: TEX_1:17 for X being non empty TopSpace holds (for A being Subset of X holds Cl A = A) implies X is discrete; theorem :: TEX_1:18 for X being non empty TopSpace holds (for A being Subset of X holds Int A = A) implies X is discrete; theorem :: TEX_1:19 for D being non empty set holds ADTS(D) = 1TopSp(D) iff ex d0 being Element of D st D = {d0}; registration cluster discrete non anti-discrete strict non empty for TopSpace; cluster anti-discrete non discrete strict non empty for TopSpace; end; begin :: 4. An Example of a Topological Space. definition let D be set, d0 be Element of D; func STS(D,d0) -> TopStruct equals :: TEX_1:def 4 TopStruct (#D,(bool D) \ {A where A is Subset of D : d0 in A & A <> D}#); end; registration let D be set, d0 be Element of D; cluster STS(D,d0) -> strict TopSpace-like; end; registration let D be non empty set, d0 be Element of D; cluster STS(D,d0) -> non empty; end; reserve D for non empty set, d0 for Element of D; theorem :: TEX_1:20 for A being Subset of STS(D,d0) holds ({d0} c= A implies A is closed) & (A is non empty & A is closed implies {d0} c= A); theorem :: TEX_1:21 D \ {d0} is non empty implies for A being Subset of STS(D,d0) holds (A = {d0} implies A is closed & A is boundary) & (A is non empty & A is closed & A is boundary implies A = {d0}); theorem :: TEX_1:22 for A being Subset of STS(D,d0) holds (A c= D \ {d0} implies A is open) & (A <> D & A is open implies A c= D \ {d0}); theorem :: TEX_1:23 D \ {d0} is non empty implies for A being Subset of STS(D,d0) holds (A = D \ {d0} implies A is open & A is dense) & (A <> D & A is open & A is dense implies A = D \ {d0}); registration cluster non anti-discrete non discrete strict non empty for TopSpace; end; theorem :: TEX_1:24 for Y being non empty TopSpace holds the TopStruct of Y = the TopStruct of STS(D,d0) iff the carrier of Y = D & for A being Subset of Y holds ({d0} c= A implies A is closed) & (A is non empty & A is closed implies {d0} c= A); theorem :: TEX_1:25 for Y being non empty TopSpace holds the TopStruct of Y = the TopStruct of STS(D,d0) iff the carrier of Y = D & for A being Subset of Y holds (A c= D \ {d0} implies A is open) & (A <> D & A is open implies A c= D \ {d0}); theorem :: TEX_1:26 for Y being non empty TopSpace holds the TopStruct of Y = the TopStruct of STS(D,d0) iff the carrier of Y = D & for A being non empty Subset of Y holds Cl A = A \/ {d0}; theorem :: TEX_1:27 for Y being non empty TopSpace holds the TopStruct of Y = the TopStruct of STS(D,d0) iff the carrier of Y = D & for A being Subset of Y st A <> D holds Int A = A \ {d0}; theorem :: TEX_1:28 STS(D,d0) = ADTS(D) iff D = {d0}; theorem :: TEX_1:29 STS(D,d0) = 1TopSp(D) iff D = {d0}; theorem :: TEX_1:30 for D being non empty set, d0 being Element of D for A being Subset of STS(D,d0) st A = {d0} holds 1TopSp(D) = STS(D,d0) modified_with_respect_to A; begin :: 5. Discrete and Almost Discrete Spaces. definition let X be non empty TopSpace; redefine attr X is discrete means :: TEX_1:def 5 for A being non empty Subset of X holds A is not boundary; end; theorem :: TEX_1:31 X is discrete iff for A being Subset of X holds A <> the carrier of X implies A is not dense; registration cluster non almost_discrete -> non discrete non anti-discrete for non empty TopSpace; end; definition let X be non empty TopSpace; redefine attr X is almost_discrete means :: TEX_1:def 6 for A being non empty Subset of X holds A is not nowhere_dense; end; theorem :: TEX_1:32 X is almost_discrete iff for A being Subset of X holds A <> the carrier of X implies A is not everywhere_dense; theorem :: TEX_1:33 X is non almost_discrete iff ex A being non empty Subset of X st A is boundary & A is closed; theorem :: TEX_1:34 X is non almost_discrete iff ex A being Subset of X st A <> the carrier of X & A is dense & A is open; registration cluster almost_discrete non discrete non anti-discrete strict non empty for TopSpace; end; theorem :: TEX_1:35 for C being non empty set, c0 being Element of C holds C \ {c0} is non empty iff STS(C,c0) is non almost_discrete; registration cluster non almost_discrete strict non empty for TopSpace; end; theorem :: TEX_1:36 for A being non empty Subset of X st A is boundary holds X modified_with_respect_to A` is non almost_discrete; theorem :: TEX_1:37 for A being Subset of X st A <> the carrier of X & A is dense holds X modified_with_respect_to A is non almost_discrete;