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

### On Discrete and Almost Discrete Topological Spaces

by
Zbigniew Karno

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

```environ

vocabulary PRE_TOPC, TMAP_1, SUBSET_1, BOOLE, TOPS_1, TOPS_3, REALSET1,
SETFAM_1, TDLAT_3, NATTRA_1, TARSKI, TEX_1, PCOMPS_1;
notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, SETFAM_1, STRUCT_0, REALSET1,
PRE_TOPC, TOPS_1, TMAP_1, TDLAT_3, TOPS_3, PCOMPS_1;
constructors REALSET1, TOPS_1, TMAP_1, TDLAT_3, TOPS_3, DOMAIN_1, PCOMPS_1,
MEMBERED;
clusters TDLAT_3, STRUCT_0, COMPLSP1, TMAP_1, SUBSET_1, TOPS_1, PCOMPS_1,
XBOOLE_0, ZFMISC_1;
requirements BOOLE, SUBSET;

begin
:: 1. Properties of Subsets of a Topological Space with Modified Topology.
reserve X for non empty TopSpace, D for Subset of X;

theorem :: TEX_1:1
for B being Subset of X,
C being Subset of X modified_with_respect_to D st
B = C holds B is open implies C is open;

theorem :: TEX_1:2
for B being Subset of X,
C being Subset of X modified_with_respect_to D st
B = C holds B is closed implies C is closed;

theorem :: TEX_1:3
for C being Subset of X modified_with_respect_to  D` st C = D holds
C is closed;

theorem :: TEX_1:4
for C being Subset of X modified_with_respect_to D
st C = D holds
D is dense implies C is dense & C is open;

theorem :: TEX_1:5
for C being Subset of X modified_with_respect_to D
st D c= C holds
D is dense implies C is everywhere_dense;

theorem :: TEX_1:6
for C being Subset of X modified_with_respect_to  D`
st C = D holds
D is boundary implies C is boundary & C is closed;

theorem :: TEX_1:7
for C being Subset of X modified_with_respect_to  D`
st C c= D holds
D is boundary implies C is nowhere_dense;

begin
:: 2. Trivial Topological Spaces.

definition let Y be non empty 1-sorted;
redefine attr Y is trivial means
:: TEX_1:def 1
ex d being Element of Y st the carrier of Y = {d};
end;

