Volume 5, 1993

University of Bialystok

Copyright (c) 1993 Association of Mizar Users

### The abstract of the Mizar article:

### Maximal Discrete Subspaces of Almost Discrete Topological Spaces

**by****Zbigniew Karno**- Received November 5, 1993
- MML identifier: TEX_2

- [ Mizar article, MML identifier index ]

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

Back to top