:: On Discrete and Almost Discrete Topological Spaces
:: by Zbigniew Karno
::
:: Received April 6, 1993
:: Copyright (c) 1993-2012 Association of Mizar Users


begin

theorem Th1: :: TEX_1:1
for X being non empty TopSpace
for D, B being Subset of X
for C being Subset of (X modified_with_respect_to D) st B = C & B is open holds
C is open
proofend;

theorem :: TEX_1:2
for X being non empty TopSpace
for D, B being Subset of X
for C being Subset of (X modified_with_respect_to D) st B = C & B is closed holds
C is closed
proofend;

theorem Th3: :: TEX_1:3
for X being non empty TopSpace
for D being Subset of X
for C being Subset of (X modified_with_respect_to (D `)) st C = D holds
C is closed
proofend;

theorem Th4: :: TEX_1:4
for X being non empty TopSpace
for D being Subset of X
for C being Subset of (X modified_with_respect_to D) st C = D & D is dense holds
( C is dense & C is open )
proofend;

theorem Th5: :: TEX_1:5
for X being non empty TopSpace
for D being Subset of X
for C being Subset of (X modified_with_respect_to D) st D c= C & D is dense holds
C is everywhere_dense
proofend;

theorem Th6: :: TEX_1:6
for X being non empty TopSpace
for D being Subset of X
for C being Subset of (X modified_with_respect_to (D `)) st C = D & D is boundary holds
( C is boundary & C is closed )
proofend;

