:: On Discrete and Almost Discrete Topological Spaces
:: by Zbigniew Karno
::
:: Received April 6, 1993
:: Copyright (c) 1993-2017 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, TMAP_1, RCOMP_1, TARSKI, STRUCT_0,
TOPS_1, TOPS_3, ZFMISC_1, SETFAM_1, TDLAT_3, NATTRA_1, COMPTS_1, TEX_1,
CARD_1;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, SETFAM_1, DOMAIN_1, CARD_1,
STRUCT_0, PRE_TOPC, TOPS_1, TMAP_1, TDLAT_3, TOPS_3, COMPTS_1;
constructors SETFAM_1, DOMAIN_1, TOPS_1, COMPTS_1, PCOMPS_1, TDLAT_3, TMAP_1,
TOPS_3;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, TOPS_1, TDLAT_3, TMAP_1,
CARD_1;
requirements BOOLE, SUBSET, NUMERALS;
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;
registration
cluster 1-element strict for TopStruct;
cluster non trivial strict for TopStruct;
end;
theorem :: TEX_1:8
for Y being 1-element TopStruct st the topology of Y is non
empty holds Y is almost_discrete implies Y is TopSpace-like;
registration
cluster 1-element strict for TopSpace;
end;
registration
cluster -> anti-discrete discrete for 1-element TopSpace;
cluster discrete anti-discrete -> trivial for non empty TopSpace;
end;
registration
cluster non trivial strict for TopSpace;
end;
registration
cluster non discrete -> non trivial for non empty TopSpace;
cluster non anti-discrete -> non trivial for 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;
registration
let D be set;
cluster cobool D -> non empty;
end;
definition
let D be set;
func ADTS(D) -> TopStruct equals
:: TEX_1:def 3
TopStruct(#D,cobool D#);
end;
registration
let D be set;
cluster ADTS(D) -> strict anti-discrete TopSpace-like;
end;
registration
let D be non empty set;
cluster ADTS(D) -> non empty;
end;
theorem :: TEX_1:9
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:10
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:11
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:12
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:13
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:14
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:15
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;
registration
let D be set;
cluster 1TopSp D -> discrete;
end;
theorem :: TEX_1:16
for X being discrete non empty TopSpace for A being Subset of X holds
Cl A = A & Int A = A;
theorem :: TEX_1:17
for X being non empty TopSpace holds (for A being Subset of X holds Cl
A = A) implies X is discrete;
theorem :: TEX_1:18
for X being non empty TopSpace holds (for A being Subset of X holds
Int A = A) implies X is discrete;
theorem :: TEX_1:19
for D being non empty set holds ADTS(D) = 1TopSp(D) iff ex d0
being Element of D st D = {d0};
registration
cluster discrete non anti-discrete strict non empty for TopSpace;
cluster anti-discrete non discrete strict non empty for TopSpace;
end;
begin
:: 4. An Example of a Topological Space.
definition
let D be set, d0 be Element of D;
func STS(D,d0) -> TopStruct equals
:: TEX_1:def 4
TopStruct (#D,(bool D) \ {A where A is
Subset of D : d0 in A & A <> D}#);
end;
registration
let D be set, d0 be Element of D;
cluster STS(D,d0) -> strict TopSpace-like;
end;
registration
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:20
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:21
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:22
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:23
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});
registration
cluster non anti-discrete non discrete strict non empty for TopSpace;
end;
theorem :: TEX_1:24
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:25
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:26
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:27
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:28
STS(D,d0) = ADTS(D) iff D = {d0};
theorem :: TEX_1:29
STS(D,d0) = 1TopSp(D) iff D = {d0};
theorem :: TEX_1:30
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 5
for A being non empty Subset of X holds A is not boundary;
end;
theorem :: TEX_1:31
X is discrete iff for A being Subset of X holds A <> the carrier of X
implies A is not dense;
registration
cluster non almost_discrete -> non discrete non anti-discrete for non empty
TopSpace;
end;
definition
let X be non empty TopSpace;
redefine attr X is almost_discrete means
:: TEX_1:def 6
for A being non empty Subset of X holds A is not nowhere_dense;
end;
theorem :: TEX_1:32
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:33
X is non almost_discrete iff ex A being non empty Subset of X st
A is boundary & A is closed;
theorem :: TEX_1:34
X is non almost_discrete iff ex A being Subset of X st A <> the
carrier of X & A is dense & A is open;
registration
cluster almost_discrete non discrete non anti-discrete strict non empty
for TopSpace;
end;
theorem :: TEX_1:35
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;
registration
cluster non almost_discrete strict non empty for TopSpace;
end;
theorem :: TEX_1:36
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:37
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;