:: Remarks on Special Subsets of Topological Spaces :: by Zbigniew Karno :: :: Received April 6, 1993 :: Copyright (c) 1993-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 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);