Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

### Subsets of Topological Spaces

by
Miroslaw Wysocki, and
Agata Darmochwal

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

```environ

vocabulary BOOLE, SUBSET_1, PRE_TOPC, TOPS_1;
notation TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC;
constructors PRE_TOPC, MEMBERED;
clusters PRE_TOPC, STRUCT_0, MEMBERED, ZFMISC_1;
requirements BOOLE, SUBSET;

begin

reserve TS for 1-sorted,
K, Q for Subset of TS;

canceled;

theorem :: TOPS_1:2
K \/ [#] TS = [#] TS;

canceled 5;

theorem :: TOPS_1:8
([#]TS)` = {} TS;

canceled 11;

theorem :: TOPS_1:20
K c= Q iff K misses Q`;

theorem :: TOPS_1:21
K` = Q` implies K = Q;

::
::    CLOSED AND OPEN SETS, CLOSURE OF SET
::

reserve TS for TopSpace,
GX for TopStruct,
x for set,
P, Q for Subset of TS,
K, L for Subset of TS,
R, S for Subset of GX,
T, W for Subset of GX;

theorem :: TOPS_1:22
{} TS is closed;

definition let T be TopSpace;
cluster {}T -> closed;
end;

canceled 3;

theorem :: TOPS_1:26
Cl Cl T = Cl T;

theorem :: TOPS_1:27
Cl([#] GX) = [#] GX;

definition let T be TopSpace, P be Subset of T;
cluster Cl P -> closed;
end;

canceled;

theorem :: TOPS_1:29
R is closed iff R` is open;

definition let T be TopSpace, R be closed Subset of T;
cluster R` -> open;
end;

theorem :: TOPS_1:30
R is open iff R` is closed;

definition let T be TopSpace;
cluster open Subset of T;
end;

definition let T be TopSpace, R be open Subset of T;
cluster R` -> closed;
end;

theorem :: TOPS_1:31
S is closed & T c= S implies Cl T c= S;

theorem :: TOPS_1:32
Cl K \ Cl L c= Cl(K \ L);

canceled;

theorem :: TOPS_1:34
R is closed & S is closed implies Cl(R /\ S) = Cl R /\ Cl S;

theorem :: TOPS_1:35
P is closed & Q is closed implies P /\ Q is closed;

theorem :: TOPS_1:36
P is closed & Q is closed implies P \/ Q is closed;

theorem :: TOPS_1:37
P is open & Q is open implies P \/ Q is open;

theorem :: TOPS_1:38
P is open & Q is open implies P /\ Q is open;

theorem :: TOPS_1:39
for GX being non empty TopSpace, R being Subset of GX,
p being Point of GX holds
p in Cl R iff
for T being Subset of GX st T is open & p in T holds R meets T;

theorem :: TOPS_1:40
Q is open implies Q /\ Cl K c= Cl(Q /\ K);

theorem :: TOPS_1:41
Q is open implies Cl(Q /\ Cl K) = Cl(Q /\ K);

::
::    INTERIOR OF A SET
::

definition let GX be TopStruct, R be Subset of GX;
func Int R -> Subset of GX equals
:: TOPS_1:def 1
(Cl R`)`;
end;

canceled;

theorem :: TOPS_1:43
Int([#] TS) = [#] TS;

theorem :: TOPS_1:44
Int T c= T;

theorem :: TOPS_1:45
Int Int T = Int T;

theorem :: TOPS_1:46
Int K /\ Int L = Int(K /\ L);

theorem :: TOPS_1:47
Int({} GX) = {} GX;

theorem :: TOPS_1:48
T c= W implies Int T c= Int W;

theorem :: TOPS_1:49
Int T \/ Int W c= Int(T \/ W);

theorem :: TOPS_1:50
Int(K \ L) c= Int K \ Int L;

theorem :: TOPS_1:51
Int K is open;

definition let T be TopSpace, K be Subset of T;
cluster Int K -> open;
end;

theorem :: TOPS_1:52
{} TS is open;

theorem :: TOPS_1:53
[#] TS is open;

definition let T be TopSpace;
cluster {}T -> open;
cluster [#]T -> open;
end;

definition let T be TopSpace;
cluster open closed Subset of T;
end;

definition let T be non empty TopSpace;
cluster non empty open closed Subset of T;
end;

theorem :: TOPS_1:54
x in Int K iff ex Q st Q is open & Q c= K & x in Q;

theorem :: TOPS_1:55
(R is open implies Int R = R) & (Int P = P implies P is open);

theorem :: TOPS_1:56
S is open & S c= T implies S c= Int T;

theorem :: TOPS_1:57
P is open iff (for x holds x in P iff
ex Q st Q is open & Q c= P & x in Q);

theorem :: TOPS_1:58
Cl Int T = Cl Int Cl Int T;

theorem :: TOPS_1:59
R is open implies Cl Int Cl R = Cl R;

::
::    FRONTIER OF A SET
::

definition let GX be TopStruct, R be Subset of GX;
func Fr R -> Subset of GX equals
:: TOPS_1:def 2
Cl R /\ Cl R`;
end;

canceled;

