:: Subsets of Topological Spaces
:: by Miros{\l}aw Wysocki and Agata Darmochwa\l
::
:: Received April 28, 1989
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

theorem :: TOPS_1:1
for TS being 1-sorted
for K, Q being Subset of TS st K ` = Q ` holds
K = Q by SUBSET_1:42;

theorem Th2: :: TOPS_1:2
for GX being TopStruct holds Cl ([#] GX) = [#] GX
proofend;

registration
let T be TopSpace;
let P be Subset of T;
cluster Cl P ->  closed ;
coherence
 Cl P is closed
proofend;
end;

theorem Th3: :: TOPS_1:3
for GX being TopStruct
for R being Subset of GX holds
( R is closed iff R ` is open )
proofend;

registration
let T be TopSpace;
let R be closed Subset of T;
clusterR `  ->  open ;
coherence
 R ` is open by Th3;
end;

theorem Th4: :: TOPS_1:4
for GX being TopStruct
for R being Subset of GX holds
( R is open iff R ` is closed )
proofend;

registration
let T be TopSpace;
cluster open for Element of K10( the carrier of T);
existence
 ex b1 being Subset of T st b1 is open
proofend;
end;

registration
let T be TopSpace;
let R be open Subset of T;
clusterR `  ->  closed ;
coherence
 R ` is closed by Th4;
end;

theorem :: TOPS_1:5
for GX being TopStruct
for S, T being Subset of GX st S is closed & T c= S holds
Cl T c= S
proofend;

theorem Th6: :: TOPS_1:6
for TS being TopSpace
for K, L being Subset of TS holds (Cl K) \ (Cl L) c= Cl (K \ L)
proofend;

theorem Th7: :: TOPS_1:7
for GX being TopStruct
for R, S being Subset of GX st R is closed & S is closed holds
Cl (R /\ S) = (Cl R) /\ (Cl S)
proofend;

registration
let TS be TopSpace;
let P, Q be closed Subset of TS;
clusterP /\ Q ->  closed for Subset of TS;
coherence
 for b1 being Subset of TS st b1 = P /\ Q holds
b1 is closed
proofend;
clusterP \/ Q ->  closed for Subset of TS;
coherence
 for b1 being Subset of TS st b1 = P \/ Q holds
b1 is closed
proofend;
end;

theorem :: TOPS_1:8
for TS being TopSpace
for P, Q being Subset of TS st P is closed & Q is closed holds
P /\ Q is closed ;

theorem :: TOPS_1:9
for TS being TopSpace
for P, Q being Subset of TS st P is closed & Q is closed holds
P \/ Q is closed ;

registration
let TS be TopSpace;
let P, Q be open Subset of TS;
clusterP /\ Q ->  open for Subset of TS;
coherence
 for b1 being Subset of TS st b1 = P /\ Q holds
b1 is open
proofend;
clusterP \/ Q ->  open for Subset of TS;
coherence
 for b1 being Subset of TS st b1 = P \/ Q holds
b1 is open
proofend;
end;

theorem :: TOPS_1:10
for TS being TopSpace
for P, Q being Subset of TS st P is open & Q is open holds
P \/ Q is open ;

theorem :: TOPS_1:11
for TS being TopSpace
for P, Q being Subset of TS st P is open & Q is open holds
P /\ Q is open ;

theorem Th12: :: TOPS_1:12
for GX being non empty TopSpace
for R being Subset of GX
for 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 )
proofend;

theorem Th13: :: TOPS_1:13
for TS being TopSpace
for Q, K being Subset of TS st Q is open holds
Q /\ (Cl K) c= Cl (Q /\ K)
proofend;

theorem :: TOPS_1:14
for TS being TopSpace
for Q, K being Subset of TS st Q is open holds
Cl (Q /\ (Cl K)) = Cl (Q /\ K)
proofend;

::
:: INTERIOR OF A SET
::
definition
let GX be TopStruct ;
let R be Subset of GX;
func Int R ->  Subset of GX equals :: TOPS_1:def 1
(Cl (R `)) ` ;
coherence
 (Cl (R `)) ` is Subset of GX ;
projectivity
 for b1, b2 being Subset of GX st b1 = (Cl (b2 `)) ` holds
b1 = (Cl (b1 `)) ` ;
end;

:: deftheorem  defines Int TOPS_1:def_1_:_
 for GX being TopStruct
for R being Subset of GX holds Int R = (Cl (R `)) ` ;

theorem Th15: :: TOPS_1:15
for TS being TopSpace holds Int ([#] TS) = [#] TS
proofend;

theorem Th16: :: TOPS_1:16
for GX being TopStruct
for T being Subset of GX holds Int T c= T
proofend;

theorem Th17: :: TOPS_1:17
for TS being TopSpace
for K, L being Subset of TS holds (Int K) /\ (Int L) = Int (K /\ L)
proofend;

registration
let GX be TopStruct ;
cluster Int ({} GX) ->  empty ;
coherence
 Int ({} GX) is empty
proofend;
end;

theorem :: TOPS_1:18
for GX being TopStruct holds Int ({} GX) = {} GX ;

theorem Th19: :: TOPS_1:19
for GX being TopStruct
for T, W being Subset of GX st T c= W holds
Int T c= Int W
proofend;

theorem Th20: :: TOPS_1:20
for GX being TopStruct
for T, W being Subset of GX holds (Int T) \/ (Int W) c= Int (T \/ W)
proofend;

theorem :: TOPS_1:21
for TS being TopSpace
for K, L being Subset of TS holds Int (K \ L) c= (Int K) \ (Int L)
proofend;

registration
let T be TopSpace;
let K be Subset of T;
cluster Int K ->  open ;
coherence
 Int K is open ;
end;

registration
let T be TopSpace;
cluster empty  ->  open for Element of K10( the carrier of T);
coherence
 for b1 being Subset of T st b1 is empty holds
b1 is open
proofend;
cluster [#] T ->  open ;
coherence
 [#] T is open
proofend;
end;

registration
let T be TopSpace;
cluster open closed for Element of K10( the carrier of T);
existence
 ex b1 being Subset of T st
( b1 is open & b1 is closed )
proofend;
end;

registration
let T be non empty TopSpace;
cluster non empty open closed for Element of K10( the carrier of T);
existence
 ex b1 being Subset of T st
( not b1 is empty & b1 is open & b1 is closed )
proofend;
end;

theorem Th22: :: TOPS_1:22
for TS being TopSpace
for x being set
for K being Subset of TS holds
( x in Int K iff ex Q being Subset of TS st
( Q is open & Q c= K & x in Q ) )
proofend;

theorem Th23: :: TOPS_1:23
for TS being TopSpace
for GX being TopStruct
for P being Subset of TS
for R being Subset of GX holds
( ( R is open implies Int R = R ) & ( Int P = P implies P is open ) )
proofend;

theorem :: TOPS_1:24
for GX being TopStruct
for S, T being Subset of GX st S is open & S c= T holds
S c= Int T
proofend;

theorem :: TOPS_1:25
for TS being TopSpace
for P being Subset of TS holds
( P is open iff for x being set holds
( x in P iff ex Q being Subset of TS st
( Q is open & Q c= P & x in Q ) ) )
proofend;

theorem Th26: :: TOPS_1:26
for GX being TopStruct
for T being Subset of GX holds Cl (Int T) = Cl (Int (Cl (Int T)))
proofend;

theorem :: TOPS_1:27
for GX being TopStruct
for R being Subset of GX st R is open holds
Cl (Int (Cl R)) = Cl R
proofend;

::
:: FRONTIER OF A SET
::
definition
let GX be TopStruct ;
let R be Subset of GX;
func Fr R ->  Subset of GX equals :: TOPS_1:def 2
(Cl R) /\ (Cl (R `));
coherence
 (Cl R) /\ (Cl (R `)) is Subset of GX ;
end;

:: deftheorem  defines Fr TOPS_1:def_2_:_
 for GX being TopStruct
for R being Subset of GX holds Fr R = (Cl R) /\ (Cl (R `));

registration
let T be TopSpace;
let A be Subset of T;
cluster Fr A ->  closed ;
coherence
 Fr A is closed ;
end;

theorem Th28: :: TOPS_1:28
for GX being non empty TopSpace
for R being Subset of GX
for 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 ) )
proofend;

theorem :: TOPS_1:29
for GX being TopStruct
for T being Subset of GX holds Fr T = Fr (T `) ;

theorem :: TOPS_1:30
for GX being TopStruct
for T being Subset of GX holds Fr T = ((Cl (T `)) /\ T) \/ ((Cl T) \ T)
proofend;

theorem Th31: :: TOPS_1:31
for GX being TopStruct
for T being Subset of GX holds Cl T = T \/ (Fr T)
proofend;

theorem Th32: :: TOPS_1:32
for TS being TopSpace
for K, L being Subset of TS holds Fr (K /\ L) c= (Fr K) \/ (Fr L)
proofend;

theorem Th33: :: TOPS_1:33
for TS being TopSpace
for K, L being Subset of TS holds Fr (K \/ L) c= (Fr K) \/ (Fr L)
proofend;

theorem Th34: :: TOPS_1:34
for GX being TopStruct
for T being Subset of GX holds Fr (Fr T) c= Fr T
proofend;

theorem :: TOPS_1:35
for GX being TopStruct
for R being Subset of GX st R is closed holds
Fr R c= R
proofend;

Lm1:  for TS being TopSpace
for K, L being Subset of TS holds Fr K c= ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L))
proofend;

theorem :: TOPS_1:36
for TS being TopSpace
for K, L being Subset of TS holds (Fr K) \/ (Fr L) = ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L))
proofend;

theorem :: TOPS_1:37
for GX being TopStruct
for T being Subset of GX holds Fr (Int T) c= Fr T
proofend;

theorem :: TOPS_1:38
for GX being TopStruct
for T being Subset of GX holds Fr (Cl T) c= Fr T
proofend;

theorem Th39: :: TOPS_1:39
for GX being TopStruct
for T being Subset of GX holds Int T misses Fr T
proofend;

theorem Th40: :: TOPS_1:40
for GX being TopStruct
for T being Subset of GX holds Int T = T \ (Fr T)
proofend;

Lm2:  for GX being TopStruct
for T being Subset of GX holds Fr T = (Cl T) \ (Int T)
proofend;

Lm3:  for TS being TopSpace
for K being Subset of TS holds Cl (Fr K) = Fr K
proofend;

Lm4:  for TS being TopSpace
for K being Subset of TS holds Int (Fr (Fr K)) = {}
proofend;

theorem :: TOPS_1:41
for TS being TopSpace
for K being Subset of TS holds Fr (Fr (Fr K)) = Fr (Fr K)
proofend;

Lm5:  for X, Y, Z being set st X c= Z & Y = Z \ X holds
X c= Z \ Y
proofend;

theorem Th42: :: TOPS_1:42
for TS being TopSpace
for P being Subset of TS holds
( P is open iff Fr P = (Cl P) \ P )
proofend;

theorem Th43: :: TOPS_1:43
for TS being TopSpace
for P being Subset of TS holds
( P is closed iff Fr P = P \ (Int P) )
proofend;

::
:: DENSE, BOUNDARY AND NOWHEREDENSE SETS
::
definition
let GX be TopStruct ;
let R be Subset of GX;
attrR is dense  means :Def3: :: TOPS_1:def 3
 Cl R = [#] GX;
end;

:: deftheorem Def3 defines dense TOPS_1:def_3_:_
 for GX being TopStruct
for R being Subset of GX holds
( R is dense iff Cl R = [#] GX );

registration
let GX be TopStruct ;
cluster [#] GX ->  dense ;
coherence
 [#] GX is dense
proofend;
cluster dense for Element of K10( the carrier of GX);
existence
 ex b1 being Subset of GX st b1 is dense
proofend;
end;

theorem :: TOPS_1:44
for GX being TopStruct
for R, S being Subset of GX st R is dense & R c= S holds
S is dense
proofend;

theorem Th45: :: TOPS_1:45
for TS being TopSpace
for P being Subset of TS holds
( P is dense iff for Q being Subset of TS st Q <> {} &amp; Q is open holds
P meets Q )
proofend;

theorem Th46: :: TOPS_1:46
for TS being TopSpace
for P being Subset of TS st P is dense holds
for Q being Subset of TS st Q is open holds
Cl Q = Cl (Q /\ P)
proofend;

theorem :: TOPS_1:47
for TS being TopSpace
for P, Q being Subset of TS st P is dense &amp; Q is dense &amp; Q is open holds
P /\ Q is dense
proofend;

definition
let GX be TopStruct ;
let R be Subset of GX;
attrR is boundary  means :Def4: :: TOPS_1:def 4
R ` is dense ;
end;

:: deftheorem Def4 defines boundary TOPS_1:def_4_:_
 for GX being TopStruct
for R being Subset of GX holds
( R is boundary iff R ` is dense );

registration
let GX be TopStruct ;
cluster empty  ->  boundary for Element of K10( the carrier of GX);
coherence
 for b1 being Subset of GX st b1 is empty holds
b1 is boundary
proofend;
end;

theorem Th48: :: TOPS_1:48
for GX being TopStruct
for R being Subset of GX holds
( R is boundary iff Int R = {} )
proofend;

registration
let GX be TopStruct ;
cluster boundary for Element of K10( the carrier of GX);
existence
 ex b1 being Subset of GX st b1 is boundary
proofend;
end;

registration
let GX be TopStruct ;
let R be boundary Subset of GX;
cluster Int R ->  empty ;
coherence
 Int R is empty by Th48;
end;

theorem Th49: :: TOPS_1:49
for TS being TopSpace
for P, Q being Subset of TS st P is boundary &amp; Q is boundary &amp; Q is closed holds
P \/ Q is boundary
proofend;

theorem :: TOPS_1:50
for TS being TopSpace
for P being Subset of TS holds
( P is boundary iff for Q being Subset of TS st Q c= P &amp; Q is open holds
Q = {} )
proofend;

theorem :: TOPS_1:51
for TS being TopSpace
for P being Subset of TS st P is closed holds
( P is boundary iff for Q being Subset of TS st Q <> {} &amp; Q is open holds
ex G being Subset of TS st
( G c= Q &amp; G <> {} &amp; G is open &amp; P misses G ) )
proofend;

theorem :: TOPS_1:52
for GX being TopStruct
for R being Subset of GX holds
( R is boundary iff R c= Fr R )
proofend;

registration
let GX be non empty TopSpace;
cluster [#] GX ->  non boundary ;
coherence
 not [#] GX is boundary
proofend;
cluster non empty non boundary for Element of K10( the carrier of GX);
existence
 ex b1 being Subset of GX st
( not b1 is boundary &amp; not b1 is empty )
proofend;
end;

definition
let GX be TopStruct ;
let R be Subset of GX;
attrR is nowhere_dense  means :Def5: :: TOPS_1:def 5
 Cl R is boundary ;
end;

:: deftheorem Def5 defines nowhere_dense TOPS_1:def_5_:_
 for GX being TopStruct
for R being Subset of GX holds
( R is nowhere_dense iff Cl R is boundary );

registration
let TS be TopSpace;
cluster empty  ->  nowhere_dense for Element of K10( the carrier of TS);
coherence
 for b1 being Subset of TS st b1 is empty holds
b1 is nowhere_dense
proofend;
end;

registration
let TS be TopSpace;
cluster nowhere_dense for Element of K10( the carrier of TS);
existence
 ex b1 being Subset of TS st b1 is nowhere_dense
proofend;
end;

theorem :: TOPS_1:53
for TS being TopSpace
for P, Q being Subset of TS st P is nowhere_dense &amp; Q is nowhere_dense holds
P \/ Q is nowhere_dense
proofend;

theorem Th54: :: TOPS_1:54
for GX being TopStruct
for R being Subset of GX st R is nowhere_dense holds
R ` is dense
proofend;

registration
let TS be TopSpace;
let R be nowhere_dense Subset of TS;
clusterR `  ->  dense ;
coherence
 R ` is dense by Th54;
end;

theorem Th55: :: TOPS_1:55
for GX being TopStruct
for R being Subset of GX st R is nowhere_dense holds
R is boundary
proofend;

registration
let TS be TopSpace;
cluster nowhere_dense  ->  boundary for Element of K10( the carrier of TS);
coherence
 for b1 being Subset of TS st b1 is nowhere_dense holds
b1 is boundary by Th55;
end;

theorem Th56: :: TOPS_1:56
for GX being TopStruct
for S being Subset of GX st S is boundary &amp; S is closed holds
S is nowhere_dense
proofend;

registration
let TS be TopSpace;
cluster closed boundary  ->  nowhere_dense for Element of K10( the carrier of TS);
coherence
 for b1 being Subset of TS st b1 is boundary &amp; b1 is closed holds
b1 is nowhere_dense by Th56;
end;

theorem :: TOPS_1:57
for GX being TopStruct
for R being Subset of GX st R is closed holds
( R is nowhere_dense iff R = Fr R )
proofend;

theorem Th58: :: TOPS_1:58
for TS being TopSpace
for P being Subset of TS st P is open holds
Fr P is nowhere_dense
proofend;

registration
let TS be TopSpace;
let P be open Subset of TS;
cluster Fr P ->  nowhere_dense ;
coherence
 Fr P is nowhere_dense by Th58;
end;

theorem Th59: :: TOPS_1:59
for TS being TopSpace
for P being Subset of TS st P is closed holds
Fr P is nowhere_dense
proofend;

registration
let TS be TopSpace;
let P be closed Subset of TS;
cluster Fr P ->  nowhere_dense ;
coherence
 Fr P is nowhere_dense by Th59;
end;

theorem Th60: :: TOPS_1:60
for TS being TopSpace
for P being Subset of TS st P is open &amp; P is nowhere_dense holds
P = {}
proofend;

registration
let TS be TopSpace;
cluster open nowhere_dense  ->  empty for Element of K10( the carrier of TS);
coherence
 for b1 being Subset of TS st b1 is open &amp; b1 is nowhere_dense holds
b1 is empty by Th60;
end;

::
:: CLOSED AND OPEN DOMAIN, DOMAIN
::
definition
let GX be TopStruct ;
let R be Subset of GX;
attrR is condensed  means :Def6: :: TOPS_1:def 6
( Int (Cl R) c= R &amp; R c= Cl (Int R) );
attrR is closed_condensed  means :Def7: :: TOPS_1:def 7
R = Cl (Int R);
attrR is open_condensed  means :Def8: :: TOPS_1:def 8
R = Int (Cl R);
end;

:: deftheorem Def6 defines condensed TOPS_1:def_6_:_
 for GX being TopStruct
for R being Subset of GX holds
( R is condensed iff ( Int (Cl R) c= R &amp; R c= Cl (Int R) ) );

:: deftheorem Def7 defines closed_condensed TOPS_1:def_7_:_
 for GX being TopStruct
for R being Subset of GX holds
( R is closed_condensed iff R = Cl (Int R) );

:: deftheorem Def8 defines open_condensed TOPS_1:def_8_:_
 for GX being TopStruct
for R being Subset of GX holds
( R is open_condensed iff R = Int (Cl R) );

theorem Th61: :: TOPS_1:61
for GX being TopStruct
for R being Subset of GX holds
( R is open_condensed iff R ` is closed_condensed )
proofend;

theorem Th62: :: TOPS_1:62
for GX being TopStruct
for R being Subset of GX st R is closed_condensed holds
Fr (Int R) = Fr R
proofend;

theorem :: TOPS_1:63
for GX being TopStruct
for R being Subset of GX st R is closed_condensed holds
Fr R c= Cl (Int R)
proofend;

theorem Th64: :: TOPS_1:64
for GX being TopStruct
for R being Subset of GX st R is open_condensed holds
( Fr R = Fr (Cl R) &amp; Fr (Cl R) = (Cl R) \ R )
proofend;

theorem :: TOPS_1:65
for GX being TopStruct
for R being Subset of GX st R is open &amp; R is closed holds
( R is closed_condensed iff R is open_condensed )
proofend;

theorem Th66: :: TOPS_1:66
for TS being TopSpace
for GX being TopStruct
for P being Subset of TS
for R being Subset of GX holds
( ( R is closed &amp; R is condensed implies R is closed_condensed ) &amp; ( P is closed_condensed implies ( P is closed &amp; P is condensed ) ) )
proofend;

theorem :: TOPS_1:67
for TS being TopSpace
for GX being TopStruct
for P being Subset of TS
for R being Subset of GX holds
( ( R is open &amp; R is condensed implies R is open_condensed ) &amp; ( P is open_condensed implies ( P is open &amp; P is condensed ) ) )
proofend;

theorem Th68: :: TOPS_1:68
for TS being TopSpace
for P, Q being Subset of TS st P is closed_condensed &amp; Q is closed_condensed holds
P \/ Q is closed_condensed
proofend;

theorem :: TOPS_1:69
for TS being TopSpace
for P, Q being Subset of TS st P is open_condensed &amp; Q is open_condensed holds
P /\ Q is open_condensed
proofend;

theorem :: TOPS_1:70
for TS being TopSpace
for P being Subset of TS st P is condensed holds
Int (Fr P) = {}
proofend;

theorem :: TOPS_1:71
for GX being TopStruct
for R being Subset of GX st R is condensed holds
( Int R is condensed &amp; Cl R is condensed )
proofend;