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


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 = {} ) )
proof end;

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 ) ) by XBOOLE_1:37;

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)
proof end;

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)
proof end;

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)
proof end;

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))
proof end;

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) = {}
proof end;

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
proof end;

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

theorem Th11: :: TOPS_3:11
for X being TopSpace
for A, B being Subset of X st B is boundary & A c= B holds
A is boundary by TOPS_1:19, XBOOLE_1:3;

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 & C is closed holds
C = the carrier of X )
proof end;

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 <> {} & G is open holds
A ` meets G )
proof end;

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) )
proof end;

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 :: TOPS_3:def 2
 Cl A = the carrier of X;
compatibility
( A is dense iff Cl A = the carrier of X )
proof end;
end;

:: deftheorem 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 <> {}
proof end;

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 )
proof end;

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 & C is closed holds
C = the carrier of X ) by TOPS_1:5, PRE_TOPC:18;

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) )
proof end;

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 :: TOPS_3:def 3
 Int (Cl A) = {} ;
compatibility
( A is nowhere_dense iff Int (Cl A) = {} ) by Def1, TOPS_1:def 5;
end;

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

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
proof end;

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

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 & C is closed & C is boundary ) )
proof end;

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 <> {} & G is open holds
ex H being Subset of X st
( H c= G & H <> {} & H is open & A misses H ) )
proof end;

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 & B is boundary holds
A \/ B is boundary
proof end;

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

:: deftheorem 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 ) ;
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
proof end;

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

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
proof end;

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

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

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 by PRE_TOPC:22;

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

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 )
proof end;

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 )
proof end;

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 & C is open & C is dense ) )
proof end;

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 & F is closed holds
ex H being Subset of X st
( F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X ) )
proof end;

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 & B is everywhere_dense holds
A /\ B is everywhere_dense
proof end;

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

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

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

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

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 & C is dense & B is nowhere_dense & C \/ B = D & C misses B )
proof end;

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 & C is dense & B is closed & B is boundary & C \/ (D /\ B) = D & C misses B & C \/ B = the carrier of X )
proof end;

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 & C is boundary & B is everywhere_dense & C /\ B = D & C \/ B = the carrier of X )
proof end;

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 & C is boundary & B is open & B is dense & C /\ (D \/ B) = D & C misses B & C \/ B = the carrier of X )
proof end;

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
proof end;

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 & C c= the carrier of Y0 & A c= C & A = B holds
Cl A = Cl B
proof end;

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
proof end;

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
proof end;

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 & C c= the carrier of Y0 & A c= C & A = B holds
Int A = Int B
proof end;

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
proof end;

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 & A is dense holds
B is dense
proof end;

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 & A c= C & A = B holds
( ( C is dense & B is dense ) iff A is dense )
proof end;

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 & A is everywhere_dense holds
B is everywhere_dense
proof end;

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 & C c= the carrier of X0 & A c= C & A = B holds
( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense )
proof end;

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 & A = B holds
( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense )
proof end;

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 & A c= C & A = B holds
( ( C is everywhere_dense & B is everywhere_dense ) iff A is everywhere_dense )
proof end;

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 & B is boundary holds
A is boundary by XBOOLE_1:3, Th56;

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 & C c= the carrier of X0 & A c= C & A = B & A is boundary holds
B is boundary by Th57;

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 )
proof end;

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 & B is nowhere_dense holds
A is nowhere_dense
proof end;

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 & C = the carrier of X0 & A = B & A is nowhere_dense holds
B is nowhere_dense
proof end;

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 & C c= the carrier of X0 & A c= C & A = B & A is nowhere_dense holds
B is nowhere_dense
proof end;

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 )
proof end;

:: 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 ` )
proof end;

theorem Th72: :: TOPS_3:72
for X1, X2 being TopStruct st the carrier of X1 = the carrier of X2 & ( 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 #)
proof end;

theorem Th73: :: TOPS_3:73
for X1, X2 being TopStruct st the carrier of X1 = the carrier of X2 & ( 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 #)
proof end;

theorem :: TOPS_3:74
for X1, X2 being TopSpace st the carrier of X1 = the carrier of X2 & ( 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 #)
proof end;

theorem :: TOPS_3:75
for X1, X2 being TopSpace st the carrier of X1 = the carrier of X2 & ( 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 #)
proof end;

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 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is open holds
D2 is open ;

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 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds
Int D1 = Int D2
proof end;

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 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds
Int D1 c= Int D2
proof end;

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 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is closed holds
D2 is closed by Th76;

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 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds
Cl D1 = Cl D2
proof end;

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 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds
Cl D1 c= Cl D2
proof end;

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 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is boundary holds
D2 is boundary
proof end;

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 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is dense holds
D2 is dense
proof end;

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 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is nowhere_dense holds
D2 is nowhere_dense
proof end;

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 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is everywhere_dense holds
D2 is everywhere_dense
proof end;