:: Remarks on Special Subsets of Topological Spaces
:: by Zbigniew Karno
::
:: Received April 6, 1993
:: Copyright (c) 1993-2021 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 PRE_TOPC, SUBSET_1, XBOOLE_0, STRUCT_0, TOPS_1, TARSKI, RCOMP_1,
TOPS_3;
notations TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1,
TSEP_1;
constructors TOPS_1, BORSUK_1, TSEP_1;
registrations PRE_TOPC, TOPS_1, BORSUK_1, TSEP_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 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 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 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 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);