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

### Remarks on Special Subsets of Topological Spaces

by
Zbigniew Karno

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

```environ

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

begin
:: 1. Selected Properties of Subsets of a Topological Space.
reserve X for TopStruct, A for Subset of X;

theorem :: TOPS_3:1
(A = {}X iff  A` = [#]X) &
(A = {} iff  A` = the carrier of X);

theorem :: TOPS_3:2
(A = [#]X iff  A` = {}X) &
(A = the carrier of X iff  A` = {});

theorem :: TOPS_3:3
for X being TopSpace, A,B being Subset of X holds
Int A /\ Cl B c= Cl(A /\ B);

reserve X for TopSpace, A,B for Subset of X;

theorem :: TOPS_3:4
Int(A \/ B) c= (Cl A) \/ Int B;

theorem :: TOPS_3:5
for A being Subset of X st A is closed holds Int(A \/ B) c= A \/ Int B;

theorem :: TOPS_3:6
for A being Subset of X st A is closed holds Int(A \/ B) = Int(A \/ Int B);

theorem :: TOPS_3:7
A misses Int Cl A implies Int Cl A = {};

theorem :: TOPS_3:8
A \/ Cl Int A = the carrier of X implies Cl Int A = the carrier of X;

begin
:: 2. Special Subsets of a Topological Space.

definition let X be TopStruct, A be Subset of X;
redefine attr A is boundary means
:: TOPS_3:def 1
Int A = {};
end;

theorem :: TOPS_3:9
{}X is boundary;

reserve X for non empty TopSpace, A for Subset of X;

theorem :: TOPS_3:10
A is boundary implies A <> the carrier of X;

reserve X for TopSpace, A,B for Subset of X;

theorem :: TOPS_3:11
B is boundary & A c= B implies A is boundary;

theorem :: TOPS_3:12
A is boundary iff
for C being Subset of X st  A` c= C & C is closed
holds C = the carrier of X;

theorem :: TOPS_3:13
A is boundary iff
for G being Subset of X st G <> {} & G is open holds ( A`) meets G;

theorem :: TOPS_3:14
A is boundary iff
for F being Subset of X holds F is closed
implies Int F = Int(F \/ A);

theorem :: TOPS_3:15
A is boundary or B is boundary implies A /\ B is boundary;

definition let X be TopStruct, A be Subset of X;
redefine attr A is dense means
:: TOPS_3:def 2
Cl A = the carrier of X;
end;

theorem :: TOPS_3:16
[#]X is dense;

reserve X for non empty TopSpace, A, B for Subset of X;

theorem :: TOPS_3:17
A is dense implies A <> {};

theorem :: TOPS_3:18
A is dense iff  A` is boundary;

theorem :: TOPS_3:19
A is dense iff
for C being Subset of X st A c= C & C is closed
holds C = the carrier of X;

theorem :: TOPS_3:20
A is dense iff
for G being Subset of X holds G is open
implies Cl G = Cl(G /\ A);

theorem :: TOPS_3:21
A is dense or B is dense implies A \/ B is dense;

definition let X be TopStruct, A be Subset of X;
redefine attr A is nowhere_dense means
:: TOPS_3:def 3
Int(Cl A) = {};
end;

theorem :: TOPS_3:22
{}X is nowhere_dense;

theorem :: TOPS_3:23
A is nowhere_dense implies A <> the carrier of X;

theorem :: TOPS_3:24
A is nowhere_dense implies Cl A is nowhere_dense;

theorem :: TOPS_3:25
A is nowhere_dense implies A is not dense;

theorem :: TOPS_3:26
B is nowhere_dense & A c= B implies A is nowhere_dense;

theorem :: TOPS_3:27
A is nowhere_dense iff ex C being Subset of X st
A c= C & C is closed & C is boundary;

theorem :: TOPS_3:28
A is nowhere_dense iff
for G being Subset of X st G <> {} & G is open
ex H being Subset of X
st H c= G & H <> {} & H is open & A misses H;

theorem :: TOPS_3:29
A is nowhere_dense or B is nowhere_dense implies A /\ B is nowhere_dense;

theorem :: TOPS_3:30
A is nowhere_dense & B is boundary implies A \/ B is boundary;

definition let X be TopStruct, A be Subset of X;
attr A is everywhere_dense means
:: TOPS_3:def 4
Cl(Int A) = [#]X;
end;

definition let X be TopStruct, A be Subset of X;
redefine attr A is everywhere_dense means
:: TOPS_3:def 5
Cl(Int A) = the carrier of X;
end;

theorem :: TOPS_3:31
[#]X is everywhere_dense;

theorem :: TOPS_3:32
A is everywhere_dense implies Int A is everywhere_dense;

theorem :: TOPS_3:33
A is everywhere_dense implies A is dense;

theorem :: TOPS_3:34
A is everywhere_dense implies A <> {};

theorem :: TOPS_3:35
A is everywhere_dense iff Int A is dense;

theorem :: TOPS_3:36
A is open & A is dense implies A is everywhere_dense;

theorem :: TOPS_3:37
A is everywhere_dense implies A is not boundary;

theorem :: TOPS_3:38
A is everywhere_dense & A c= B implies B is everywhere_dense;

theorem :: TOPS_3:39
A is everywhere_dense iff  A` is nowhere_dense;

theorem :: TOPS_3:40
A is nowhere_dense iff  A` is everywhere_dense;

theorem :: TOPS_3:41
A is everywhere_dense iff ex C being Subset of X st
C c= A & C is open & C is dense;

theorem :: TOPS_3:42
A is everywhere_dense iff
for F being Subset of X st F <> the carrier of X & F is closed
ex H being Subset of X st
F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X;

theorem :: TOPS_3:43
A is everywhere_dense or B is everywhere_dense implies
A \/ B is everywhere_dense;

theorem :: TOPS_3:44
A is everywhere_dense & B is everywhere_dense implies
A /\ B is everywhere_dense;

theorem :: TOPS_3:45
A is everywhere_dense & B is dense implies A /\ B is dense;

theorem :: TOPS_3:46
A is dense & B is nowhere_dense implies A \ B is dense;

theorem :: TOPS_3:47
A is everywhere_dense & B is boundary implies A \ B is dense;

theorem :: TOPS_3:48
A is everywhere_dense & B is nowhere_dense implies A \ B is everywhere_dense
;

reserve D for Subset of X;

theorem :: TOPS_3:49
D is everywhere_dense implies
ex C,B being Subset of X st
C is open & C is dense & B is nowhere_dense & C \/ B = D & C misses B;

theorem :: TOPS_3:50
D is everywhere_dense implies
ex C,B being Subset of X
st C is open & C is dense & B is closed &
B is boundary & C \/ (D /\ B) = D &
C misses B & C \/ B = the carrier of X;

theorem :: TOPS_3:51
D is nowhere_dense implies
ex C,B being Subset of X st C is closed & C is boundary &
B is everywhere_dense & C /\ B = D & C \/ B = the carrier of X;

theorem :: TOPS_3:52
D is nowhere_dense implies
ex C,B being Subset of X st C is closed & C is boundary & B is open &
B is dense & C /\ (D \/ B) = D & C misses B & C \/ B = the carrier of X;

begin
:: 3. Properties of Subsets in Subspaces.
reserve Y0 for SubSpace of X;

theorem :: TOPS_3:53
for A being Subset of X, B being Subset of Y0
st B c= A holds Cl B c= Cl A;

theorem :: TOPS_3:54
for C, A being Subset of X,
B being Subset of Y0 st
C is closed & C c= the carrier of Y0 & A c= C & A = B holds Cl A = Cl B;

theorem :: TOPS_3:55
for Y0 being closed non empty SubSpace of X
for A being Subset of X, B being Subset of Y0
st A = B holds Cl A = Cl B;

theorem :: TOPS_3:56
for A being Subset of X, B being Subset of Y0
st A c= B holds Int A c= Int B;

theorem :: TOPS_3:57
for Y0 being non empty SubSpace of X,
C, A being Subset of X,
B being Subset of Y0 st
C is open & C c= the carrier of Y0 & A c= C & A = B holds Int A = Int B;

theorem :: TOPS_3:58
for Y0 being open non empty SubSpace of X
for A being Subset of X, B being Subset of Y0
st A = B holds Int A = Int B;

reserve X0 for SubSpace of X;

theorem :: TOPS_3:59
for A being Subset of X, B being Subset of X0 st A c= B holds
A is dense implies B is dense;

theorem :: TOPS_3:60
for C, A being Subset of X, B being Subset of X0 st
C c= the carrier of X0 & A c= C & A = B holds
C is dense & B is dense iff A is dense;

reserve X0 for non empty SubSpace of X;

theorem :: TOPS_3:61
for A being Subset of X, B being Subset of X0 st A c= B holds
A is everywhere_dense implies B is everywhere_dense;

theorem :: TOPS_3:62
for C, A being Subset of X,
B being Subset of X0 st
C is open & C c= the carrier of X0 & A c= C & A = B holds
C is dense & B is everywhere_dense iff A is everywhere_dense;

theorem :: TOPS_3:63
for X0 being open non empty SubSpace of X
for A,C being Subset of X,
B being Subset of X0 st
C = the carrier of X0 & A = B holds
C is dense & B is everywhere_dense iff A is everywhere_dense;

theorem :: TOPS_3:64
for C, A being Subset of X,
B being Subset of X0 st
C c= the carrier of X0 & A c= C & A = B holds
C is everywhere_dense & B is everywhere_dense iff A is everywhere_dense;

theorem :: TOPS_3:65
for A being Subset of X,
B being Subset of X0 st A c= B holds
B is boundary implies A is boundary;

theorem :: TOPS_3:66
for C, A being Subset of X,
B being Subset of X0 st
C is open & C c= the carrier of X0 & A c= C & A = B holds
A is boundary implies B is boundary;

theorem :: TOPS_3:67
for X0 being open non empty SubSpace of X
for A being Subset of X,
B being Subset of X0 st A = B holds
A is boundary iff B is boundary;

theorem :: TOPS_3:68
for A being Subset of X,
B being Subset of X0 st A c= B holds
B is nowhere_dense implies A is nowhere_dense;

theorem :: TOPS_3:69
for C, A being Subset of X,
B being Subset of X0 st
C is open & C c= the carrier of X0 & A c= C & A = B holds
A is nowhere_dense implies B is nowhere_dense;

theorem :: TOPS_3:70
for X0 being open non empty SubSpace of X
for A being Subset of X,
B being Subset of X0 st A = B holds
A is nowhere_dense iff B is nowhere_dense;

begin
:: 4. Subsets in Topological Spaces with the same Topological Structures.
theorem :: TOPS_3:71
for X1, X2 being 1-sorted holds
the carrier of X1 = the carrier of X2 implies
for C1 being Subset of X1,
C2 being Subset of X2 holds
C1 = C2 iff  C1` =  C2`;

reserve X1,X2 for TopStruct;

theorem :: TOPS_3:72
the carrier of X1 = the carrier of X2 &
(for C1 being Subset of X1,
C2 being Subset of X2 st C1 = C2 holds
(C1 is open iff C2 is open)) implies
the TopStruct of X1 = the TopStruct of X2;

theorem :: TOPS_3:73
the carrier of X1 = the carrier of X2 &
(for C1 being Subset of X1,
C2 being Subset of X2 st C1 = C2 holds
(C1 is closed iff C2 is closed)) implies
the TopStruct of X1 = the TopStruct of X2;

reserve X1,X2 for TopSpace;

theorem :: TOPS_3:74
the carrier of X1 = the carrier of X2 &
(for C1 being Subset of X1,
C2 being Subset of X2 st C1 = C2 holds
Int C1 = Int C2) implies
the TopStruct of X1 = the TopStruct of X2;

theorem :: TOPS_3:75
the carrier of X1 = the carrier of X2 &
(for C1 being Subset of X1,
C2 being Subset of X2 st C1 = C2 holds
Cl C1 = Cl C2) implies
the TopStruct of X1 = the TopStruct of X2;

reserve D1 for Subset of X1, D2 for Subset of X2;

theorem :: TOPS_3:76
D1 = D2 & the TopStruct of X1 = the TopStruct of X2 implies
(D1 is open implies D2 is open);

theorem :: TOPS_3:77
D1 = D2 & the TopStruct of X1 = the TopStruct of X2 implies Int D1 = Int D2;

theorem :: TOPS_3:78
D1 c= D2 & the TopStruct of X1 = the TopStruct of X2 implies Int D1 c= Int D2;

theorem :: TOPS_3:79
D1 = D2 & the TopStruct of X1 = the TopStruct of X2 implies
(D1 is closed implies D2 is closed);

theorem :: TOPS_3:80
D1 = D2 & the TopStruct of X1 = the TopStruct of X2 implies Cl D1 = Cl D2;

theorem :: TOPS_3:81
D1 c= D2 & the TopStruct of X1 = the TopStruct of X2 implies Cl D1 c= Cl D2;

theorem :: TOPS_3:82
D2 c= D1 & the TopStruct of X1 = the TopStruct of X2 implies
(D1 is boundary implies D2 is boundary);

theorem :: TOPS_3:83
D1 c= D2 & the TopStruct of X1 = the TopStruct of X2 implies
(D1 is dense implies D2 is dense);

theorem :: TOPS_3:84
D2 c= D1 & the TopStruct of X1 = the TopStruct of X2 implies
(D1 is nowhere_dense implies D2 is nowhere_dense);

reserve X1,X2 for non empty TopSpace;
reserve D1 for Subset of X1, D2 for Subset of X2;

theorem :: TOPS_3:85
D1 c= D2 & the TopStruct of X1 = the TopStruct of X2 implies
(D1 is everywhere_dense implies D2 is everywhere_dense);

```