:: Subsets of Topological Spaces
:: by Miros{\l}aw Wysocki and Agata Darmochwa\l
::
:: Received April 28, 1989
:: Copyright (c) 1990-2018 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 STRUCT_0, SUBSET_1, PRE_TOPC, XBOOLE_0, RCOMP_1, TARSKI, TOPS_1;
notations TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC;
constructors SETFAM_1, PRE_TOPC;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC;
requirements BOOLE, SUBSET;
begin
reserve TS for 1-sorted,
K, Q for Subset of TS;
theorem :: TOPS_1:1
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:2
Cl([#] GX) = [#] GX;
registration
let T be TopSpace, P be Subset of T;
cluster Cl P -> closed;
end;
theorem :: TOPS_1:3
R is closed iff R` is open;
registration
let T be TopSpace, R be closed Subset of T;
cluster R` -> open;
end;
theorem :: TOPS_1:4
R is open iff R` is closed;
registration
let T be TopSpace;
cluster open for Subset of T;
end;
registration
let T be TopSpace, R be open Subset of T;
cluster R` -> closed;
end;
theorem :: TOPS_1:5
S is closed & T c= S implies Cl T c= S;
theorem :: TOPS_1:6
Cl K \ Cl L c= Cl(K \ L);
theorem :: TOPS_1:7
R is closed & S is closed implies Cl(R /\ S) = Cl R /\ Cl S;
registration
let TS;
let P,Q be closed Subset of TS;
cluster P /\ Q -> closed for Subset of TS;
cluster P \/ Q -> closed for Subset of TS;
end;
theorem :: TOPS_1:8
P is closed & Q is closed implies P /\ Q is closed;
theorem :: TOPS_1:9
P is closed & Q is closed implies P \/ Q is closed;
registration
let TS;
let P,Q be open Subset of TS;
cluster P /\ Q -> open for Subset of TS;
cluster P \/ Q -> open for Subset of TS;
end;
theorem :: TOPS_1:10
P is open & Q is open implies P \/ Q is open;
theorem :: TOPS_1:11
P is open & Q is open implies P /\ Q is open;
theorem :: TOPS_1:12
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:13
Q is open implies Q /\ Cl K c= Cl(Q /\ K);
theorem :: TOPS_1:14
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`)`;
projectivity;
end;
theorem :: TOPS_1:15
Int([#] TS) = [#] TS;
theorem :: TOPS_1:16
Int T c= T;
theorem :: TOPS_1:17
Int K /\ Int L = Int(K /\ L);
registration
let GX;
cluster Int {}GX -> empty;
end;
theorem :: TOPS_1:18
Int({} GX) = {} GX;
theorem :: TOPS_1:19
T c= W implies Int T c= Int W;
theorem :: TOPS_1:20
Int T \/ Int W c= Int(T \/ W);
theorem :: TOPS_1:21
Int(K \ L) c= Int K \ Int L;
registration
let T be TopSpace, K be Subset of T;
cluster Int K -> open;
end;
registration
let T be TopSpace;
cluster empty -> open for Subset of T;
cluster [#]T -> open;
end;
registration
let T be TopSpace;
cluster open closed for Subset of T;
end;
registration
let T be non empty TopSpace;
cluster non empty open closed for Subset of T;
end;
theorem :: TOPS_1:22
x in Int K iff ex Q st Q is open & Q c= K & x in Q;
theorem :: TOPS_1:23
(R is open implies Int R = R) & (Int P = P implies P is open);
theorem :: TOPS_1:24
S is open & S c= T implies S c= Int T;
theorem :: TOPS_1:25
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:26
Cl Int T = Cl Int Cl Int T;
theorem :: TOPS_1:27
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;
registration
let T be TopSpace, A be Subset of T;
cluster Fr A -> closed;
end;
theorem :: TOPS_1:28
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:29
Fr T = Fr T`;
theorem :: TOPS_1:30
Fr T = Cl(T`) /\ T \/ (Cl T \ T);
theorem :: TOPS_1:31
Cl T = T \/ Fr T;
theorem :: TOPS_1:32
Fr(K /\ L) c= Fr K \/ Fr L;
theorem :: TOPS_1:33
Fr(K \/ L) c= Fr K \/ Fr L;
theorem :: TOPS_1:34
Fr Fr T c= Fr T;
theorem :: TOPS_1:35
R is closed implies Fr R c= R;
theorem :: TOPS_1:36
Fr K \/ Fr L = Fr(K \/ L) \/ Fr(K /\ L) \/ (Fr K /\ Fr L);
theorem :: TOPS_1:37
Fr Int T c= Fr T;
theorem :: TOPS_1:38
Fr Cl T c= Fr T;
theorem :: TOPS_1:39
Int T misses Fr T;
theorem :: TOPS_1:40
Int T = T \ Fr T;
theorem :: TOPS_1:41
Fr Fr Fr K = Fr Fr K;
theorem :: TOPS_1:42
P is open iff Fr P = Cl P \ P;
theorem :: TOPS_1:43
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;
registration
let GX;
cluster [#]GX -> dense;
cluster dense for Subset of GX;
end;
theorem :: TOPS_1:44
R is dense & R c= S implies S is dense;
theorem :: TOPS_1:45
P is dense iff for Q st Q <> {} & Q is open holds P meets Q;
theorem :: TOPS_1:46
P is dense implies for Q holds Q is open implies Cl Q = Cl(Q /\ P);
theorem :: TOPS_1:47
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;
registration
let GX;
cluster empty -> boundary for Subset of GX;
end;
theorem :: TOPS_1:48
R is boundary iff Int R = {};
registration
let GX;
cluster boundary for Subset of GX;
end;
registration
let GX;
let R be boundary Subset of GX;
cluster Int R -> empty;
end;
theorem :: TOPS_1:49
P is boundary & Q is boundary & Q is closed implies P \/ Q is boundary;
theorem :: TOPS_1:50
P is boundary iff for Q st Q c= P & Q is open holds Q = {};
theorem :: TOPS_1:51
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:52
R is boundary iff R c= Fr R;
registration
let GX be non empty TopSpace;
cluster [#]GX -> non boundary;
cluster non boundary non empty for Subset of GX;
end;
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;
registration
let TS;
cluster empty -> nowhere_dense for Subset of TS;
end;
registration
let TS;
cluster nowhere_dense for Subset of TS;
end;
theorem :: TOPS_1:53
P is nowhere_dense & Q is nowhere_dense implies P \/ Q is nowhere_dense;
theorem :: TOPS_1:54
R is nowhere_dense implies R` is dense;
registration
let TS;
let R be nowhere_dense Subset of TS;
cluster R` -> dense;
end;
theorem :: TOPS_1:55
R is nowhere_dense implies R is boundary;
registration
let TS;
cluster nowhere_dense -> boundary for Subset of TS;
end;
theorem :: TOPS_1:56
S is boundary & S is closed implies S is nowhere_dense;
registration
let TS;
cluster boundary closed -> nowhere_dense for Subset of TS;
end;
theorem :: TOPS_1:57
R is closed implies (R is nowhere_dense iff R = Fr R);
theorem :: TOPS_1:58
P is open implies Fr P is nowhere_dense;
registration
let TS;
let P be open Subset of TS;
cluster Fr P -> nowhere_dense;
end;
theorem :: TOPS_1:59
P is closed implies Fr P is nowhere_dense;
registration
let TS;
let P be closed Subset of TS;
cluster Fr P -> nowhere_dense;
end;
theorem :: TOPS_1:60
P is open & P is nowhere_dense implies P = {};
registration
let TS;
cluster open nowhere_dense -> empty for Subset of TS;
end;
::
:: 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;
theorem :: TOPS_1:61
R is open_condensed iff R` is closed_condensed;
theorem :: TOPS_1:62
R is closed_condensed implies Fr Int R = Fr R;
theorem :: TOPS_1:63
R is closed_condensed implies Fr R c= Cl Int R;
theorem :: TOPS_1:64
R is open_condensed implies Fr R = Fr Cl R & Fr Cl R = Cl R \ R;
theorem :: TOPS_1:65
R is open & R is closed implies (R is closed_condensed iff R is
open_condensed);
theorem :: TOPS_1:66
(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:67
(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:68
P is closed_condensed & Q is closed_condensed implies P \/ Q is
closed_condensed;
theorem :: TOPS_1:69
P is open_condensed & Q is open_condensed implies P /\ Q is open_condensed;
theorem :: TOPS_1:70
P is condensed implies Int Fr P = {};
theorem :: TOPS_1:71
R is condensed implies Int R is condensed & Cl R is condensed;