Volume 1, 1989

University of Bialystok

Copyright (c) 1989 Association of Mizar Users

### 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;

Back to top