theorem :: TOPS_1:61
for GX being non empty TopSpace, R being Subset of GX,
p being Point of GX holds p in Fr R iff
(for S being Subset of GX st S is open & p in S
holds R meets S & R` meets S);

theorem :: TOPS_1:62
Fr T = Fr T`;

theorem :: TOPS_1:63
Fr T c= Cl T;

theorem :: TOPS_1:64
Fr T = Cl(T`) /\ T \/ (Cl T \ T);

theorem :: TOPS_1:65
Cl T = T \/ Fr T;

theorem :: TOPS_1:66
Fr(K /\ L) c= Fr K \/ Fr L;

theorem :: TOPS_1:67
Fr(K \/ L) c= Fr K \/ Fr L;

theorem :: TOPS_1:68
Fr Fr T c= Fr T;

theorem :: TOPS_1:69
R is closed implies Fr R c= R;

theorem :: TOPS_1:70
Fr K \/ Fr L = Fr(K \/ L) \/ Fr(K /\ L) \/ (Fr K /\ Fr L);

theorem :: TOPS_1:71
Fr Int T c= Fr T;

theorem :: TOPS_1:72
Fr Cl T c= Fr T;

theorem :: TOPS_1:73
Int T misses Fr T;

theorem :: TOPS_1:74
Int T = T \ Fr T;

theorem :: TOPS_1:75
Fr Fr Fr K = Fr Fr K;

theorem :: TOPS_1:76
P is open iff Fr P = Cl P \ P;

theorem :: TOPS_1:77
P is closed iff Fr P = P \ Int P;

::
::    DENSE, BOUNDARY AND NOWHEREDENSE SETS
::

definition let GX be TopStruct, R be Subset of GX;
attr R is dense means
:: TOPS_1:def 3
Cl R = [#] GX;
end;

canceled;

theorem :: TOPS_1:79
R is dense & R c= S implies S is dense;

theorem :: TOPS_1:80
P is dense iff (for Q st Q <> {} & Q is open holds P meets Q);

theorem :: TOPS_1:81
P is dense implies (for Q holds Q is open implies Cl Q = Cl(Q /\ P));

theorem :: TOPS_1:82
P is dense & Q is dense & Q is open implies P /\ Q is dense;

definition let GX be TopStruct, R be Subset of GX;
attr R is boundary means
:: TOPS_1:def 4
R` is dense;
end;

canceled;

theorem :: TOPS_1:84
R is boundary iff Int R = {};

theorem :: TOPS_1:85
P is boundary & Q is boundary & Q is closed implies
P \/ Q is boundary;

theorem :: TOPS_1:86
P is boundary iff (for Q st Q c= P & Q is open holds Q = {});

theorem :: TOPS_1:87
P is closed implies (P is boundary iff
for Q st Q <> {} & Q is open
ex G being Subset of TS st G c= Q & G <> {} & G is open & P misses G);

theorem :: TOPS_1:88
R is boundary iff R c= Fr R;

definition let GX be TopStruct, R be Subset of GX;
attr R is nowhere_dense means
:: TOPS_1:def 5
Cl R is boundary;
end;

canceled;

theorem :: TOPS_1:90
P is nowhere_dense & Q is nowhere_dense implies P \/ Q is nowhere_dense;

theorem :: TOPS_1:91
R is nowhere_dense implies R` is dense;

theorem :: TOPS_1:92
R is nowhere_dense implies R is boundary;

theorem :: TOPS_1:93
S is boundary & S is closed implies S is nowhere_dense;

theorem :: TOPS_1:94
R is closed implies (R is nowhere_dense iff R = Fr R);

theorem :: TOPS_1:95
P is open implies Fr P is nowhere_dense;

theorem :: TOPS_1:96
P is closed implies Fr P is nowhere_dense;

theorem :: TOPS_1:97
P is open & P is nowhere_dense implies P = {};

::
::    CLOSED AND OPEN DOMAIN, DOMAIN
::

definition let GX be TopStruct, R be Subset of GX;
attr R is condensed means
:: TOPS_1:def 6
Int Cl R c= R & R c= Cl Int R;
attr R is closed_condensed means
:: TOPS_1:def 7
R = Cl Int R;
attr R is open_condensed means
:: TOPS_1:def 8
R = Int Cl R;
end;

canceled 3;

theorem :: TOPS_1:101
R is open_condensed iff R` is closed_condensed;

theorem :: TOPS_1:102
R is closed_condensed implies Fr Int R = Fr R;

theorem :: TOPS_1:103
R is closed_condensed implies Fr R c= Cl Int R;

theorem :: TOPS_1:104
R is open_condensed implies Fr R = Fr Cl R & Fr Cl R = Cl R \ R;

theorem :: TOPS_1:105
R is open & R is closed implies
(R is closed_condensed iff R is open_condensed);

theorem :: TOPS_1:106
(R is closed & R is condensed implies R is closed_condensed) &
(P is closed_condensed implies P is closed & P is condensed);

theorem :: TOPS_1:107
(R is open & R is condensed implies R is open_condensed) &
(P is open_condensed implies P is open & P is condensed);

theorem :: TOPS_1:108
P is closed_condensed & Q is closed_condensed implies
P \/ Q is closed_condensed;

theorem :: TOPS_1:109
P is open_condensed & Q is open_condensed implies P /\ Q is open_condensed;

theorem :: TOPS_1:110
P is condensed implies Int Fr P = {};

theorem :: TOPS_1:111
R is condensed implies Int R is condensed & Cl R is condensed;
```