theorem Th7: :: TEX_1:7
for X being non empty TopSpace
for D being Subset of X
for C being Subset of (X modified_with_respect_to (D `)) st C c= D & D is boundary holds
C is nowhere_dense
proofend;

Lm1:  for X, Y being set holds
( X c= Y iff X is Subset of Y )
;

begin

:: 2. Trivial Topological Spaces.
definition
let Y be non empty 1-sorted ;
redefine attr Y is trivial  means :Def1: :: TEX_1:def 1
 ex d being Element of Y st the carrier of Y = {d};
compatibility
 ( Y is trivial iff ex d being Element of Y st the carrier of Y = {d} )
proofend;
end;

:: deftheorem Def1 defines trivial TEX_1:def_1_:_
 for Y being non empty 1-sorted holds
( Y is trivial iff ex d being Element of Y st the carrier of Y = {d} );

registration
cluster1 -element strict for TopStruct ;
existence
 ex b1 being TopStruct st
( b1 is 1 -element & b1 is strict )
proofend;
cluster non trivial strict for TopStruct ;
existence
 ex b1 being TopStruct st
( not b1 is trivial & b1 is strict )
proofend;
end;

theorem :: TEX_1:8
for Y being 1 -element TopStruct st not the topology of Y is empty & Y is almost_discrete holds
Y is TopSpace-like
proofend;

registration
cluster1 -element strict TopSpace-like for TopStruct ;
existence
 ex b1 being TopSpace st
( b1 is 1 -element & b1 is strict )
proofend;
end;

registration
cluster1 -element TopSpace-like  -> 1 -element discrete anti-discrete for TopStruct ;
coherence
 for b1 being 1 -element TopSpace holds
( b1 is anti-discrete & b1 is discrete )
proofend;
cluster non empty TopSpace-like discrete anti-discrete  ->  non empty trivial for TopStruct ;
coherence
 for b1 being non empty TopSpace st b1 is discrete & b1 is anti-discrete holds
b1 is trivial
proofend;
end;

registration
cluster non trivial strict TopSpace-like for TopStruct ;
existence
 ex b1 being TopSpace st
( not b1 is trivial & b1 is strict )
proofend;
end;

registration
cluster non empty TopSpace-like non discrete  ->  non empty non trivial for TopStruct ;
coherence
 for b1 being non empty TopSpace st not b1 is discrete holds
not b1 is trivial
proofend;
cluster non empty TopSpace-like non anti-discrete  ->  non empty non trivial for TopStruct ;
coherence
 for b1 being non empty TopSpace st not b1 is anti-discrete holds
not b1 is trivial
proofend;
end;

begin

:: 3. Examples of Discrete and Anti-discrete Topological Spaces.
definition
let D be set ;
func cobool D ->  Subset-Family of D equals :: TEX_1:def 2
{{},D};
coherence
 {{},D} is Subset-Family of D
proofend;
end;

:: deftheorem  defines cobool TEX_1:def_2_:_
 for D being set holds cobool D = {{},D};

registration
let D be set ;
cluster cobool D ->  non empty ;
coherence
 not cobool D is empty ;
end;

definition
let D be set ;
func ADTS D ->  TopStruct  equals :: TEX_1:def 3
 TopStruct(# D,(cobool D) #);
coherence
 TopStruct(# D,(cobool D) #) is TopStruct ;
end;

:: deftheorem  defines ADTS TEX_1:def_3_:_
 for D being set holds ADTS D = TopStruct(# D,(cobool D) #);

registration
let D be set ;
cluster ADTS D ->  strict TopSpace-like anti-discrete ;
coherence
 ( ADTS D is strict & ADTS D is anti-discrete & ADTS D is TopSpace-like )
proofend;
end;

registration
let D be non empty set ;
cluster ADTS D ->  non empty ;
coherence
 not ADTS D is empty ;
end;

theorem Th9: :: TEX_1:9
for X being non empty anti-discrete TopSpace
for A being Subset of X holds
( ( A is empty implies Cl A = {} ) & ( not A is empty implies Cl A = the carrier of X ) )
proofend;

theorem Th10: :: TEX_1:10
for X being non empty anti-discrete TopSpace
for A being Subset of X holds
( ( A <> the carrier of X implies Int A = {} ) &amp; ( A = the carrier of X implies Int A = the carrier of X ) )
proofend;

theorem Th11: :: TEX_1:11
for X being non empty TopSpace st ( for A being Subset of X st not A is empty holds
Cl A = the carrier of X ) holds
X is anti-discrete
proofend;

theorem Th12: :: TEX_1:12
for X being non empty TopSpace st ( for A being Subset of X st A <> the carrier of X holds
Int A = {} ) holds
X is anti-discrete
proofend;

theorem :: TEX_1:13
for X being non empty anti-discrete TopSpace
for A being Subset of X holds
( ( A <> {} implies A is dense ) &amp; ( A <> the carrier of X implies A is boundary ) )
proofend;

theorem :: TEX_1:14
for X being non empty TopSpace st ( for A being Subset of X st A <> {} holds
A is dense ) holds
X is anti-discrete
proofend;

theorem :: TEX_1:15
for X being non empty TopSpace st ( for A being Subset of X st A <> the carrier of X holds
A is boundary ) holds
X is anti-discrete
proofend;

registration
let D be set ;
cluster 1TopSp D ->  discrete ;
coherence
 1TopSp D is discrete by TDLAT_3:def_1;
end;

theorem :: TEX_1:16
for X being non empty discrete TopSpace
for A being Subset of X holds
( Cl A = A &amp; Int A = A )
proofend;

theorem :: TEX_1:17
for X being non empty TopSpace st ( for A being Subset of X holds Cl A = A ) holds
X is discrete
proofend;

theorem :: TEX_1:18
for X being non empty TopSpace st ( for A being Subset of X holds Int A = A ) holds
X is discrete
proofend;

theorem Th19: :: TEX_1:19
for D being non empty set holds
( ADTS D = 1TopSp D iff ex d0 being Element of D st D = {d0} )
proofend;

registration
cluster non empty strict TopSpace-like discrete non anti-discrete for TopStruct ;
existence
 ex b1 being TopSpace st
( b1 is discrete &amp; not b1 is anti-discrete &amp; b1 is strict &amp; not b1 is empty )
proofend;
cluster non empty strict TopSpace-like non discrete anti-discrete for TopStruct ;
existence
 ex b1 being TopSpace st
( b1 is anti-discrete &amp; not b1 is discrete &amp; b1 is strict &amp; not b1 is empty )
proofend;
end;

begin

:: 4. An Example of a Topological Space.
definition
let D be set ;
let d0 be Element of D;
func STS (D,d0) ->  TopStruct  equals :: TEX_1:def 4
 TopStruct(# D,((bool D) \  {  A where A is Subset of D : ( d0 in A &amp; A <> D )  }  ) #);
coherence
 TopStruct(# D,((bool D) \  {  A where A is Subset of D : ( d0 in A &amp; A <> D )  }  ) #) is TopStruct ;
end;

:: deftheorem  defines STS TEX_1:def_4_:_
 for D being set
for d0 being Element of D holds STS (D,d0) = TopStruct(# D,((bool D) \  {  A where A is Subset of D : ( d0 in A &amp; A <> D )  }  ) #);

registration
let D be set ;
let d0 be Element of D;
cluster STS (D,d0) ->  strict TopSpace-like ;
coherence
 ( STS (D,d0) is strict &amp; STS (D,d0) is TopSpace-like )
proofend;
end;

registration
let D be non empty set ;
let d0 be Element of D;
cluster STS (D,d0) ->  non empty ;
coherence
 not STS (D,d0) is empty ;
end;

theorem Th20: :: TEX_1:20
for D being non empty set
for d0 being Element of D
for A being Subset of (STS (D,d0)) holds
( ( {d0} c= A implies A is closed ) &amp; ( not A is empty &amp; A is closed implies {d0} c= A ) )
proofend;

theorem Th21: :: TEX_1:21
for D being non empty set
for d0 being Element of D st not D \ {d0} is empty holds
for A being Subset of (STS (D,d0)) holds
( ( A = {d0} implies ( A is closed &amp; A is boundary ) ) &amp; ( not A is empty &amp; A is closed &amp; A is boundary implies A = {d0} ) )
proofend;

theorem Th22: :: TEX_1:22
for D being non empty set
for d0 being Element of D
for A being Subset of (STS (D,d0)) holds
( ( A c= D \ {d0} implies A is open ) &amp; ( A <> D &amp; A is open implies A c= D \ {d0} ) )
proofend;

theorem :: TEX_1:23
for D being non empty set
for d0 being Element of D st not D \ {d0} is empty holds
for A being Subset of (STS (D,d0)) holds
( ( A = D \ {d0} implies ( A is open &amp; A is dense ) ) &amp; ( A <> D &amp; A is open &amp; A is dense implies A = D \ {d0} ) )
proofend;

registration
cluster non empty strict TopSpace-like non discrete non anti-discrete for TopStruct ;
existence
 ex b1 being TopSpace st
( not b1 is anti-discrete &amp; not b1 is discrete &amp; b1 is strict &amp; not b1 is empty )
proofend;
end;

theorem Th24: :: TEX_1:24
for D being non empty set
for d0 being Element of D
for Y being non empty TopSpace holds
( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) iff ( the carrier of Y = D &amp; ( for A being Subset of Y holds
( ( {d0} c= A implies A is closed ) &amp; ( not A is empty &amp; A is closed implies {d0} c= A ) ) ) ) )
proofend;

theorem Th25: :: TEX_1:25
for D being non empty set
for d0 being Element of D
for Y being non empty TopSpace holds
( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) iff ( the carrier of Y = D &amp; ( for A being Subset of Y holds
( ( A c= D \ {d0} implies A is open ) &amp; ( A <> D &amp; A is open implies A c= D \ {d0} ) ) ) ) )
proofend;

theorem :: TEX_1:26
for D being non empty set
for d0 being Element of D
for Y being non empty TopSpace holds
( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) iff ( the carrier of Y = D &amp; ( for A being non empty Subset of Y holds Cl A = A \/ {d0} ) ) )
proofend;

theorem :: TEX_1:27
for D being non empty set
for d0 being Element of D
for Y being non empty TopSpace holds
( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) iff ( the carrier of Y = D &amp; ( for A being Subset of Y st A <> D holds
Int A = A \ {d0} ) ) )
proofend;

Lm2: now__::_thesis:_for_D_being_non_empty_set_
for_d0_being_Element_of_D
for_G_being_set_st_G_=__{__P_where_P_is_Subset_of_D_:_(_d0_in_P_&amp;_P_<>_D_)__}__&amp;_D_=_{d0}_holds_
not_G_<>_{}
let D be non empty set ; ::_thesis: for d0 being Element of D
for G being set st G =  {  P where P is Subset of D : ( d0 in P &amp; P <> D )  }  &amp; D = {d0} holds
not G <> {}
let d0 be Element of D; ::_thesis: for G being set st G =  {  P where P is Subset of D : ( d0 in P &amp; P <> D )  }  &amp; D = {d0} holds
not G <> {}
let G be set ; ::_thesis: ( G =  {  P where P is Subset of D : ( d0 in P &amp; P <> D )  }  &amp; D = {d0} implies not G <> {} )
assume A1: G =  {  P where P is Subset of D : ( d0 in P &amp; P <> D )  }  ; ::_thesis: ( D = {d0} implies not G <> {} )
set x = the Element of G;
assume A2: D = {d0} ; ::_thesis: not G <> {}
assume  G <> {} ; ::_thesis: contradiction
then  the Element of G in G ;
then consider S being Subset of D such that
 the Element of G = S and
A3: d0 in S and
A4: S <> D by A1;
set d1 = the Element of D \ S;
A5: now__::_thesis:_not_D_\_S_=_{}
assume  D \ S = {} ; ::_thesis: contradiction
then  D c= S by XBOOLE_1:37;
hence  contradiction by A4, XBOOLE_0:def_10; ::_thesis: verum
end;
then reconsider d1 = the Element of D \ S as Element of D by XBOOLE_0:def_5;
 d0 <> d1 by A3, A5, XBOOLE_0:def_5;
hence  contradiction by A2, TARSKI:def_1; ::_thesis: verum
end;

theorem :: TEX_1:28
for D being non empty set
for d0 being Element of D holds
( STS (D,d0) = ADTS D iff D = {d0} )
proofend;

theorem :: TEX_1:29
for D being non empty set
for d0 being Element of D holds
( STS (D,d0) = 1TopSp D iff D = {d0} )
proofend;

theorem :: TEX_1:30
for D being non empty set
for d0 being Element of D
for A being Subset of (STS (D,d0)) st A = {d0} holds
1TopSp D = (STS (D,d0)) modified_with_respect_to A
proofend;

begin

:: 5. Discrete and Almost Discrete Spaces.
definition
let X be non empty TopSpace;
redefine attr X is discrete  means :Def5: :: TEX_1:def 5
 for A being non empty Subset of X holds not A is boundary ;
compatibility
 ( X is discrete iff for A being non empty Subset of X holds not A is boundary )
proofend;
end;

:: deftheorem Def5 defines discrete TEX_1:def_5_:_
 for X being non empty TopSpace holds
( X is discrete iff for A being non empty Subset of X holds not A is boundary );

theorem :: TEX_1:31
for X being non empty TopSpace holds
( X is discrete iff for A being Subset of X st A <> the carrier of X holds
not A is dense )
proofend;

registration
cluster non empty TopSpace-like non almost_discrete  ->  non empty non discrete non anti-discrete for TopStruct ;
coherence
 for b1 being non empty TopSpace st not b1 is almost_discrete holds
( not b1 is discrete &amp; not b1 is anti-discrete ) ;
end;

definition
let X be non empty TopSpace;
redefine attr X is almost_discrete  means :Def6: :: TEX_1:def 6
 for A being non empty Subset of X holds not A is nowhere_dense ;
compatibility
 ( X is almost_discrete iff for A being non empty Subset of X holds not A is nowhere_dense )
proofend;
end;

:: deftheorem Def6 defines almost_discrete TEX_1:def_6_:_
 for X being non empty TopSpace holds
( X is almost_discrete iff for A being non empty Subset of X holds not A is nowhere_dense );

theorem Th32: :: TEX_1:32
for X being non empty TopSpace holds
( X is almost_discrete iff for A being Subset of X st A <> the carrier of X holds
not A is everywhere_dense )
proofend;

theorem Th33: :: TEX_1:33
for X being non empty TopSpace holds
( not X is almost_discrete iff ex A being non empty Subset of X st
( A is boundary &amp; A is closed ) )
proofend;

theorem :: TEX_1:34
for X being non empty TopSpace holds
( not X is almost_discrete iff ex A being Subset of X st
( A <> the carrier of X &amp; A is dense &amp; A is open ) )
proofend;

registration
cluster non empty strict TopSpace-like non discrete non anti-discrete almost_discrete for TopStruct ;
existence
 ex b1 being TopSpace st
( b1 is almost_discrete &amp; not b1 is discrete &amp; not b1 is anti-discrete &amp; b1 is strict &amp; not b1 is empty )
proofend;
end;

theorem Th35: :: TEX_1:35
for C being non empty set
for c0 being Element of C holds
( not C \ {c0} is empty iff not STS (C,c0) is almost_discrete )
proofend;

registration
cluster non empty strict TopSpace-like non almost_discrete for TopStruct ;
existence
 ex b1 being TopSpace st
( not b1 is almost_discrete &amp; b1 is strict &amp; not b1 is empty )
proofend;
end;

theorem :: TEX_1:36
for X being non empty TopSpace
for A being non empty Subset of X st A is boundary holds
not X modified_with_respect_to (A `) is almost_discrete
proofend;

theorem :: TEX_1:37
for X being non empty TopSpace
for A being Subset of X st A <> the carrier of X &amp; A is dense holds
not X modified_with_respect_to A is almost_discrete
proofend;