:: On Nowhere and Everywhere Dense Subspaces of Topological Spaces
:: by Zbigniew Karno
::
:: Received November 9, 1993
:: Copyright (c) 1993-2018 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;