definition let A be non empty set;
cluster 1-sorted(#A#) -> non empty;
end;

definition
cluster trivial strict non empty 1-sorted;
cluster non trivial strict non empty 1-sorted;
end;

definition
cluster trivial strict non empty TopStruct;
cluster non trivial strict non empty TopStruct;
end;

theorem :: TEX_1:8
for Y being trivial non empty TopStruct st the topology of Y is non empty
holds Y is almost_discrete implies Y is TopSpace-like;

definition
cluster trivial strict non empty TopSpace;
end;

definition
cluster trivial -> anti-discrete discrete (non empty TopSpace);
cluster discrete anti-discrete -> trivial (non empty TopSpace);
end;

definition
cluster non trivial strict non empty TopSpace;
end;

definition
cluster non discrete -> non trivial (non empty TopSpace);
cluster non anti-discrete -> non trivial (non empty TopSpace);
end;

begin
:: 3. Examples of Discrete and Anti-discrete Topological Spaces.

definition let D be set;
func cobool D -> Subset-Family of D equals
:: TEX_1:def 2
{{},D};
end;

definition let D be set;
cluster cobool D -> non empty;
end;

definition let D be set;
:: TEX_1:def 3
TopStruct(#D,cobool D#);
end;

definition let D be set;
cluster ADTS(D) -> strict anti-discrete TopSpace-like;
end;

definition let D be non empty set;
end;

theorem :: TEX_1:9
for X being anti-discrete non empty TopSpace holds
the TopStruct of X = ADTS(the carrier of X);

theorem :: TEX_1:10
for X being non empty TopSpace st
the TopStruct of X = the TopStruct of ADTS(the carrier of X) holds
X is anti-discrete;

theorem :: TEX_1:11
for X being anti-discrete non empty TopSpace
for A being Subset of X holds (A is empty implies Cl A = {}) &
(A is non empty implies Cl A = the carrier of X);

theorem :: TEX_1:12
for X being anti-discrete non empty TopSpace
for A being Subset of X holds (A <> the carrier of X
implies Int A = {}) &
(A = the carrier of X implies Int A = the carrier of X);

theorem :: TEX_1:13
for X being non empty TopSpace holds
(for A being Subset of X holds
(A is non empty implies Cl A = the carrier of X))
implies X is anti-discrete;

theorem :: TEX_1:14
for X being non empty TopSpace holds
(for A being Subset of X
holds (A <> the carrier of X implies Int A = {}))
implies X is anti-discrete;

theorem :: TEX_1:15
for X being anti-discrete non empty TopSpace
for A being Subset of X holds (A <> {} implies A is dense) &
(A <> the carrier of X implies A is boundary);

theorem :: TEX_1:16
for X being non empty TopSpace holds
(for A being Subset of X holds (A <> {} implies A is dense))
implies X is anti-discrete;

theorem :: TEX_1:17
for X being non empty TopSpace holds
(for A being Subset of X
holds (A <> the carrier of X implies A is boundary))
implies X is anti-discrete;

definition let D be set;
cluster 1TopSp D -> discrete;
end;

theorem :: TEX_1:18
for X being discrete non empty TopSpace holds
the TopStruct of X = 1TopSp (the carrier of X);

theorem :: TEX_1:19
for X being non empty TopSpace st
the TopStruct of X = the TopStruct of 1TopSp(the carrier of X) holds
X is discrete;

theorem :: TEX_1:20
for X being discrete non empty TopSpace
for A being Subset of X holds Cl A = A & Int A = A;

theorem :: TEX_1:21
for X being non empty TopSpace holds
(for A being Subset of X holds Cl A = A) implies X is discrete;

theorem :: TEX_1:22
for X being non empty TopSpace holds
(for A being Subset of X
holds Int A = A) implies X is discrete;

theorem :: TEX_1:23
for D being non empty set holds
ADTS(D) = 1TopSp(D) iff ex d0 being Element of D st D = {d0};

definition
cluster discrete non anti-discrete strict non empty TopSpace;
cluster anti-discrete non discrete strict non empty TopSpace;
end;

begin
:: 4. An Example of a Topological Space.

definition let D be set, F be Subset-Family of D, S be set;
redefine func F \ S -> Subset-Family of D;
end;

definition let D be set, d0 be Element of D;
canceled;

func STS(D,d0) -> TopStruct equals
:: TEX_1:def 5
TopStruct (#D,(bool D) \ {A where A is Subset of D : d0 in A & A <> D}#);
end;

definition let D be set, d0 be Element of D;
cluster STS(D,d0) -> strict TopSpace-like;
end;

definition let D be non empty set, d0 be Element of D;
cluster STS(D,d0) -> non empty;
end;

reserve D for non empty set, d0 for Element of D;

theorem :: TEX_1:24
for A being Subset of STS(D,d0) holds
({d0} c= A implies A is closed) &
(A is non empty & A is closed implies {d0} c= A);

theorem :: TEX_1:25
D \ {d0} is non empty implies
for A being Subset of STS(D,d0) holds
(A = {d0} implies A is closed & A is boundary) &
(A is non empty & A is closed & A is boundary implies A = {d0});

theorem :: TEX_1:26
for A being Subset of STS(D,d0) holds
(A c= D \ {d0} implies A is open) &
(A <> D & A is open implies A c= D \ {d0});

theorem :: TEX_1:27
D \ {d0} is non empty implies
for A being Subset of STS(D,d0) holds
(A = D \ {d0} implies A is open & A is dense) &
(A <> D & A is open & A is dense implies A = D \ {d0});

definition
cluster non anti-discrete non discrete strict non empty TopSpace;
end;

theorem :: TEX_1:28
for Y being non empty TopSpace holds
the TopStruct of Y = the TopStruct of STS(D,d0) iff
the carrier of Y = D &
for A being Subset of Y
holds ({d0} c= A implies A is closed) &
(A is non empty & A is closed implies {d0} c= A);

theorem :: TEX_1:29
for Y being non empty TopSpace holds
the TopStruct of Y = the TopStruct of STS(D,d0) iff
the carrier of Y = D &
for A being Subset of Y
holds (A c= D \ {d0} implies A is open) &
(A <> D & A is open implies A c= D \ {d0});

theorem :: TEX_1:30
for Y being non empty TopSpace holds
the TopStruct of Y = the TopStruct of STS(D,d0) iff
the carrier of Y = D &
for A being non empty Subset of Y holds Cl A = A \/ {d0};

theorem :: TEX_1:31
for Y being non empty TopSpace holds
the TopStruct of Y = the TopStruct of STS(D,d0) iff
the carrier of Y = D &
for A being Subset of Y st A <> D holds Int A = A \ {d0};

theorem :: TEX_1:32
STS(D,d0) = ADTS(D) iff D = {d0};

theorem :: TEX_1:33
STS(D,d0) = 1TopSp(D) iff D = {d0};

theorem :: TEX_1:34
for D being non empty set, d0 being Element of D
for A being Subset of STS(D,d0) st A = {d0} holds
1TopSp(D) = STS(D,d0) modified_with_respect_to A;

begin
:: 5. Discrete and Almost Discrete Spaces.

definition let X be non empty TopSpace;
redefine attr X is discrete means
:: TEX_1:def 6
for A being non empty Subset of X holds A is not boundary;
end;

theorem :: TEX_1:35
X is discrete iff
for A being Subset of X
holds A <> the carrier of X implies A is not dense;

definition
cluster non almost_discrete ->
non discrete non anti-discrete (non empty TopSpace);
end;

definition let X be non empty TopSpace;
redefine attr X is almost_discrete means
:: TEX_1:def 7
for A being non empty Subset of X holds A is not nowhere_dense;
end;

theorem :: TEX_1:36
X is almost_discrete iff
for A being Subset of X holds
A <> the carrier of X implies A is not everywhere_dense;

theorem :: TEX_1:37
X is non almost_discrete iff
ex A being non empty Subset of X st A is boundary & A is closed;

theorem :: TEX_1:38
X is non almost_discrete iff
ex A being Subset of X st A <> the carrier of X & A is dense & A is open;

definition
cluster
almost_discrete non discrete non anti-discrete strict non empty TopSpace;
end;

theorem :: TEX_1:39
for C being non empty set, c0 being Element of C holds
C \ {c0} is non empty iff STS(C,c0) is non almost_discrete;

definition
cluster non almost_discrete strict non empty TopSpace;
end;

theorem :: TEX_1:40
for A being non empty Subset of X st A is boundary holds
X modified_with_respect_to  A` is non almost_discrete;

theorem :: TEX_1:41
for A being Subset of X st A <> the carrier of X & A is dense holds
X modified_with_respect_to A is non almost_discrete;

```