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

### Maximal Discrete Subspaces of Almost Discrete Topological Spaces

by
Zbigniew Karno

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

```environ

vocabulary REALSET1, BOOLE, COLLSP, TARSKI, SUBSET_1, PRE_TOPC, SETFAM_1,
RELAT_1, NATTRA_1, TDLAT_3, TOPS_3, TOPS_1, FUNCT_1, ORDINAL2, TEX_1,
BORSUK_1, TEX_2, PCOMPS_1;
notation TARSKI, XBOOLE_0, SUBSET_1, DOMAIN_1, RELAT_1, FUNCT_1, PARTFUN1,
FUNCT_2, REALSET1, STRUCT_0, PRE_TOPC, TOPS_1, TOPS_2, BORSUK_1, TSEP_1,
TDLAT_3, TOPS_3, PCOMPS_1, TEX_1;
constructors DOMAIN_1, REALSET1, TOPS_1, TOPS_2, TMAP_1, BORSUK_1, TOPS_3,
TEX_1, TDLAT_3, MEMBERED, PARTFUN1;
clusters PRE_TOPC, TDLAT_3, TEX_1, REALSET1, STRUCT_0, RELSET_1, PCOMPS_1,
SUBSET_1, BORSUK_1, MEMBERED, ZFMISC_1, FUNCT_2, PARTFUN1;
requirements BOOLE, SUBSET;

begin
:: 1. Proper Subsets of 1-sorted Structures.

definition let X be non empty set;
redefine attr X is trivial means
:: TEX_2:def 1
ex s being Element of X st X = {s};
end;

definition
cluster trivial non empty set;
end;

theorem :: TEX_2:1
for A being non empty set, B being trivial non empty set st
A c= B holds A = B;

theorem :: TEX_2:2
for A being trivial non empty set, B being set st
A /\ B is non empty holds A c= B;

canceled;

theorem :: TEX_2:4
for S, T being 1-sorted st the carrier of S = the carrier of T
holds S is trivial implies T is trivial;

definition let S be set;
let IT be Element of S;
attr IT is proper means
:: TEX_2:def 2
IT <> union S;
end;

definition let S be set;
cluster non proper Subset of S;
end;

theorem :: TEX_2:5
for S being set, A being Subset of S holds A is proper iff A <> S;

definition let S be non empty set;
cluster non proper -> non empty Subset of S;
cluster empty -> proper Subset of S;
end;

definition let S be trivial non empty set;
cluster proper -> empty Subset of S;
cluster non empty -> non proper Subset of S;
end;

definition let S be non empty set;
cluster proper Subset of S;
cluster non proper Subset of S;
end;

definition let S be non empty set;
cluster trivial (non empty Subset of S);
end;

definition let y be set;
cluster {y} -> trivial;
end;

theorem :: TEX_2:6
for S being non empty set, y being Element of S holds
{y} is proper implies S is non trivial;

theorem :: TEX_2:7
for S being non trivial non empty set, y being Element of S holds
{y} is proper;

definition let S be trivial non empty set;
cluster non proper -> trivial (non empty Subset of S);
end;

definition let S be non trivial non empty set;
cluster trivial -> proper (non empty Subset of S);
cluster non proper -> non trivial (non empty Subset of S);
end;

definition let S be non trivial non empty set;
cluster trivial proper (non empty Subset of S);
cluster non trivial non proper (non empty Subset of S);
end;

theorem :: TEX_2:8
for Y being non empty 1-sorted, y being Element of Y holds
{y} is proper implies Y is non trivial;

theorem :: TEX_2:9
for Y being non trivial non empty 1-sorted,
y being Element of Y holds
{y} is proper;

definition let Y be trivial non empty 1-sorted;
cluster -> non proper (non empty Subset of Y);
cluster non proper -> trivial (non empty Subset of Y);
end;

definition let Y be non trivial non empty 1-sorted;
cluster trivial -> proper (non empty Subset of Y);
cluster non proper -> non trivial (non empty Subset of Y);
end;

definition let Y be non trivial non empty 1-sorted;
cluster trivial proper (non empty Subset of Y);
cluster non trivial non proper (non empty Subset of Y);
end;

definition let Y be non trivial non empty 1-sorted;
cluster non empty trivial proper Subset of Y;
end;

begin
:: 2. Proper Subspaces of Topological Spaces.

theorem :: TEX_2:10
for X being non empty TopStruct, X0 being SubSpace of X holds
the TopStruct of X0 is strict SubSpace of X;

canceled;

theorem :: TEX_2:12
for Y0, Y1 being TopStruct st
the TopStruct of Y0 = the TopStruct of Y1 holds
Y0 is TopSpace-like implies Y1 is TopSpace-like;

definition let Y be TopStruct;
let IT be SubSpace of Y;
attr IT is proper means
:: TEX_2:def 3
for A being Subset of Y st A = the carrier of IT
holds A is proper;
end;

reserve Y for TopStruct;

theorem :: TEX_2:13
for Y0 being SubSpace of Y, A being Subset of Y st
A = the carrier of Y0 holds A is proper iff Y0 is proper;

theorem :: TEX_2:14
for Y0, Y1 being SubSpace of Y st
the TopStruct of Y0 = the TopStruct of Y1 holds
Y0 is proper implies Y1 is proper;

theorem :: TEX_2:15
for Y0 being SubSpace of Y holds
the carrier of Y0 = the carrier of Y implies Y0 is non proper;

definition let Y be trivial non empty TopStruct;
cluster -> non proper (non empty SubSpace of Y);
cluster non proper -> trivial (non empty SubSpace of Y);
end;

definition let Y be non trivial non empty TopStruct;
cluster trivial -> proper (non empty SubSpace of Y);
cluster non proper -> non trivial (non empty SubSpace of Y);
end;

definition let Y be non empty TopStruct;
cluster non proper strict non empty SubSpace of Y;
end;

theorem :: TEX_2:16
for Y being non empty TopStruct,
Y0 being non proper SubSpace of Y holds
the TopStruct of Y0 = the TopStruct of Y;

definition let Y be non empty TopStruct;
cluster discrete -> TopSpace-like SubSpace of Y;
cluster anti-discrete -> TopSpace-like SubSpace of Y;
cluster non TopSpace-like -> non discrete SubSpace of Y;
cluster non TopSpace-like -> non anti-discrete SubSpace of Y;
end;

theorem :: TEX_2:17
for Y0, Y1 being TopStruct st
the TopStruct of Y0 = the TopStruct of Y1 holds
Y0 is discrete implies Y1 is discrete;

theorem :: TEX_2:18
for Y0, Y1 being TopStruct st
the TopStruct of Y0 = the TopStruct of Y1 holds
Y0 is anti-discrete implies Y1 is anti-discrete;

definition let Y be non empty TopStruct;
cluster discrete -> almost_discrete SubSpace of Y;
cluster non almost_discrete -> non discrete SubSpace of Y;
cluster anti-discrete -> almost_discrete SubSpace of Y;
cluster non almost_discrete -> non anti-discrete SubSpace of Y;
end;

theorem :: TEX_2:19
for Y0, Y1 being TopStruct st
the TopStruct of Y0 = the TopStruct of Y1 holds
Y0 is almost_discrete implies Y1 is almost_discrete;

definition let Y be non empty TopStruct;
cluster discrete anti-discrete -> trivial (non empty SubSpace of Y);
cluster anti-discrete non trivial -> non discrete (non empty SubSpace of Y);
cluster discrete non trivial -> non anti-discrete (non empty SubSpace of Y);
end;

definition let Y be non empty TopStruct, y be Point of Y;
func Sspace(y) -> strict non empty SubSpace of Y means
:: TEX_2:def 4
the carrier of it = {y};
end;

definition let Y be non empty TopStruct;
cluster trivial strict non empty SubSpace of Y;
end;

definition let Y be non empty TopStruct, y be Point of Y;
cluster Sspace(y) -> trivial;
end;

theorem :: TEX_2:20
for Y being non empty TopStruct, y being Point of Y holds
Sspace(y) is proper iff {y} is proper;

theorem :: TEX_2:21
for Y being non empty TopStruct, y being Point of Y holds
Sspace(y) is proper implies Y is non trivial;

theorem :: TEX_2:22
for Y being non trivial non empty TopStruct, y being Point of Y holds
Sspace(y) is proper;

definition let Y be non trivial non empty TopStruct;
cluster proper trivial strict (non empty SubSpace of Y);
end;

theorem :: TEX_2:23
for Y being non empty TopStruct, Y0 be trivial non empty SubSpace of Y holds
ex y being Point of Y st the TopStruct of Y0 = the TopStruct of Sspace(y);

theorem :: TEX_2:24
for Y being non empty TopStruct, y being Point of Y holds
Sspace(y) is TopSpace-like implies Sspace(y) is discrete anti-discrete;

definition let Y be non empty TopStruct;
cluster trivial TopSpace-like ->
discrete anti-discrete (non empty SubSpace of Y);
end;

definition let X be non empty TopSpace;
cluster trivial strict TopSpace-like non empty SubSpace of X;
end;

definition let X be non empty TopSpace, x be Point of X;
cluster Sspace(x) -> TopSpace-like;
end;

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

definition let X be non empty TopSpace, x be Point of X;
cluster Sspace(x) -> discrete anti-discrete;
end;

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

definition let X be non empty TopSpace;
cluster open closed strict SubSpace of X;
end;

definition let X be discrete non empty TopSpace;
cluster anti-discrete -> trivial (non empty SubSpace of X);
cluster non trivial -> non anti-discrete (non empty SubSpace of X);
end;

definition let X be discrete non trivial non empty TopSpace;
cluster discrete open closed proper strict SubSpace of X;
end;

definition let X be anti-discrete non empty TopSpace;
cluster discrete -> trivial (non empty SubSpace of X);
cluster non trivial -> non discrete (non empty SubSpace of X);
end;

definition let X be anti-discrete non trivial non empty TopSpace;
cluster -> non open non closed (proper non empty SubSpace of X);
cluster -> trivial proper (discrete non empty SubSpace of X);
end;

definition let X be anti-discrete non trivial non empty TopSpace;
cluster anti-discrete non open non closed proper strict SubSpace of X;
end;

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

begin
:: 3. Maximal Discrete Subsets and Subspaces.

definition let Y be TopStruct,
IT be Subset of Y;
attr IT is discrete means
:: TEX_2:def 5
for D being Subset of Y st D c= IT
ex G being Subset of Y st G is open & IT /\ G = D;
end;

definition let Y be TopStruct;
let A be Subset of Y;
redefine attr A is discrete means
:: TEX_2:def 6
for D being Subset of Y st D c= A
ex F being Subset of Y st F is closed & A /\ F = D;
end;

theorem :: TEX_2:25
for Y0, Y1 being TopStruct, D0 being Subset of Y0,
D1 being Subset of Y1 st
the TopStruct of Y0 = the TopStruct of Y1 & D0 = D1 holds
D0 is discrete implies D1 is discrete;

theorem :: TEX_2:26
for Y being non empty TopStruct,
Y0 being non empty SubSpace of Y, A being Subset of Y
st A = the carrier of Y0 holds
A is discrete iff Y0 is discrete;

theorem :: TEX_2:27
for Y being non empty TopStruct, A being Subset of Y
st A = the carrier of Y
holds A is discrete iff Y is discrete;

theorem :: TEX_2:28
for A, B being Subset of Y st B c= A holds
A is discrete implies B is discrete;

theorem :: TEX_2:29
for A, B being Subset of Y holds
A is discrete or B is discrete implies A /\ B is discrete;

theorem :: TEX_2:30
(for P, Q being Subset of Y st P is open & Q is open holds
P /\ Q is open & P \/ Q is open)
implies
for A, B being Subset of Y st A is open & B is open holds
A is discrete & B is discrete implies A \/ B is discrete;

theorem :: TEX_2:31
(for P, Q being Subset of Y st P is closed & Q is closed holds
P /\ Q is closed & P \/ Q is closed)
implies
for A, B being Subset of Y st A is closed & B is closed
holds
A is discrete & B is discrete implies A \/ B is discrete;

theorem :: TEX_2:32
for A being Subset of Y holds A is discrete implies
for x being Point of Y st x in A
ex G being Subset of Y st G is open & A /\ G = {x};

theorem :: TEX_2:33
for A being Subset of Y holds A is discrete implies
for x being Point of Y st x in A
ex F being Subset of Y st F is closed & A /\ F = {x};

reserve X for non empty TopSpace;

theorem :: TEX_2:34
for A0 being non empty Subset of X st A0 is discrete
ex X0 being discrete strict non empty SubSpace of X st A0 = the carrier of X0
;

theorem :: TEX_2:35
for A being empty Subset of X holds A is discrete;

theorem :: TEX_2:36
for x being Point of X holds {x} is discrete;

theorem :: TEX_2:37
for A being Subset of X holds
(for x being Point of X st x in A
ex G being Subset of X st G is open & A /\ G = {x})
implies
A is discrete;

theorem :: TEX_2:38
for A, B being Subset of X st A is open & B is open holds
A is discrete & B is discrete implies A \/ B is discrete;

theorem :: TEX_2:39
for A, B being Subset of X st A is closed & B is closed holds
A is discrete & B is discrete implies A \/ B is discrete;

theorem :: TEX_2:40
for A being Subset of X st A is everywhere_dense holds
A is discrete implies A is open;

theorem :: TEX_2:41
for A being Subset of X holds
A is discrete iff
for D being Subset of X st D c= A holds A /\ Cl D = D;

theorem :: TEX_2:42
for A being Subset of X holds A is discrete implies
for x being Point of X st x in A holds A /\ Cl {x} = {x};

theorem :: TEX_2:43
for X being discrete non empty TopSpace, A being Subset of X
holds A is discrete;

theorem :: TEX_2:44
for X being anti-discrete non empty TopSpace,
A being non empty Subset of X holds
A is discrete iff A is trivial;

definition let Y be TopStruct,
IT be Subset of Y;
attr IT is maximal_discrete means
:: TEX_2:def 7
IT is discrete &
for D being Subset of Y st D is discrete & IT c= D holds IT = D;
end;

theorem :: TEX_2:45
for Y0, Y1 being TopStruct, D0 being Subset of Y0,
D1 being Subset of Y1 st
the TopStruct of Y0 = the TopStruct of Y1 & D0 = D1 holds
D0 is maximal_discrete implies D1 is maximal_discrete;

theorem :: TEX_2:46
for A being empty Subset of X holds A is not maximal_discrete;

theorem :: TEX_2:47
for A being Subset of X st A is open holds
A is maximal_discrete implies A is dense;

theorem :: TEX_2:48
for A being Subset of X st A is dense holds
A is discrete implies A is maximal_discrete;

theorem :: TEX_2:49
for X being discrete non empty TopSpace, A being Subset of X
holds A is maximal_discrete iff A is non proper;

theorem :: TEX_2:50
for X being anti-discrete non empty TopSpace,
A being non empty Subset of X holds
A is maximal_discrete iff A is trivial;

definition let Y be non empty TopStruct;
let IT be SubSpace of Y;
attr IT is maximal_discrete means
:: TEX_2:def 8
for A being Subset of Y st A = the carrier of IT holds
A is maximal_discrete;
end;

theorem :: TEX_2:51
for Y being non empty TopStruct, Y0 being SubSpace of Y,
A being Subset of Y st
A = the carrier of Y0 holds
A is maximal_discrete iff Y0 is maximal_discrete;

definition let Y be non empty TopStruct;
cluster maximal_discrete -> discrete (non empty SubSpace of Y);
cluster non discrete -> non maximal_discrete (non empty SubSpace of Y);
end;

theorem :: TEX_2:52
for X0 being non empty SubSpace of X holds
X0 is maximal_discrete iff
X0 is discrete &
for Y0 being discrete non empty SubSpace of X st X0 is SubSpace of Y0 holds
the TopStruct of X0 = the TopStruct of Y0;

theorem :: TEX_2:53
for A0 being non empty Subset of X st A0 is maximal_discrete
ex X0 being strict non empty SubSpace of X st
X0 is maximal_discrete & A0 = the carrier of X0;

definition let X be discrete non empty TopSpace;
cluster maximal_discrete -> non proper SubSpace of X;
cluster proper -> non maximal_discrete SubSpace of X;
cluster non proper -> maximal_discrete SubSpace of X;
cluster non maximal_discrete -> proper SubSpace of X;
end;

definition let X be anti-discrete non empty TopSpace;
cluster maximal_discrete -> trivial (non empty SubSpace of X);
cluster non trivial -> non maximal_discrete (non empty SubSpace of X);
cluster trivial -> maximal_discrete (non empty SubSpace of X);
cluster non maximal_discrete -> non trivial (non empty SubSpace of X);
end;

begin
:: 4. Maximal Discrete Subspaces of Almost Discrete Spaces.

scheme
ExChoiceFCol{X()->non empty TopStruct,F()->Subset-Family of X(),P[set,set]}:
ex f being Function of F(),the carrier of X() st
for S being Subset of X() st S in F() holds P[S,f.S]
provided
for S being Subset of X() st S in F()
ex x being Point of X() st P[S,x];

reserve X for almost_discrete non empty TopSpace;

theorem :: TEX_2:54
for A being Subset of X holds
Cl A = union {Cl {a} where a is Point of X : a in A};

theorem :: TEX_2:55
for a, b being Point of X holds
a in Cl {b} implies Cl {a} = Cl {b};

theorem :: TEX_2:56
for a, b being Point of X holds
Cl {a} misses Cl {b} or Cl {a} = Cl {b};

theorem :: TEX_2:57
for A being Subset of X holds
(for x being Point of X st x in A
ex F being Subset of X st F is closed & A /\ F = {x})
implies
A is discrete;

theorem :: TEX_2:58
for A being Subset of X holds
(for x being Point of X st x in A holds A /\ Cl {x} = {x}) implies
A is discrete;

theorem :: TEX_2:59
for A being Subset of X holds
A is discrete iff
for a, b being Point of X st a in A & b in A holds
a <> b implies Cl {a} misses Cl {b};

theorem :: TEX_2:60
for A being Subset of X holds
A is discrete iff
for x being Point of X st x in Cl A
ex a being Point of X st a in A & A /\ Cl {x} = {a};

theorem :: TEX_2:61
for A being Subset of X st A is open or A is closed holds
A is maximal_discrete implies A is not proper;

theorem :: TEX_2:62
for A being Subset of X holds
A is maximal_discrete implies A is dense;

theorem :: TEX_2:63
for A being Subset of X st A is maximal_discrete holds
union {Cl {a} where a is Point of X : a in A} = the carrier of X;

theorem :: TEX_2:64
for A being Subset of X holds
A is maximal_discrete iff
for x being Point of X ex a being Point of X st
a in A & A /\ Cl {x} = {a};

theorem :: TEX_2:65
for A being Subset of X holds A is discrete implies
ex M being Subset of X st A c= M & M is maximal_discrete;

theorem :: TEX_2:66
ex M being Subset of X st M is maximal_discrete;

theorem :: TEX_2:67
for Y0 being discrete non empty SubSpace of X
ex X0 being strict non empty SubSpace of X st
Y0 is SubSpace of X0 & X0 is maximal_discrete;

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

definition let X be almost_discrete non anti-discrete non empty TopSpace;
cluster maximal_discrete -> non trivial (non empty SubSpace of X);
cluster trivial -> non maximal_discrete (non empty SubSpace of X);
end;

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

begin
:: 5. Continuous Mappings and Almost Discrete Spaces.

scheme MapExChoiceF{X,Y()->non empty TopStruct,P[set,set]}:
ex f being map of X(),Y() st
for x being Point of X() holds P[x,f.x]
provided
for x being Point of X() ex y being Point of Y() st P[x,y];

reserve X,Y for non empty TopSpace;

theorem :: TEX_2:68
for X being discrete non empty TopSpace, f being map of X,Y holds
f is continuous;

theorem :: TEX_2:69
(for Y being non empty TopSpace, f being map of X,Y holds f is continuous)
implies X is discrete;

theorem :: TEX_2:70
for Y being anti-discrete non empty TopSpace, f being map of X,Y holds
f is continuous;

theorem :: TEX_2:71
(for X being non empty TopSpace, f being map of X,Y holds f is continuous)
implies Y is anti-discrete;

reserve X for discrete non empty TopSpace, X0 for non empty SubSpace of X;

theorem :: TEX_2:72
ex r being continuous map of X,X0 st r is_a_retraction;

theorem :: TEX_2:73
X0 is_a_retract_of X;

reserve X for almost_discrete non empty TopSpace,
X0 for maximal_discrete non empty SubSpace of X;

theorem :: TEX_2:74
ex r being continuous map of X,X0 st r is_a_retraction;

theorem :: TEX_2:75
X0 is_a_retract_of X;

theorem :: TEX_2:76
for r being continuous map of X,X0 holds
r is_a_retraction implies
for F being Subset of X0, E being Subset of X
st F = E holds r" F = Cl E;

theorem :: TEX_2:77
for r being continuous map of X,X0 holds
r is_a_retraction implies
for a being Point of X0, b being Point of X st a = b holds r" {a} = Cl {b};

reserve X0 for discrete non empty SubSpace of X;

theorem :: TEX_2:78
ex r being continuous map of X,X0 st r is_a_retraction;

theorem :: TEX_2:79
X0 is_a_retract_of X;
```