The abstract of the Mizar article:

Subsets of Topological Spaces

by

Miroslaw Wysocki, and

Agata Darmochwal

Received April 28, 1989

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;