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

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

proof end;

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;

begin

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

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 B, A being Subset of X st B is boundary & A c= B holds
A is boundary

proof end;

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 :Def2: :: 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 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 <> {}

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 )

proof end;

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:79, 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) = {} )

proof end;

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

proof end;

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 B, A 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 :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 )

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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;

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

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

proof end;

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

proof end;

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;

begin

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

proof end;

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

proof end;

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;