:: Maximal Discrete Subspaces of Almost Discrete Topological Spaces :: by Zbigniew Karno :: :: Received November 5, 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, ZFMISC_1, SUBSET_1, TARSKI, STRUCT_0, PRE_TOPC, RELAT_1, NATTRA_1, TDLAT_3, RCOMP_1, TOPS_3, TOPS_1, SETFAM_1, FUNCT_1, ORDINAL2, COMPTS_1, TEX_1, BORSUK_1, TEX_2, CARD_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, DOMAIN_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, CARD_1, STRUCT_0, PRE_TOPC, TOPS_1, TOPS_2, BORSUK_1, TSEP_1, TDLAT_3, TOPS_3, COMPTS_1, TEX_1; constructors SETFAM_1, TOPS_1, TOPS_2, COMPTS_1, REALSET2, BORSUK_1, TSEP_1, TDLAT_3, TOPS_3, TEX_1; registrations SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, ZFMISC_1, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1, TDLAT_3, TEX_1, CARD_1; requirements BOOLE, SUBSET; begin :: 1. Proper Subsets of 1-sorted Structures. theorem :: TEX_2:1 for A being non empty set, B being 1-element set st A c= B holds A = B; theorem :: TEX_2:2 for A being 1-element set, B being set st A /\ B is non empty holds A c= B; registration let S be 1-element set; cluster proper -> empty for Subset of S; cluster non empty -> non proper for Subset of S; end; theorem :: TEX_2:3 for S being non empty set, y being Element of S holds {y} is proper implies S is non trivial; theorem :: TEX_2:4 for S being non trivial set, y being Element of S holds {y} is proper; registration let S be 1-element set; cluster non proper -> trivial for non empty Subset of S; end; registration let S be non trivial set; cluster trivial -> proper for non empty Subset of S; cluster non proper -> non trivial for non empty Subset of S; end; registration let S be non trivial set; cluster trivial proper for non empty Subset of S; cluster non trivial non proper for non empty Subset of S; end; theorem :: TEX_2:5 for Y being non empty 1-sorted, y being Element of Y holds {y} is proper implies Y is non trivial; theorem :: TEX_2:6 for Y being non trivial 1-sorted, y being Element of Y holds {y} is proper; registration let Y be 1-element 1-sorted; cluster -> non proper for non empty Subset of Y; cluster non proper -> trivial for non empty Subset of Y; end; registration let Y be non trivial 1-sorted; cluster trivial -> proper for non empty Subset of Y; cluster non proper -> non trivial for non empty Subset of Y; end; registration let Y be non trivial 1-sorted; cluster trivial proper for non empty Subset of Y; cluster non trivial non proper for non empty Subset of Y; end; registration let Y be non trivial 1-sorted; cluster non empty trivial proper for Subset of Y; end; registration let X be non empty set; let A be proper Subset of X; cluster A` -> non empty; end; begin :: 2. Proper Subspaces of Topological Spaces. theorem :: TEX_2:7 for Y0, Y1 being TopStruct st the TopStruct of Y0 = the TopStruct of Y1 holds Y0 is TopSpace-like implies Y1 is TopSpace-like; definition let Y be TopStruct; let IT be SubSpace of Y; attr IT is proper means :: TEX_2:def 1 for A being Subset of Y st A = the carrier of IT holds A is proper; end; reserve Y for TopStruct; theorem :: TEX_2:8 for Y0 being SubSpace of Y, A being Subset of Y st A = the carrier of Y0 holds A is proper iff Y0 is proper; theorem :: TEX_2:9 for Y0, Y1 being SubSpace of Y st the TopStruct of Y0 = the TopStruct of Y1 holds Y0 is proper implies Y1 is proper; theorem :: TEX_2:10 for Y0 being SubSpace of Y holds the carrier of Y0 = the carrier of Y implies Y0 is non proper; registration let Y be 1-element TopStruct; cluster -> non proper for non empty SubSpace of Y; cluster non proper -> trivial for non empty SubSpace of Y; end; registration let Y be non trivial TopStruct; cluster trivial -> proper for non empty SubSpace of Y; cluster non proper -> non trivial for non empty SubSpace of Y; end; registration let Y be non empty TopStruct; cluster non proper strict non empty for SubSpace of Y; end; theorem :: TEX_2:11 for Y being non empty TopStruct, Y0 being non proper SubSpace of Y holds the TopStruct of Y0 = the TopStruct of Y; registration let Y be non empty TopStruct; cluster discrete -> TopSpace-like for SubSpace of Y; cluster anti-discrete -> TopSpace-like for SubSpace of Y; cluster non TopSpace-like -> non discrete for SubSpace of Y; cluster non TopSpace-like -> non anti-discrete for SubSpace of Y; end; theorem :: TEX_2:12 for Y0, Y1 being TopStruct st the TopStruct of Y0 = the TopStruct of Y1 holds Y0 is discrete implies Y1 is discrete; theorem :: TEX_2:13 for Y0, Y1 being TopStruct st the TopStruct of Y0 = the TopStruct of Y1 holds Y0 is anti-discrete implies Y1 is anti-discrete; registration let Y be non empty TopStruct; cluster discrete -> almost_discrete for SubSpace of Y; cluster non almost_discrete -> non discrete for SubSpace of Y; cluster anti-discrete -> almost_discrete for SubSpace of Y; cluster non almost_discrete -> non anti-discrete for SubSpace of Y; end; theorem :: TEX_2:14 for Y0, Y1 being TopStruct st the TopStruct of Y0 = the TopStruct of Y1 holds Y0 is almost_discrete implies Y1 is almost_discrete; registration let Y be non empty TopStruct; cluster discrete anti-discrete -> trivial for non empty SubSpace of Y; cluster anti-discrete non trivial -> non discrete for non empty SubSpace of Y; cluster discrete non trivial -> non anti-discrete for non empty SubSpace of Y; end; definition let Y be non empty TopStruct, y be Point of Y; func Sspace(y) -> strict non empty SubSpace of Y means :: TEX_2:def 2 the carrier of it = {y}; end; registration let Y be non empty TopStruct; cluster strict 1-element for SubSpace of Y; end; registration let Y be non empty TopStruct, y be Point of Y; cluster Sspace(y) -> 1-element; end; theorem :: TEX_2:15 for Y being non empty TopStruct, y being Point of Y holds Sspace(y) is proper iff {y} is proper; theorem :: TEX_2:16 for Y being non empty TopStruct, y being Point of Y holds Sspace(y) is proper implies Y is non trivial; registration let Y be non trivial TopStruct; cluster proper trivial strict for non empty SubSpace of Y; end; registration let Y be non empty TopStruct; cluster 1-element for SubSpace of Y; end; theorem :: TEX_2:17 for Y being non empty TopStruct, Y0 be 1-element SubSpace of Y holds ex y being Point of Y st the TopStruct of Y0 = the TopStruct of Sspace(y) ; theorem :: TEX_2:18 for Y being non empty TopStruct, y being Point of Y holds Sspace(y) is TopSpace-like implies Sspace(y) is discrete anti-discrete; registration let Y be non empty TopStruct; cluster trivial TopSpace-like -> discrete anti-discrete for non empty SubSpace of Y; end; registration let X be non empty TopSpace; cluster trivial strict TopSpace-like non empty for SubSpace of X; end; registration let X be non empty TopSpace, x be Point of X; cluster Sspace(x) -> TopSpace-like; end; registration let X be non empty TopSpace; cluster discrete anti-discrete strict non empty for SubSpace of X; end; registration let X be non empty TopSpace, x be Point of X; cluster Sspace(x) -> discrete anti-discrete; end; registration let X be non empty TopSpace; cluster non proper -> open closed for SubSpace of X; cluster non open -> proper for SubSpace of X; cluster non closed -> proper for SubSpace of X; end; registration let X be non empty TopSpace; cluster open closed strict for SubSpace of X; end; registration let X be discrete non empty TopSpace; cluster anti-discrete -> trivial for non empty SubSpace of X; cluster non trivial -> non anti-discrete for non empty SubSpace of X; end; registration let X be discrete non trivial TopSpace; cluster discrete open closed proper strict for SubSpace of X; end; registration let X be anti-discrete non empty TopSpace; cluster discrete -> trivial for non empty SubSpace of X; cluster non trivial -> non discrete for non empty SubSpace of X; end; registration let X be anti-discrete non trivial TopSpace; cluster -> non open non closed for proper non empty SubSpace of X; cluster -> trivial proper for discrete non empty SubSpace of X; end; registration let X be anti-discrete non trivial TopSpace; cluster anti-discrete non open non closed proper strict for SubSpace of X; end; registration let X be almost_discrete non trivial TopSpace; cluster almost_discrete proper strict non empty for SubSpace of X; end; begin :: 3. Maximal Discrete Subsets and Subspaces. definition let Y be TopStruct, IT be Subset of Y; attr IT is discrete means :: TEX_2:def 3 for D being Subset of Y st D c= IT ex G being Subset of Y st G is open & IT /\ G = D; end; definition let Y be TopStruct; let A be Subset of Y; redefine attr A is discrete means :: TEX_2:def 4 for D being Subset of Y st D c= A ex F being Subset of Y st F is closed & A /\ F = D; end; theorem :: TEX_2:19 for Y0, Y1 being TopStruct, D0 being Subset of Y0, D1 being Subset of Y1 st the TopStruct of Y0 = the TopStruct of Y1 & D0 = D1 holds D0 is discrete implies D1 is discrete; theorem :: TEX_2:20 for Y being non empty TopStruct, Y0 being non empty SubSpace of Y, A being Subset of Y st A = the carrier of Y0 holds A is discrete iff Y0 is discrete; theorem :: TEX_2:21 for Y being non empty TopStruct, A being Subset of Y st A = the carrier of Y holds A is discrete iff Y is discrete; theorem :: TEX_2:22 for A, B being Subset of Y st B c= A holds A is discrete implies B is discrete; theorem :: TEX_2:23 for A, B being Subset of Y holds A is discrete or B is discrete implies A /\ B is discrete; theorem :: TEX_2:24 (for P, Q being Subset of Y st P is open & Q is open holds P /\ Q is open & P \/ Q is open) implies for A, B being Subset of Y st A is open & B is open holds A is discrete & B is discrete implies A \/ B is discrete; theorem :: TEX_2:25 (for P, Q being Subset of Y st P is closed & Q is closed holds P /\ Q is closed & P \/ Q is closed) implies for A, B being Subset of Y st A is closed & B is closed holds A is discrete & B is discrete implies A \/ B is discrete; theorem :: TEX_2:26 for A being Subset of Y holds A is discrete implies for x being Point of Y st x in A ex G being Subset of Y st G is open & A /\ G = {x}; theorem :: TEX_2:27 for A being Subset of Y holds A is discrete implies for x being Point of Y st x in A ex F being Subset of Y st F is closed & A /\ F = {x}; reserve X for non empty TopSpace; theorem :: TEX_2:28 for A0 being non empty Subset of X st A0 is discrete ex X0 being discrete strict non empty SubSpace of X st A0 = the carrier of X0; theorem :: TEX_2:29 for A being empty Subset of X holds A is discrete; theorem :: TEX_2:30 for x being Point of X holds {x} is discrete; theorem :: TEX_2:31 for A being Subset of X holds (for x being Point of X st x in A ex G being Subset of X st G is open & A /\ G = {x}) implies A is discrete; theorem :: TEX_2:32 for A, B being Subset of X st A is open & B is open holds A is discrete & B is discrete implies A \/ B is discrete; theorem :: TEX_2:33 for A, B being Subset of X st A is closed & B is closed holds A is discrete & B is discrete implies A \/ B is discrete; theorem :: TEX_2:34 for A being Subset of X st A is everywhere_dense holds A is discrete implies A is open; theorem :: TEX_2:35 for A being Subset of X holds A is discrete iff for D being Subset of X st D c= A holds A /\ Cl D = D; theorem :: TEX_2:36 for A being Subset of X holds A is discrete implies for x being Point of X st x in A holds A /\ Cl {x} = {x}; theorem :: TEX_2:37 for X being discrete non empty TopSpace, A being Subset of X holds A is discrete; theorem :: TEX_2:38 for X being anti-discrete non empty TopSpace, A being non empty Subset of X holds A is discrete iff A is trivial; definition let Y be TopStruct, IT be Subset of Y; attr IT is maximal_discrete means :: TEX_2:def 5 IT is discrete & for D being Subset of Y st D is discrete & IT c= D holds IT = D; end; theorem :: TEX_2:39 for Y0, Y1 being TopStruct, D0 being Subset of Y0, D1 being Subset of Y1 st the TopStruct of Y0 = the TopStruct of Y1 & D0 = D1 holds D0 is maximal_discrete implies D1 is maximal_discrete; theorem :: TEX_2:40 for A being empty Subset of X holds A is not maximal_discrete; theorem :: TEX_2:41 for A being Subset of X st A is open holds A is maximal_discrete implies A is dense; theorem :: TEX_2:42 for A being Subset of X st A is dense holds A is discrete implies A is maximal_discrete; theorem :: TEX_2:43 for X being discrete non empty TopSpace, A being Subset of X holds A is maximal_discrete iff A is non proper; theorem :: TEX_2:44 for X being anti-discrete non empty TopSpace, A being non empty Subset of X holds A is maximal_discrete iff A is trivial; definition let Y be non empty TopStruct; let IT be SubSpace of Y; attr IT is maximal_discrete means :: TEX_2:def 6 for A being Subset of Y st A = the carrier of IT holds A is maximal_discrete; end; theorem :: TEX_2:45 for Y being non empty TopStruct, Y0 being SubSpace of Y, A being Subset of Y st A = the carrier of Y0 holds A is maximal_discrete iff Y0 is maximal_discrete; registration let Y be non empty TopStruct; cluster maximal_discrete -> discrete for non empty SubSpace of Y; cluster non discrete -> non maximal_discrete for non empty SubSpace of Y; end; theorem :: TEX_2:46 for X0 being non empty SubSpace of X holds X0 is maximal_discrete iff X0 is discrete & for Y0 being discrete non empty SubSpace of X st X0 is SubSpace of Y0 holds the TopStruct of X0 = the TopStruct of Y0; theorem :: TEX_2:47 for A0 being non empty Subset of X st A0 is maximal_discrete ex X0 being strict non empty SubSpace of X st X0 is maximal_discrete & A0 = the carrier of X0; registration let X be discrete non empty TopSpace; cluster maximal_discrete -> non proper for SubSpace of X; cluster proper -> non maximal_discrete for SubSpace of X; cluster non proper -> maximal_discrete for SubSpace of X; cluster non maximal_discrete -> proper for SubSpace of X; end; registration let X be anti-discrete non empty TopSpace; cluster maximal_discrete -> trivial for non empty SubSpace of X; cluster non trivial -> non maximal_discrete for non empty SubSpace of X; cluster trivial -> maximal_discrete for non empty SubSpace of X; cluster non maximal_discrete -> non trivial for non empty SubSpace of X; end; begin :: 4. Maximal Discrete Subspaces of Almost Discrete Spaces. scheme :: TEX_2:sch 1 ExChoiceFCol{X()->non empty TopStruct,F()->Subset-Family of X(), P[object,object]}: ex f being Function of F(),the carrier of X() st for S being Subset of X() st S in F() holds P[S,f.S] provided for S being Subset of X() st S in F() ex x being Point of X() st P[S ,x]; reserve X for almost_discrete non empty TopSpace; theorem :: TEX_2:48 for A being Subset of X holds Cl A = union {Cl {a} where a is Point of X : a in A}; theorem :: TEX_2:49 for a, b being Point of X holds a in Cl {b} implies Cl {a} = Cl {b}; theorem :: TEX_2:50 for a, b being Point of X holds Cl {a} misses Cl {b} or Cl {a} = Cl {b}; theorem :: TEX_2:51 for A being Subset of X holds (for x being Point of X st x in A ex F being Subset of X st F is closed & A /\ F = {x}) implies A is discrete; theorem :: TEX_2:52 for A being Subset of X holds (for x being Point of X st x in A holds A /\ Cl {x} = {x}) implies A is discrete; theorem :: TEX_2:53 for A being Subset of X holds A is discrete iff for a, b being Point of X st a in A & b in A holds a <> b implies Cl {a} misses Cl {b}; theorem :: TEX_2:54 for A being Subset of X holds A is discrete iff for x being Point of X st x in Cl A ex a being Point of X st a in A & A /\ Cl {x} = {a}; theorem :: TEX_2:55 for A being Subset of X st A is open or A is closed holds A is maximal_discrete implies A is not proper; theorem :: TEX_2:56 for A being Subset of X holds A is maximal_discrete implies A is dense; theorem :: TEX_2:57 for A being Subset of X st A is maximal_discrete holds union {Cl {a} where a is Point of X : a in A} = the carrier of X; theorem :: TEX_2:58 for A being Subset of X holds A is maximal_discrete iff for x being Point of X ex a being Point of X st a in A & A /\ Cl {x} = {a}; theorem :: TEX_2:59 for A being Subset of X holds A is discrete implies ex M being Subset of X st A c= M & M is maximal_discrete; theorem :: TEX_2:60 ex M being Subset of X st M is maximal_discrete; theorem :: TEX_2:61 for Y0 being discrete non empty SubSpace of X ex X0 being strict non empty SubSpace of X st Y0 is SubSpace of X0 & X0 is maximal_discrete; registration let X be almost_discrete non discrete non empty TopSpace; cluster maximal_discrete -> proper for non empty SubSpace of X; cluster non proper -> non maximal_discrete for non empty SubSpace of X; end; registration let X be almost_discrete non anti-discrete non empty TopSpace; cluster maximal_discrete -> non trivial for non empty SubSpace of X; cluster trivial -> non maximal_discrete for non empty SubSpace of X; end; registration let X be almost_discrete non empty TopSpace; cluster maximal_discrete strict non empty non empty for SubSpace of X; end; begin :: 5. Continuous Mappings and Almost Discrete Spaces. reserve X,Y for non empty TopSpace; theorem :: TEX_2:62 for X being discrete TopSpace, Y being TopSpace, f being Function of X,Y holds f is continuous; theorem :: TEX_2:63 (for Y being non empty TopSpace, f being Function of X,Y holds f is continuous) implies X is discrete; theorem :: TEX_2:64 for Y being anti-discrete non empty TopSpace, f being Function of X,Y holds f is continuous; theorem :: TEX_2:65 (for X being non empty TopSpace, f being Function of X,Y holds f is continuous ) implies Y is anti-discrete; reserve X for discrete non empty TopSpace, X0 for non empty SubSpace of X; theorem :: TEX_2:66 ex r being continuous Function of X,X0 st r is being_a_retraction; theorem :: TEX_2:67 X0 is_a_retract_of X; reserve X for almost_discrete non empty TopSpace, X0 for maximal_discrete non empty SubSpace of X; theorem :: TEX_2:68 ex r being continuous Function of X,X0 st r is being_a_retraction; theorem :: TEX_2:69 X0 is_a_retract_of X; theorem :: TEX_2:70 for r being continuous Function of X,X0 holds r is being_a_retraction implies for F being Subset of X0, E being Subset of X st F = E holds r" F = Cl E; theorem :: TEX_2:71 for r being continuous Function of X,X0 holds r is being_a_retraction implies for a being Point of X0, b being Point of X st a = b holds r" {a} = Cl {b}; reserve X0 for discrete non empty SubSpace of X; theorem :: TEX_2:72 ex r being continuous Function of X,X0 st r is being_a_retraction; theorem :: TEX_2:73 X0 is_a_retract_of X;