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