:: On Nowhere and Everywhere Dense Subspaces of Topological Spaces :: by Zbigniew Karno :: :: Received November 9, 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, TSEP_2, STRUCT_0, TOPS_3, TOPS_1, ZFMISC_1, RCOMP_1, TARSKI, SETFAM_1, NATTRA_1, TDLAT_3; notations TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1, TSEP_1, TSEP_2, TDLAT_3, TOPS_3, TEX_2; constructors TOPS_1, BORSUK_1, TSEP_1, TDLAT_3, TOPS_3, TEX_2, TSEP_2; registrations XBOOLE_0, STRUCT_0, PRE_TOPC, BORSUK_1, TDLAT_3, TEX_1, TEX_2, TOPS_1; requirements BOOLE, SUBSET; begin :: 1. Some Properties of Subsets of a Topological Space. reserve X for non empty TopSpace, A,B for Subset of X; theorem :: TEX_3:1 A,B constitute_a_decomposition implies (A is non empty iff B is proper); theorem :: TEX_3:2 A,B constitute_a_decomposition implies (A is dense iff B is boundary); theorem :: TEX_3:3 A,B constitute_a_decomposition implies (A is boundary iff B is dense); theorem :: TEX_3:4 A,B constitute_a_decomposition implies (A is everywhere_dense iff B is nowhere_dense); theorem :: TEX_3:5 A,B constitute_a_decomposition implies (A is nowhere_dense iff B is everywhere_dense); reserve Y1,Y2 for non empty SubSpace of X; theorem :: TEX_3:6 Y1,Y2 constitute_a_decomposition implies Y1 is proper & Y2 is proper; theorem :: TEX_3:7 for X being non trivial TopSpace, D being non empty proper Subset of X ex Y0 being proper strict non empty SubSpace of X st D = the carrier of Y0; theorem :: TEX_3:8 for X being non trivial TopSpace, Y1 being proper non empty SubSpace of X ex Y2 being proper strict non empty SubSpace of X st Y1,Y2 constitute_a_decomposition; begin :: 2. Dense and Everywhere Dense Subspaces. definition let X be non empty TopSpace; let IT be SubSpace of X; attr IT is dense means :: TEX_3:def 1 for A being Subset of X st A = the carrier of IT holds A is dense; end; theorem :: TEX_3:9 for X0 being SubSpace of X, A being Subset of X st A = the carrier of X0 holds X0 is dense iff A is dense; registration let X be non empty TopSpace; cluster dense closed -> non proper for SubSpace of X; cluster dense proper -> non closed for SubSpace of X; cluster proper closed -> non dense for SubSpace of X; end; registration let X be non empty TopSpace; cluster dense strict non empty for SubSpace of X; end; ::Properties of Dense Subspaces. theorem :: TEX_3:10 for A0 being non empty Subset of X st A0 is dense ex X0 being dense strict non empty SubSpace of X st A0 = the carrier of X0; theorem :: TEX_3:11 for X0 being dense non empty SubSpace of X, A being Subset of X, B being Subset of X0 st A = B holds B is dense iff A is dense; theorem :: TEX_3:12 for X1 being dense SubSpace of X, X2 being SubSpace of X holds X1 is SubSpace of X2 implies X2 is dense; theorem :: TEX_3:13 for X1 being dense non empty SubSpace of X, X2 being non empty SubSpace of X holds X1 is SubSpace of X2 implies X1 is dense SubSpace of X2; theorem :: TEX_3:14 for X1 being dense non empty SubSpace of X, X2 being dense non empty SubSpace of X1 holds X2 is dense non empty SubSpace of X; theorem :: TEX_3:15 for Y1, Y2 being non empty TopSpace st Y2 = the TopStruct of Y1 holds Y1 is dense SubSpace of X iff Y2 is dense SubSpace of X; definition let X be non empty TopSpace; let IT be SubSpace of X; attr IT is everywhere_dense means :: TEX_3:def 2 for A being Subset of X st A = the carrier of IT holds A is everywhere_dense; end; theorem :: TEX_3:16 for X0 being SubSpace of X, A being Subset of X st A = the carrier of X0 holds X0 is everywhere_dense iff A is everywhere_dense; registration let X be non empty TopSpace; cluster everywhere_dense -> dense for SubSpace of X; cluster non dense -> non everywhere_dense for SubSpace of X; cluster non proper -> everywhere_dense for SubSpace of X; cluster non everywhere_dense -> proper for SubSpace of X; end; registration let X be non empty TopSpace; cluster everywhere_dense strict non empty for SubSpace of X; end; ::Properties of Everywhere Dense Subspaces. theorem :: TEX_3:17 for A0 being non empty Subset of X st A0 is everywhere_dense ex X0 being everywhere_dense strict non empty SubSpace of X st A0 = the carrier of X0; theorem :: TEX_3:18 for X0 being everywhere_dense non empty SubSpace of X, A being Subset of X, B being Subset of X0 st A = B holds B is everywhere_dense iff A is everywhere_dense; theorem :: TEX_3:19 for X1 being everywhere_dense SubSpace of X, X2 being SubSpace of X holds X1 is SubSpace of X2 implies X2 is everywhere_dense; theorem :: TEX_3:20 for X1 being everywhere_dense non empty SubSpace of X, X2 being non empty SubSpace of X holds X1 is SubSpace of X2 implies X1 is everywhere_dense SubSpace of X2; theorem :: TEX_3:21 for X1 being everywhere_dense non empty SubSpace of X, X2 being everywhere_dense non empty SubSpace of X1 holds X2 is everywhere_dense SubSpace of X; theorem :: TEX_3:22 for Y1, Y2 being non empty TopSpace st Y2 = the TopStruct of Y1 holds Y1 is everywhere_dense SubSpace of X iff Y2 is everywhere_dense SubSpace of X ; registration let X be non empty TopSpace; cluster dense open -> everywhere_dense for SubSpace of X; cluster dense non everywhere_dense -> non open for SubSpace of X; cluster open non everywhere_dense -> non dense for SubSpace of X; end; registration let X be non empty TopSpace; cluster dense open strict non empty for SubSpace of X; end; ::Properties of Dense Open Subspaces. theorem :: TEX_3:23 for A0 being non empty Subset of X st A0 is dense open ex X0 being dense open strict non empty SubSpace of X st A0 = the carrier of X0; theorem :: TEX_3:24 for X0 being SubSpace of X holds X0 is everywhere_dense iff ex X1 being dense open strict SubSpace of X st X1 is SubSpace of X0; reserve X1, X2 for non empty SubSpace of X; theorem :: TEX_3:25 X1 is dense or X2 is dense implies X1 union X2 is dense SubSpace of X; theorem :: TEX_3:26 X1 is everywhere_dense or X2 is everywhere_dense implies X1 union X2 is everywhere_dense SubSpace of X; theorem :: TEX_3:27 X1 is everywhere_dense & X2 is everywhere_dense implies X1 meet X2 is everywhere_dense SubSpace of X; theorem :: TEX_3:28 X1 is everywhere_dense & X2 is dense or X1 is dense & X2 is everywhere_dense implies X1 meet X2 is dense SubSpace of X; begin :: 3. Boundary and Nowhere Dense Subspaces. definition let X be non empty TopSpace; let IT be SubSpace of X; attr IT is boundary means :: TEX_3:def 3 for A being Subset of X st A = the carrier of IT holds A is boundary; end; theorem :: TEX_3:29 for X0 being SubSpace of X, A being Subset of X st A = the carrier of X0 holds X0 is boundary iff A is boundary; registration let X be non empty TopSpace; cluster open -> non boundary for non empty SubSpace of X; cluster boundary -> non open for non empty SubSpace of X; cluster everywhere_dense -> non boundary for SubSpace of X; cluster boundary -> non everywhere_dense for SubSpace of X; end; ::Properties of Boundary Subspaces. theorem :: TEX_3:30 for A0 being non empty Subset of X st A0 is boundary ex X0 being strict SubSpace of X st X0 is boundary & A0 = the carrier of X0; theorem :: TEX_3:31 for X1,X2 being SubSpace of X st X1,X2 constitute_a_decomposition holds X1 is dense iff X2 is boundary; theorem :: TEX_3:32 for X1,X2 being non empty SubSpace of X st X1,X2 constitute_a_decomposition holds X1 is boundary iff X2 is dense; theorem :: TEX_3:33 for X0 being SubSpace of X st X0 is boundary for A being Subset of X st A c= the carrier of X0 holds A is boundary; theorem :: TEX_3:34 for X1,X2 being SubSpace of X st X1 is boundary holds X2 is SubSpace of X1 implies X2 is boundary; definition let X be non empty TopSpace; let IT be SubSpace of X; attr IT is nowhere_dense means :: TEX_3:def 4 for A being Subset of X st A = the carrier of IT holds A is nowhere_dense; end; theorem :: TEX_3:35 for X0 being SubSpace of X, A being Subset of X st A = the carrier of X0 holds X0 is nowhere_dense iff A is nowhere_dense; registration let X be non empty TopSpace; cluster nowhere_dense -> boundary for SubSpace of X; cluster non boundary -> non nowhere_dense for SubSpace of X; cluster nowhere_dense -> non dense for SubSpace of X; cluster dense -> non nowhere_dense for SubSpace of X; end; reserve X for non empty TopSpace; ::Properties of Nowhere Dense Subspaces. theorem :: TEX_3:36 for A0 being non empty Subset of X st A0 is nowhere_dense ex X0 being strict SubSpace of X st X0 is nowhere_dense & A0 = the carrier of X0; theorem :: TEX_3:37 for X1,X2 being SubSpace of X st X1,X2 constitute_a_decomposition holds X1 is everywhere_dense iff X2 is nowhere_dense ; theorem :: TEX_3:38 for X1,X2 being non empty SubSpace of X st X1,X2 constitute_a_decomposition holds X1 is nowhere_dense iff X2 is everywhere_dense ; theorem :: TEX_3:39 for X0 being SubSpace of X st X0 is nowhere_dense for A being Subset of X st A c= the carrier of X0 holds A is nowhere_dense; theorem :: TEX_3:40 for X1,X2 being SubSpace of X st X1 is nowhere_dense holds X2 is SubSpace of X1 implies X2 is nowhere_dense; registration let X be non empty TopSpace; cluster boundary closed -> nowhere_dense for SubSpace of X; cluster boundary non nowhere_dense -> non closed for SubSpace of X; cluster closed non nowhere_dense -> non boundary for SubSpace of X; end; ::Properties of Boundary Closed Subspaces. theorem :: TEX_3:41 for A0 being non empty Subset of X st A0 is boundary closed ex X0 being closed strict non empty SubSpace of X st X0 is boundary & A0 = the carrier of X0; theorem :: TEX_3:42 for X0 being non empty SubSpace of X holds X0 is nowhere_dense iff ex X1 being closed strict non empty SubSpace of X st X1 is boundary & X0 is SubSpace of X1; reserve X1, X2 for non empty SubSpace of X; theorem :: TEX_3:43 (X1 is boundary or X2 is boundary) & X1 meets X2 implies X1 meet X2 is boundary; theorem :: TEX_3:44 X1 is nowhere_dense & X2 is nowhere_dense implies X1 union X2 is nowhere_dense; theorem :: TEX_3:45 X1 is nowhere_dense & X2 is boundary or X1 is boundary & X2 is nowhere_dense implies X1 union X2 is boundary; theorem :: TEX_3:46 (X1 is nowhere_dense or X2 is nowhere_dense) & X1 meets X2 implies X1 meet X2 is nowhere_dense; begin :: 4. Dense and Boundary Subspaces of non Discrete Spaces. theorem :: TEX_3:47 for X being non empty TopSpace holds (for X0 being SubSpace of X holds X0 is non boundary) implies X is discrete; theorem :: TEX_3:48 for X being non trivial TopSpace holds (for X0 being proper SubSpace of X holds X0 is non dense) implies X is discrete; registration let X be discrete non empty TopSpace; cluster -> non boundary for non empty SubSpace of X; cluster proper -> non dense for SubSpace of X; cluster dense -> non proper for SubSpace of X; end; registration let X be discrete non empty TopSpace; cluster non boundary strict non empty for SubSpace of X; end; registration let X be discrete non trivial TopSpace; cluster non dense strict for SubSpace of X; end; theorem :: TEX_3:49 for X being non empty TopSpace holds (ex X0 being non empty SubSpace of X st X0 is boundary) implies X is non discrete; theorem :: TEX_3:50 for X being non empty TopSpace holds (ex X0 being non empty SubSpace of X st X0 is dense proper) implies X is non discrete; registration let X be non discrete non empty TopSpace; cluster boundary strict non empty for SubSpace of X; cluster dense proper strict non empty for SubSpace of X; end; reserve X for non discrete non empty TopSpace; theorem :: TEX_3:51 for A0 being non empty Subset of X st A0 is boundary ex X0 being boundary strict SubSpace of X st A0 = the carrier of X0; theorem :: TEX_3:52 for A0 being non empty proper Subset of X st A0 is dense ex X0 being dense proper strict SubSpace of X st A0 = the carrier of X0; theorem :: TEX_3:53 for X1 being boundary non empty SubSpace of X ex X2 being dense proper strict non empty SubSpace of X st X1,X2 constitute_a_decomposition; theorem :: TEX_3:54 for X1 being dense proper non empty SubSpace of X ex X2 being boundary strict non empty SubSpace of X st X1,X2 constitute_a_decomposition; theorem :: TEX_3:55 for Y1, Y2 being non empty TopSpace st Y2 = the TopStruct of Y1 holds Y1 is boundary SubSpace of X iff Y2 is boundary SubSpace of X; begin :: 5. Everywhere and Nowhere Dense Subspaces of non Almost Discrete Spaces. theorem :: TEX_3:56 for X being non empty TopSpace holds (for X0 being SubSpace of X holds X0 is non nowhere_dense) implies X is almost_discrete; theorem :: TEX_3:57 for X being non trivial TopSpace holds (for X0 being proper SubSpace of X holds X0 is non everywhere_dense) implies X is almost_discrete; registration let X be almost_discrete non empty TopSpace; cluster -> non nowhere_dense for non empty SubSpace of X; cluster proper -> non everywhere_dense for SubSpace of X; cluster everywhere_dense -> non proper for SubSpace of X; cluster boundary -> non closed for non empty SubSpace of X; cluster closed -> non boundary for non empty SubSpace of X; cluster dense proper -> non open for SubSpace of X; cluster dense open -> non proper for SubSpace of X; cluster open proper -> non dense for SubSpace of X; end; registration let X be almost_discrete non empty TopSpace; cluster non nowhere_dense strict non empty for SubSpace of X; end; registration let X be almost_discrete non trivial TopSpace; cluster non everywhere_dense strict for SubSpace of X; end; theorem :: TEX_3:58 for X being non empty TopSpace holds (ex X0 being non empty SubSpace of X st X0 is nowhere_dense) implies X is non almost_discrete; theorem :: TEX_3:59 for X being non empty TopSpace holds (ex X0 being non empty SubSpace of X st X0 is boundary closed) implies X is non almost_discrete; theorem :: TEX_3:60 for X being non empty TopSpace holds (ex X0 being non empty SubSpace of X st X0 is everywhere_dense proper) implies X is non almost_discrete; theorem :: TEX_3:61 for X being non empty TopSpace holds (ex X0 being non empty SubSpace of X st X0 is dense open proper) implies X is non almost_discrete; registration let X be non almost_discrete non empty TopSpace; cluster nowhere_dense strict non empty for SubSpace of X; cluster everywhere_dense proper strict non empty for SubSpace of X; end; reserve X for non almost_discrete non empty TopSpace; theorem :: TEX_3:62 for A0 being non empty Subset of X st A0 is nowhere_dense ex X0 being nowhere_dense strict non empty SubSpace of X st A0 = the carrier of X0; theorem :: TEX_3:63 for A0 being non empty proper Subset of X st A0 is everywhere_dense ex X0 being everywhere_dense proper strict SubSpace of X st A0 = the carrier of X0 ; theorem :: TEX_3:64 for X1 being nowhere_dense non empty SubSpace of X ex X2 being everywhere_dense proper strict non empty SubSpace of X st X1,X2 constitute_a_decomposition; theorem :: TEX_3:65 for X1 being everywhere_dense proper non empty SubSpace of X ex X2 being nowhere_dense strict non empty SubSpace of X st X1,X2 constitute_a_decomposition; theorem :: TEX_3:66 for Y1, Y2 being non empty TopSpace st Y2 = the TopStruct of Y1 holds Y1 is nowhere_dense SubSpace of X iff Y2 is nowhere_dense SubSpace of X; registration let X be non almost_discrete non empty TopSpace; cluster boundary closed strict non empty for SubSpace of X; cluster dense open proper strict non empty for SubSpace of X; end; theorem :: TEX_3:67 for A0 being non empty Subset of X st A0 is boundary closed ex X0 being boundary closed strict non empty SubSpace of X st A0 = the carrier of X0; theorem :: TEX_3:68 for A0 being non empty proper Subset of X st A0 is dense open ex X0 being dense open proper strict SubSpace of X st A0 = the carrier of X0; theorem :: TEX_3:69 for X1 being boundary closed non empty SubSpace of X ex X2 being dense open proper strict non empty SubSpace of X st X1,X2 constitute_a_decomposition; theorem :: TEX_3:70 for X1 being dense open proper non empty SubSpace of X ex X2 being boundary closed strict non empty SubSpace of X st X1,X2 constitute_a_decomposition; theorem :: TEX_3:71 for X0 being non empty SubSpace of X holds X0 is nowhere_dense iff ex X1 being boundary closed strict non empty SubSpace of X st X0 is SubSpace of X1 ; theorem :: TEX_3:72 for X0 being nowhere_dense non empty SubSpace of X holds X0 is boundary closed or ex X1 being everywhere_dense proper strict non empty SubSpace of X, X2 being boundary closed strict non empty SubSpace of X st X1 meet X2 = the TopStruct of X0 & X1 union X2 = the TopStruct of X; theorem :: TEX_3:73 for X0 being everywhere_dense non empty SubSpace of X holds X0 is dense open or ex X1 being dense open proper strict non empty SubSpace of X, X2 being nowhere_dense strict non empty SubSpace of X st X1 misses X2 & X1 union X2 = the TopStruct of X0; theorem :: TEX_3:74 for X0 being nowhere_dense non empty SubSpace of X ex X1 being dense open proper strict non empty SubSpace of X, X2 being boundary closed strict non empty SubSpace of X st X1,X2 constitute_a_decomposition & X0 is SubSpace of X2; theorem :: TEX_3:75 for X0 being everywhere_dense proper SubSpace of X ex X1 being dense open proper strict SubSpace of X, X2 being boundary closed strict SubSpace of X st X1,X2 constitute_a_decomposition & X1 is SubSpace of X0;