Journal of Formalized Mathematics
Volume 5, 1993
University of Bialystok
Copyright (c) 1993 Association of Mizar Users

On Nowhere and Everywhere Dense Subspaces of Topological Spaces

by
Zbigniew Karno

MML identifier: TEX_3
[ Mizar article, MML identifier index ]

```environ

vocabulary PRE_TOPC, TSEP_2, COLLSP, TOPS_3, BOOLE, TOPS_1, REALSET1,
SUBSET_1, TARSKI, SETFAM_1, NATTRA_1, TDLAT_3;
notation TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1,
TSEP_1, TSEP_2, TDLAT_3, TOPS_3, TEX_1, TEX_2;
constructors REALSET1, TOPS_1, BORSUK_1, TSEP_1, TSEP_2, TDLAT_3, TOPS_3,
TEX_2, MEMBERED;
clusters PRE_TOPC, BORSUK_1, TDLAT_3, TEX_1, TEX_2, STRUCT_0, MEMBERED,
ZFMISC_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 (non empty 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 (non empty 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;

definition let X be non empty TopSpace;
cluster dense closed -> non proper SubSpace of X;
cluster dense proper -> non closed SubSpace of X;
cluster proper closed -> non dense SubSpace of X;
end;

definition let X be non empty TopSpace;
cluster dense strict non empty 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;

definition let X be non empty TopSpace;
cluster everywhere_dense -> dense SubSpace of X;
cluster non dense -> non everywhere_dense SubSpace of X;
cluster non proper -> everywhere_dense SubSpace of X;
cluster non everywhere_dense -> proper SubSpace of X;
end;

definition let X be non empty TopSpace;
cluster everywhere_dense strict non empty 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;

definition let X be non empty TopSpace;
cluster dense open -> everywhere_dense SubSpace of X;
cluster dense non everywhere_dense -> non open SubSpace of X;
cluster open non everywhere_dense -> non dense SubSpace of X;
end;

definition let X be non empty TopSpace;
cluster dense open strict non empty 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;

definition let X be non empty TopSpace;
cluster open -> non boundary (non empty SubSpace of X);
cluster boundary -> non open (non empty SubSpace of X);
cluster everywhere_dense -> non boundary SubSpace of X;
cluster boundary -> non everywhere_dense 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;

definition let X be non empty TopSpace;
cluster nowhere_dense -> boundary SubSpace of X;
cluster non boundary -> non nowhere_dense SubSpace of X;
cluster nowhere_dense -> non dense SubSpace of X;
cluster dense -> non nowhere_dense 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;

definition let X be non empty TopSpace;
cluster boundary closed -> nowhere_dense SubSpace of X;
cluster boundary non nowhere_dense -> non closed SubSpace of X;
cluster closed non nowhere_dense -> non boundary 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 (non empty TopSpace) holds
(for X0 being proper SubSpace of X holds X0 is non dense) implies
X is discrete;

definition let X be discrete non empty TopSpace;
cluster -> non boundary (non empty SubSpace of X);
cluster proper -> non dense SubSpace of X;
cluster dense -> non proper SubSpace of X;
end;

definition let X be discrete non empty TopSpace;
cluster non boundary strict non empty SubSpace of X;
end;

definition let X be discrete non trivial (non empty TopSpace);
cluster non dense strict 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;

definition let X be non discrete non empty TopSpace;
cluster boundary strict non empty SubSpace of X;
cluster dense proper strict non empty 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 (non empty TopSpace) holds
(for X0 being proper SubSpace of X holds X0 is non everywhere_dense) implies
X is almost_discrete;

definition let X be almost_discrete non empty TopSpace;
cluster -> non nowhere_dense (non empty SubSpace of X);
cluster proper -> non everywhere_dense SubSpace of X;
cluster everywhere_dense -> non proper SubSpace of X;
cluster boundary -> non closed (non empty SubSpace of X);
cluster closed -> non boundary (non empty SubSpace of X);
cluster dense proper -> non open SubSpace of X;
cluster dense open -> non proper SubSpace of X;
cluster open proper -> non dense SubSpace of X;
end;

definition let X be almost_discrete non empty TopSpace;
cluster non nowhere_dense strict non empty SubSpace of X;
end;

definition let X be almost_discrete non trivial (non empty TopSpace);
cluster non everywhere_dense strict 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;

definition let X be non almost_discrete non empty TopSpace;
cluster nowhere_dense strict non empty SubSpace of X;
cluster everywhere_dense proper strict non empty 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;

definition let X be non almost_discrete non empty TopSpace;
cluster boundary closed strict non empty SubSpace of X;
cluster dense open proper strict non empty 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;

```