:: Remarks on Special Subsets of Topological Spaces
:: by Zbigniew Karno
::
:: Received April 6, 1993
:: Copyright (c) 1993-2012 Association of Mizar Users


begin

theorem Th1: :: TOPS_3:1
for X being TopStruct
for A being Subset of X holds
( ( A = {} X implies A ` = [#] X ) & ( A ` = [#] X implies A = {} X ) & ( A = {} implies A ` = the carrier of X ) & ( A ` = the carrier of X implies A = {} ) )
proofend;

theorem Th2: :: TOPS_3:2
for X being TopStruct
for A being Subset of X holds
( ( A = [#] X implies A ` = {} X ) & ( A ` = {} X implies A = [#] X ) & ( A = the carrier of X implies A ` = {} ) & ( A ` = {} implies A = the carrier of X ) )
proofend;

theorem Th3: :: TOPS_3:3
for X being TopSpace
for A, B being Subset of X holds (Int A) /\ (Cl B) c= Cl (A /\ B)
proofend;

theorem Th4: :: TOPS_3:4
for X being TopSpace
for A, B being Subset of X holds Int (A \/ B) c= (Cl A) \/ (Int B)
proofend;

theorem Th5: :: TOPS_3:5
for X being TopSpace
for B, A being Subset of X st A is closed holds
Int (A \/ B) c= A \/ (Int B)
proofend;

theorem Th6: :: TOPS_3:6
for X being TopSpace
for B, A being Subset of X st A is closed holds
Int (A \/ B) = Int (A \/ (Int B))
proofend;

theorem Th7: :: TOPS_3:7
for X being TopSpace
for A being Subset of X st A misses Int (Cl A) holds
Int (Cl A) = {}
proofend;

theorem :: TOPS_3:8
for X being TopSpace
for A being Subset of X st A \/ (Cl (Int A)) = the carrier of X holds
Cl (Int A) = the carrier of X
proofend;

begin

:: 2. Special Subsets of a Topological Space.
definition
let X be TopStruct ;
let A be Subset of X;
redefine attr A is boundary  means :Def1: :: TOPS_3:def 1
 Int A = {} ;
compatibility
 ( A is boundary iff Int A = {} ) by TOPS_1:48;
end;

:: deftheorem Def1 defines boundary TOPS_3:def_1_:_
 for X being TopStruct
for A being Subset of X holds
( A is boundary iff Int A = {} );

theorem :: TOPS_3:9
for X being TopSpace holds {} X is boundary ;

theorem Th10: :: TOPS_3:10
for X being non empty TopSpace
for A being Subset of X st A is boundary holds
A <> the carrier of X
proofend;

theorem Th11: :: TOPS_3:11
for X being TopSpace
for B, A being Subset of X st B is boundary &amp; A c= B holds
A is boundary
proofend;

theorem :: TOPS_3:12
for X being TopSpace
for A being Subset of X holds
( A is boundary iff for C being Subset of X st A ` c= C &amp; C is closed holds
C = the carrier of X )
proofend;

theorem :: TOPS_3:13
for X being TopSpace
for A being Subset of X holds
( A is boundary iff for G being Subset of X st G <> {} &amp; G is open holds
A ` meets G )
proofend;

theorem :: TOPS_3:14
for X being TopSpace
for A being Subset of X holds
( A is boundary iff for F being Subset of X st F is closed holds
Int F = Int (F \/ A) )
proofend;

theorem :: TOPS_3:15
for X being TopSpace
for A, B being Subset of X st A is boundary holds
A /\ B is boundary by Th11, XBOOLE_1:17;

definition
let X be TopStruct ;
let A be Subset of X;
redefine attr A is dense  means :Def2: :: TOPS_3:def 2
 Cl A = the carrier of X;
compatibility
 ( A is dense iff Cl A = the carrier of X )
proofend;
end;

:: deftheorem Def2 defines dense TOPS_3:def_2_:_
 for X being TopStruct
for A being Subset of X holds
( A is dense iff Cl A = the carrier of X );

theorem :: TOPS_3:16
for X being TopSpace holds [#] X is dense ;

theorem Th17: :: TOPS_3:17
for X being non empty TopSpace
for A being Subset of X st A is dense holds
A <> {}
proofend;

theorem Th18: :: TOPS_3:18
for X being non empty TopSpace
for A being Subset of X holds
( A is dense iff A ` is boundary )
proofend;

theorem :: TOPS_3:19
for X being non empty TopSpace
for A being Subset of X holds
( A is dense iff for C being Subset of X st A c= C &amp; C is closed holds
C = the carrier of X )
proofend;

theorem :: TOPS_3:20
for X being non empty TopSpace
for A being Subset of X holds
( A is dense iff for G being Subset of X st G is open holds
Cl G = Cl (G /\ A) )
proofend;

theorem :: TOPS_3:21
for X being non empty TopSpace
for A, B being Subset of X st A is dense holds
A \/ B is dense by TOPS_1:44, XBOOLE_1:7;

definition
let X be TopStruct ;
let A be Subset of X;
redefine attr A is nowhere_dense  means :Def3: :: TOPS_3:def 3
 Int (Cl A) = {} ;
compatibility
 ( A is nowhere_dense iff Int (Cl A) = {} )
proofend;
end;

:: deftheorem Def3 defines nowhere_dense TOPS_3:def_3_:_
 for X being TopStruct
for A being Subset of X holds
( A is nowhere_dense iff Int (Cl A) = {} );

theorem :: TOPS_3:22
for X being non empty TopSpace holds {} X is nowhere_dense ;

theorem :: TOPS_3:23
for X being non empty TopSpace
for A being Subset of X st A is nowhere_dense holds
A <> the carrier of X by Th10;

theorem :: TOPS_3:24
for X being non empty TopSpace
for A being Subset of X st A is nowhere_dense holds
Cl A is nowhere_dense
proofend;

theorem :: TOPS_3:25
for X being non empty TopSpace
for A being Subset of X st A is nowhere_dense holds
not A is dense
proofend;

theorem Th26: :: TOPS_3:26
for X being non empty TopSpace
for B, A being Subset of X st B is nowhere_dense &amp; A c= B holds
A is nowhere_dense
proofend;

theorem Th27: :: TOPS_3:27
for X being non empty TopSpace
for A being Subset of X holds
( A is nowhere_dense iff ex C being Subset of X st
( A c= C &amp; C is closed &amp; C is boundary ) )
proofend;

theorem Th28: :: TOPS_3:28
for X being non empty TopSpace
for A being Subset of X holds
( A is nowhere_dense iff for G being Subset of X st G <> {} &amp; G is open holds
ex H being Subset of X st
( H c= G &amp; H <> {} &amp; H is open &amp; A misses H ) )
proofend;

theorem :: TOPS_3:29
for X being non empty TopSpace
for A, B being Subset of X st A is nowhere_dense holds
A /\ B is nowhere_dense by Th26, XBOOLE_1:17;

theorem Th30: :: TOPS_3:30
for X being non empty TopSpace
for A, B being Subset of X st A is nowhere_dense &amp; B is boundary holds
A \/ B is boundary
proofend;

definition
let X be TopStruct ;
let A be Subset of X;
attrA is everywhere_dense  means :Def4: :: TOPS_3:def 4
 Cl (Int A) = [#] X;
end;

:: deftheorem Def4 defines everywhere_dense TOPS_3:def_4_:_
 for X being TopStruct
for A being Subset of X holds
( A is everywhere_dense iff Cl (Int A) = [#] X );

definition
let X be TopStruct ;
let A be Subset of X;
redefine attr A is everywhere_dense  means :: TOPS_3:def 5
 Cl (Int A) = the carrier of X;
compatibility
 ( A is everywhere_dense iff Cl (Int A) = the carrier of X )
proofend;
end;

:: deftheorem  defines everywhere_dense TOPS_3:def_5_:_
 for X being TopStruct
for A being Subset of X holds
( A is everywhere_dense iff Cl (Int A) = the carrier of X );

theorem :: TOPS_3:31
for X being non empty TopSpace holds [#] X is everywhere_dense
proofend;

theorem Th32: :: TOPS_3:32
for X being non empty TopSpace
for A being Subset of X st A is everywhere_dense holds
Int A is everywhere_dense
proofend;

theorem Th33: :: TOPS_3:33
for X being non empty TopSpace
for A being Subset of X st A is everywhere_dense holds
A is dense
proofend;

theorem :: TOPS_3:34
for X being non empty TopSpace
for A being Subset of X st A is everywhere_dense holds
A <> {} by Th17, Th33;

theorem Th35: :: TOPS_3:35
for X being non empty TopSpace
for A being Subset of X holds
( A is everywhere_dense iff Int A is dense )
proofend;

theorem Th36: :: TOPS_3:36
for X being non empty TopSpace
for A being Subset of X st A is open &amp; A is dense holds
A is everywhere_dense
proofend;

theorem :: TOPS_3:37
for X being non empty TopSpace
for A being Subset of X st A is everywhere_dense holds
not A is boundary
proofend;

theorem Th38: :: TOPS_3:38
for X being non empty TopSpace
for A, B being Subset of X st A is everywhere_dense &amp; A c= B holds
B is everywhere_dense
proofend;

theorem Th39: :: TOPS_3:39
for X being non empty TopSpace
for A being Subset of X holds
( A is everywhere_dense iff A ` is nowhere_dense )
proofend;

theorem Th40: :: TOPS_3:40
for X being non empty TopSpace
for A being Subset of X holds
( A is nowhere_dense iff A ` is everywhere_dense )
proofend;

theorem Th41: :: TOPS_3:41
for X being non empty TopSpace
for A being Subset of X holds
( A is everywhere_dense iff ex C being Subset of X st
( C c= A &amp; C is open &amp; C is dense ) )
proofend;

theorem :: TOPS_3:42
for X being non empty TopSpace
for A being Subset of X holds
( A is everywhere_dense iff for F being Subset of X st F <> the carrier of X &amp; F is closed holds
ex H being Subset of X st
( F c= H &amp; H <> the carrier of X &amp; H is closed &amp; A \/ H = the carrier of X ) )
proofend;

theorem :: TOPS_3:43
for X being non empty TopSpace
for A, B being Subset of X st A is everywhere_dense holds
A \/ B is everywhere_dense by Th38, XBOOLE_1:7;

theorem Th44: :: TOPS_3:44
for X being non empty TopSpace
for A, B being Subset of X st A is everywhere_dense &amp; B is everywhere_dense holds
A /\ B is everywhere_dense
proofend;

theorem Th45: :: TOPS_3:45
for X being non empty TopSpace
for A, B being Subset of X st A is everywhere_dense &amp; B is dense holds
A /\ B is dense
proofend;

theorem :: TOPS_3:46
for X being non empty TopSpace
for A, B being Subset of X st A is dense &amp; B is nowhere_dense holds
A \ B is dense
proofend;

theorem :: TOPS_3:47
for X being non empty TopSpace
for A, B being Subset of X st A is everywhere_dense &amp; B is boundary holds
A \ B is dense
proofend;

theorem :: TOPS_3:48
for X being non empty TopSpace
for A, B being Subset of X st A is everywhere_dense &amp; B is nowhere_dense holds
A \ B is everywhere_dense
proofend;

theorem :: TOPS_3:49
for X being non empty TopSpace
for D being Subset of X st D is everywhere_dense holds
ex C, B being Subset of X st
( C is open &amp; C is dense &amp; B is nowhere_dense &amp; C \/ B = D &amp; C misses B )
proofend;

theorem :: TOPS_3:50
for X being non empty TopSpace
for D being Subset of X st D is everywhere_dense holds
ex C, B being Subset of X st
( C is open &amp; C is dense &amp; B is closed &amp; B is boundary &amp; C \/ (D /\ B) = D &amp; C misses B &amp; C \/ B = the carrier of X )
proofend;

theorem :: TOPS_3:51
for X being non empty TopSpace
for D being Subset of X st D is nowhere_dense holds
ex C, B being Subset of X st
( C is closed &amp; C is boundary &amp; B is everywhere_dense &amp; C /\ B = D &amp; C \/ B = the carrier of X )
proofend;

theorem :: TOPS_3:52
for X being non empty TopSpace
for D being Subset of X st D is nowhere_dense holds
ex C, B being Subset of X st
( C is closed &amp; C is boundary &amp; B is open &amp; B is dense &amp; C /\ (D \/ B) = D &amp; C misses B &amp; C \/ B = the carrier of X )
proofend;

begin

theorem Th53: :: TOPS_3:53
for X being non empty TopSpace
for Y0 being SubSpace of X
for A being Subset of X
for B being Subset of Y0 st B c= A holds
Cl B c= Cl A
proofend;

theorem Th54: :: TOPS_3:54
for X being non empty TopSpace
for Y0 being SubSpace of X
for C, A being Subset of X
for B being Subset of Y0 st C is closed &amp; C c= the carrier of Y0 &amp; A c= C &amp; A = B holds
Cl A = Cl B
proofend;

theorem :: TOPS_3:55
for X being non empty TopSpace
for Y0 being non empty closed SubSpace of X
for A being Subset of X
for B being Subset of Y0 st A = B holds
Cl A = Cl B
proofend;

theorem Th56: :: TOPS_3:56
for X being non empty TopSpace
for Y0 being SubSpace of X
for A being Subset of X
for B being Subset of Y0 st A c= B holds
Int A c= Int B
proofend;

theorem Th57: :: TOPS_3:57
for X being non empty TopSpace
for Y0 being non empty SubSpace of X
for C, A being Subset of X
for B being Subset of Y0 st C is open &amp; C c= the carrier of Y0 &amp; A c= C &amp; A = B holds
Int A = Int B
proofend;

theorem :: TOPS_3:58
for X being non empty TopSpace
for Y0 being non empty open SubSpace of X
for A being Subset of X
for B being Subset of Y0 st A = B holds
Int A = Int B
proofend;

theorem Th59: :: TOPS_3:59
for X being non empty TopSpace
for X0 being SubSpace of X
for A being Subset of X
for B being Subset of X0 st A c= B &amp; A is dense holds
B is dense
proofend;

theorem Th60: :: TOPS_3:60
for X being non empty TopSpace
for X0 being SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C c= the carrier of X0 &amp; A c= C &amp; A = B holds
( ( C is dense &amp; B is dense ) iff A is dense )
proofend;

theorem Th61: :: TOPS_3:61
for X being non empty TopSpace
for X0 being non empty SubSpace of X
for A being Subset of X
for B being Subset of X0 st A c= B &amp; A is everywhere_dense holds
B is everywhere_dense
proofend;

theorem Th62: :: TOPS_3:62
for X being non empty TopSpace
for X0 being non empty SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C is open &amp; C c= the carrier of X0 &amp; A c= C &amp; A = B holds
( ( C is dense &amp; B is everywhere_dense ) iff A is everywhere_dense )
proofend;

theorem :: TOPS_3:63
for X being non empty TopSpace
for X0 being non empty open SubSpace of X
for A, C being Subset of X
for B being Subset of X0 st C = the carrier of X0 &amp; A = B holds
( ( C is dense &amp; B is everywhere_dense ) iff A is everywhere_dense )
proofend;

theorem :: TOPS_3:64
for X being non empty TopSpace
for X0 being non empty SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C c= the carrier of X0 &amp; A c= C &amp; A = B holds
( ( C is everywhere_dense &amp; B is everywhere_dense ) iff A is everywhere_dense )
proofend;

theorem Th65: :: TOPS_3:65
for X being non empty TopSpace
for X0 being non empty SubSpace of X
for A being Subset of X
for B being Subset of X0 st A c= B &amp; B is boundary holds
A is boundary
proofend;

theorem Th66: :: TOPS_3:66
for X being non empty TopSpace
for X0 being non empty SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C is open &amp; C c= the carrier of X0 &amp; A c= C &amp; A = B &amp; A is boundary holds
B is boundary
proofend;

theorem :: TOPS_3:67
for X being non empty TopSpace
for X0 being non empty open SubSpace of X
for A being Subset of X
for B being Subset of X0 st A = B holds
( A is boundary iff B is boundary )
proofend;

theorem Th68: :: TOPS_3:68
for X being non empty TopSpace
for X0 being non empty SubSpace of X
for A being Subset of X
for B being Subset of X0 st A c= B &amp; B is nowhere_dense holds
A is nowhere_dense
proofend;

Lm1:  for X being non empty TopSpace
for X0 being non empty SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C is open &amp; C = the carrier of X0 &amp; A = B &amp; A is nowhere_dense holds
B is nowhere_dense
proofend;

theorem Th69: :: TOPS_3:69
for X being non empty TopSpace
for X0 being non empty SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C is open &amp; C c= the carrier of X0 &amp; A c= C &amp; A = B &amp; A is nowhere_dense holds
B is nowhere_dense
proofend;

theorem :: TOPS_3:70
for X being non empty TopSpace
for X0 being non empty open SubSpace of X
for A being Subset of X
for B being Subset of X0 st A = B holds
( A is nowhere_dense iff B is nowhere_dense )
proofend;

begin

:: 4. Subsets in Topological Spaces with the same Topological Structures.
theorem :: TOPS_3:71
for X1, X2 being 1-sorted st the carrier of X1 = the carrier of X2 holds
for C1 being Subset of X1
for C2 being Subset of X2 holds
( C1 = C2 iff C1 ` = C2 ` )
proofend;

theorem Th72: :: TOPS_3:72
for X1, X2 being TopStruct st the carrier of X1 = the carrier of X2 &amp; ( for C1 being Subset of X1
for C2 being Subset of X2 st C1 = C2 holds
( C1 is open iff C2 is open ) ) holds
TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)
proofend;

theorem Th73: :: TOPS_3:73
for X1, X2 being TopStruct st the carrier of X1 = the carrier of X2 &amp; ( for C1 being Subset of X1
for C2 being Subset of X2 st C1 = C2 holds
( C1 is closed iff C2 is closed ) ) holds
TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)
proofend;

theorem :: TOPS_3:74
for X1, X2 being TopSpace st the carrier of X1 = the carrier of X2 &amp; ( for C1 being Subset of X1
for C2 being Subset of X2 st C1 = C2 holds
Int C1 = Int C2 ) holds
TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)
proofend;

theorem :: TOPS_3:75
for X1, X2 being TopSpace st the carrier of X1 = the carrier of X2 &amp; ( for C1 being Subset of X1
for C2 being Subset of X2 st C1 = C2 holds
Cl C1 = Cl C2 ) holds
TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)
proofend;

theorem Th76: :: TOPS_3:76
for X1, X2 being TopSpace
for D1 being Subset of X1
for D2 being Subset of X2 st D1 = D2 &amp; TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) &amp; D1 is open holds
D2 is open
proofend;

theorem Th77: :: TOPS_3:77
for X1, X2 being TopSpace
for D1 being Subset of X1
for D2 being Subset of X2 st D1 = D2 &amp; TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds
Int D1 = Int D2
proofend;

theorem Th78: :: TOPS_3:78
for X1, X2 being TopSpace
for D1 being Subset of X1
for D2 being Subset of X2 st D1 c= D2 &amp; TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds
Int D1 c= Int D2
proofend;

theorem Th79: :: TOPS_3:79
for X1, X2 being TopSpace
for D1 being Subset of X1
for D2 being Subset of X2 st D1 = D2 &amp; TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) &amp; D1 is closed holds
D2 is closed
proofend;

theorem Th80: :: TOPS_3:80
for X1, X2 being TopSpace
for D1 being Subset of X1
for D2 being Subset of X2 st D1 = D2 &amp; TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds
Cl D1 = Cl D2
proofend;

theorem Th81: :: TOPS_3:81
for X1, X2 being TopSpace
for D1 being Subset of X1
for D2 being Subset of X2 st D1 c= D2 &amp; TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds
Cl D1 c= Cl D2
proofend;

theorem Th82: :: TOPS_3:82
for X1, X2 being TopSpace
for D1 being Subset of X1
for D2 being Subset of X2 st D2 c= D1 &amp; TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) &amp; D1 is boundary holds
D2 is boundary
proofend;

theorem Th83: :: TOPS_3:83
for X1, X2 being TopSpace
for D1 being Subset of X1
for D2 being Subset of X2 st D1 c= D2 &amp; TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) &amp; D1 is dense holds
D2 is dense
proofend;

theorem :: TOPS_3:84
for X1, X2 being TopSpace
for D1 being Subset of X1
for D2 being Subset of X2 st D2 c= D1 &amp; TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) &amp; D1 is nowhere_dense holds
D2 is nowhere_dense
proofend;

theorem :: TOPS_3:85
for X1, X2 being non empty TopSpace
for D1 being Subset of X1
for D2 being Subset of X2 st D1 c= D2 &amp; TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) &amp; D1 is everywhere_dense holds
D2 is everywhere_dense
proofend;