:: Maximal Discrete Subspaces of Almost Discrete Topological Spaces
:: by Zbigniew Karno
::
:: Received November 5, 1993
:: Copyright (c) 1993 Association of Mizar Users


begin

definition
let X be non empty set ;
redefine attr X is trivial means :Def1: :: TEX_2:def 1
ex s being Element of X st X = {s};
compatibility
( X is trivial iff ex s being Element of X st X = {s} )
proof end;
end;

:: deftheorem Def1 defines trivial TEX_2:def 1 :
for X being non empty set holds
( X is trivial iff ex s being Element of X st X = {s} );

theorem Th1: :: TEX_2:1
for A being non empty set
for B being non empty trivial set st A c= B holds
A = B
proof end;

theorem :: TEX_2:2
for A being non empty trivial set
for B being set st not A /\ B is empty holds
A c= B
proof end;

theorem :: TEX_2:3
canceled;

theorem :: TEX_2:4
for S, T being 1-sorted st the carrier of S = the carrier of T & S is trivial holds
T is trivial ;

registration
let S be non empty trivial set ;
cluster proper -> empty Element of K10(S);
coherence
for b1 being Subset of S st b1 is proper holds
b1 is empty
proof end;
cluster non empty -> non proper Element of K10(S);
coherence
for b1 being Subset of S st not b1 is empty holds
not b1 is proper
;
end;

registration
let S be non empty set ;
cluster non empty trivial Element of K10(S);
existence
ex b1 being non empty Subset of S st b1 is trivial
proof end;
end;

theorem :: TEX_2:5
canceled;

theorem :: TEX_2:6
for S being non empty set
for y being Element of S st {y} is proper holds
not S is trivial ;

theorem :: TEX_2:7
for S being non empty non trivial set
for y being Element of S holds {y} is proper by SUBSET_1:def 7;

registration
let S be non empty trivial set ;
cluster non empty non proper -> non empty trivial Element of K10(S);
coherence
for b1 being non empty Subset of S st not b1 is proper holds
b1 is trivial
;
end;

registration
let S be non empty non trivial set ;
cluster non empty trivial -> non empty proper Element of K10(S);
coherence
for b1 being non empty Subset of S st b1 is trivial holds
b1 is proper
by SUBSET_1:def 7;
cluster non empty non proper -> non empty non trivial Element of K10(S);
coherence
for b1 being non empty Subset of S st not b1 is proper holds
not b1 is trivial
;
end;

registration
let S be non empty non trivial set ;
cluster non empty trivial proper Element of K10(S);
existence
ex b1 being non empty Subset of S st
( b1 is trivial & b1 is proper )
proof end;
cluster non empty non trivial non proper Element of K10(S);
existence
ex b1 being non empty Subset of S st
( not b1 is trivial & not b1 is proper )
proof end;
end;

theorem :: TEX_2:8
for Y being non empty 1-sorted
for y being Element of Y st {y} is proper holds
not Y is trivial ;

theorem :: TEX_2:9
for Y being non empty non trivial 1-sorted
for y being Element of Y holds {y} is proper ;

registration
let Y be non empty trivial 1-sorted ;
cluster non empty -> non empty non proper Element of K10( the carrier of Y);
coherence
for b1 being non empty Subset of Y holds not b1 is proper
;
cluster non empty non proper -> non empty trivial Element of K10( the carrier of Y);
coherence
for b1 being non empty Subset of Y st not b1 is proper holds
b1 is trivial
;
end;

registration
let Y be non empty non trivial 1-sorted ;
cluster non empty trivial -> non empty proper Element of K10( the carrier of Y);
coherence
for b1 being non empty Subset of Y st b1 is trivial holds
b1 is proper
;
cluster non empty non proper -> non empty non trivial Element of K10( the carrier of Y);
coherence
for b1 being non empty Subset of Y st not b1 is proper holds
not b1 is trivial
;
end;

registration
let Y be non empty non trivial 1-sorted ;
cluster non empty trivial proper Element of K10( the carrier of Y);
existence
ex b1 being non empty Subset of Y st
( b1 is trivial & b1 is proper )
proof end;
cluster non empty non trivial non proper Element of K10( the carrier of Y);
existence
ex b1 being non empty Subset of Y st
( not b1 is trivial & not b1 is proper )
proof end;
end;

registration
let Y be non empty non trivial 1-sorted ;
cluster non empty trivial proper Element of K10( the carrier of Y);
existence
ex b1 being Subset of Y st
( not b1 is empty & b1 is trivial & b1 is proper )
proof end;
end;

registration
let X be non empty set ;
let A be proper Subset of X;
cluster A ` -> non empty ;
coherence
not A ` is empty
proof end;
end;

begin

theorem :: TEX_2:10
canceled;

theorem :: TEX_2:11
canceled;

theorem :: TEX_2:12
for Y0, Y1 being TopStruct st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & Y0 is TopSpace-like holds
Y1 is TopSpace-like
proof end;

definition
canceled;
let Y be TopStruct ;
let IT be SubSpace of Y;
attr IT is proper means :Def3: :: TEX_2:def 3
for A being Subset of Y st A = the carrier of IT holds
A is proper ;
end;

:: deftheorem TEX_2:def 2 :
canceled;

:: deftheorem Def3 defines proper TEX_2:def 3 :
for Y being TopStruct
for IT being SubSpace of Y holds
( IT is proper iff for A being Subset of Y st A = the carrier of IT holds
A is proper );

theorem Th13: :: TEX_2:13
for Y being TopStruct
for Y0 being SubSpace of Y
for A being Subset of Y st A = the carrier of Y0 holds
( A is proper iff Y0 is proper )
proof end;

Lm1: now
let Z be TopStruct ; :: thesis: for Z0 being SubSpace of Z holds the carrier of Z0 is Subset of Z
let Z0 be SubSpace of Z; :: thesis: the carrier of Z0 is Subset of Z
[#] Z0 c= [#] Z by PRE_TOPC:def 9;
hence the carrier of Z0 is Subset of Z ; :: thesis: verum
end;

theorem :: TEX_2:14
for Y being TopStruct
for Y0, Y1 being SubSpace of Y st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & Y0 is proper holds
Y1 is proper
proof end;

theorem Th15: :: TEX_2:15
for Y being TopStruct
for Y0 being SubSpace of Y st the carrier of Y0 = the carrier of Y holds
not Y0 is proper
proof end;

registration
let Y be non empty trivial TopStruct ;
cluster non empty -> non empty non proper SubSpace of Y;
coherence
for b1 being non empty SubSpace of Y holds not b1 is proper
proof end;
cluster non empty non proper -> non empty trivial SubSpace of Y;
coherence
for b1 being non empty SubSpace of Y st not b1 is proper holds
b1 is trivial
proof end;
end;

registration
let Y be non empty non trivial TopStruct ;
cluster non empty trivial -> non empty proper SubSpace of Y;
coherence
for b1 being non empty SubSpace of Y st b1 is trivial holds
b1 is proper
proof end;
cluster non empty non proper -> non empty non trivial SubSpace of Y;
coherence
for b1 being non empty SubSpace of Y st not b1 is proper holds
not b1 is trivial
;
end;

registration
let Y be non empty TopStruct ;
cluster non empty strict non proper SubSpace of Y;
existence
ex b1 being SubSpace of Y st
( not b1 is proper & b1 is strict & not b1 is empty )
proof end;
end;

theorem :: TEX_2:16
for Y being non empty TopStruct
for Y0 being non proper SubSpace of Y holds TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y, the topology of Y #)
proof end;

registration
let Y be non empty TopStruct ;
cluster discrete -> TopSpace-like SubSpace of Y;
coherence
for b1 being SubSpace of Y st b1 is discrete holds
b1 is TopSpace-like
;
cluster anti-discrete -> TopSpace-like SubSpace of Y;
coherence
for b1 being SubSpace of Y st b1 is anti-discrete holds
b1 is TopSpace-like
;
cluster non TopSpace-like -> non discrete SubSpace of Y;
coherence
for b1 being SubSpace of Y st not b1 is TopSpace-like holds
not b1 is discrete
;
cluster non TopSpace-like -> non anti-discrete SubSpace of Y;
coherence
for b1 being SubSpace of Y st not b1 is TopSpace-like holds
not b1 is anti-discrete
;
end;

theorem Th17: :: TEX_2:17
for Y0, Y1 being TopStruct st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & Y0 is discrete holds
Y1 is discrete
proof end;

theorem :: TEX_2:18
for Y0, Y1 being TopStruct st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & Y0 is anti-discrete holds
Y1 is anti-discrete
proof end;

registration
let Y be non empty TopStruct ;
cluster discrete -> almost_discrete SubSpace of Y;
coherence
for b1 being SubSpace of Y st b1 is discrete holds
b1 is almost_discrete
;
cluster non almost_discrete -> non discrete SubSpace of Y;
coherence
for b1 being SubSpace of Y st not b1 is almost_discrete holds
not b1 is discrete
;
cluster anti-discrete -> almost_discrete SubSpace of Y;
coherence
for b1 being SubSpace of Y st b1 is anti-discrete holds
b1 is almost_discrete
;
cluster non almost_discrete -> non anti-discrete SubSpace of Y;
coherence
for b1 being SubSpace of Y st not b1 is almost_discrete holds
not b1 is anti-discrete
;
end;

theorem :: TEX_2:19
for Y0, Y1 being TopStruct st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & Y0 is almost_discrete holds
Y1 is almost_discrete
proof end;

registration
let Y be non empty TopStruct ;
cluster non empty discrete anti-discrete -> non empty trivial SubSpace of Y;
coherence
for b1 being non empty SubSpace of Y st b1 is discrete & b1 is anti-discrete holds
b1 is trivial
;
cluster non empty non trivial anti-discrete -> non empty non discrete SubSpace of Y;
coherence
for b1 being non empty SubSpace of Y st b1 is anti-discrete & not b1 is trivial holds
not b1 is discrete
;
cluster non empty non trivial discrete -> non empty non anti-discrete SubSpace of Y;
coherence
for b1 being non empty SubSpace of Y st b1 is discrete & not b1 is trivial holds
not b1 is anti-discrete
;
end;

definition
let Y be non empty TopStruct ;
let y be Point of Y;
func Sspace y -> non empty strict SubSpace of Y means :Def4: :: TEX_2:def 4
the carrier of it = {y};
existence
ex b1 being non empty strict SubSpace of Y st the carrier of b1 = {y}
proof end;
uniqueness
for b1, b2 being non empty strict SubSpace of Y st the carrier of b1 = {y} & the carrier of b2 = {y} holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines Sspace TEX_2:def 4 :
for Y being non empty TopStruct
for y being Point of Y
for b3 being non empty strict SubSpace of Y holds
( b3 = Sspace y iff the carrier of b3 = {y} );

Lm2: now
let Y be non empty TopStruct ; :: thesis: for y being Point of Y holds Sspace y is trivial
let y be Point of Y; :: thesis: Sspace y is trivial
set Y0 = Sspace y;
the carrier of (Sspace y) = {y} by Def4;
then reconsider y0 = y as Point of (Sspace y) by TARSKI:def 1;
the carrier of (Sspace y) = {y0} by Def4;
hence Sspace y is trivial ; :: thesis: verum
end;

registration
let Y be non empty TopStruct ;
cluster non empty trivial strict SubSpace of Y;
existence
ex b1 being SubSpace of Y st
( b1 is trivial & b1 is strict & not b1 is empty )
proof end;
end;

registration
let Y be non empty TopStruct ;
let y be Point of Y;
cluster Sspace y -> non empty trivial strict ;
coherence
Sspace y is trivial
by Lm2;
end;

theorem :: TEX_2:20
for Y being non empty TopStruct
for y being Point of Y holds
( Sspace y is proper iff {y} is proper )
proof end;

theorem :: TEX_2:21
for Y being non empty TopStruct
for y being Point of Y st Sspace y is proper holds
not Y is trivial ;

registration
let Y be non empty non trivial TopStruct ;
cluster non empty trivial strict proper SubSpace of Y;
existence
ex b1 being non empty SubSpace of Y st
( b1 is proper & b1 is trivial & b1 is strict )
proof end;
end;

theorem :: TEX_2:22
canceled;

theorem :: TEX_2:23
for Y being non empty TopStruct
for Y0 being non empty trivial SubSpace of Y ex y being Point of Y st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of (Sspace y), the topology of (Sspace y) #)
proof end;

theorem :: TEX_2:24
for Y being non empty TopStruct
for y being Point of Y st Sspace y is TopSpace-like holds
( Sspace y is discrete & Sspace y is anti-discrete ) ;

registration
let Y be non empty TopStruct ;
cluster non empty trivial TopSpace-like -> non empty discrete anti-discrete SubSpace of Y;
coherence
for b1 being non empty SubSpace of Y st b1 is trivial & b1 is TopSpace-like holds
( b1 is discrete & b1 is anti-discrete )
;
end;

registration
let X be non empty TopSpace;
cluster non empty trivial strict TopSpace-like SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is trivial & b1 is strict & b1 is TopSpace-like & not b1 is empty )
proof end;
end;

registration
let X be non empty TopSpace;
let x be Point of X;
cluster Sspace x -> non empty strict TopSpace-like ;
coherence
Sspace x is TopSpace-like
;
end;

registration
let X be non empty TopSpace;
cluster non empty strict TopSpace-like discrete anti-discrete SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is discrete & b1 is anti-discrete & b1 is strict & not b1 is empty )
proof end;
end;

registration
let X be non empty TopSpace;
let x be Point of X;
cluster Sspace x -> non empty strict discrete anti-discrete ;
coherence
( Sspace x is discrete & Sspace x is anti-discrete )
;
end;

registration
let X be non empty TopSpace;
cluster non proper -> closed open SubSpace of X;
coherence
for b1 being SubSpace of X st not b1 is proper holds
( b1 is open & b1 is closed )
proof end;
cluster non open -> proper SubSpace of X;
coherence
for b1 being SubSpace of X st not b1 is open holds
b1 is proper
;
cluster non closed -> proper SubSpace of X;
coherence
for b1 being SubSpace of X st not b1 is closed holds
b1 is proper
;
end;

registration
let X be non empty TopSpace;
cluster strict TopSpace-like closed open SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is open & b1 is closed & b1 is strict )
proof end;
end;

registration
let X be non empty discrete TopSpace;
cluster non empty anti-discrete -> non empty trivial SubSpace of X;
coherence
for b1 being non empty SubSpace of X st b1 is anti-discrete holds
b1 is trivial
;
cluster non empty non trivial -> non empty non anti-discrete SubSpace of X;
coherence
for b1 being non empty SubSpace of X st not b1 is trivial holds
not b1 is anti-discrete
;
end;

registration
let X be non empty non trivial discrete TopSpace;
cluster strict TopSpace-like closed open discrete almost_discrete proper SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is discrete & b1 is open & b1 is closed & b1 is proper & b1 is strict )
proof end;
end;

registration
let X be non empty anti-discrete TopSpace;
cluster non empty discrete -> non empty trivial SubSpace of X;
coherence
for b1 being non empty SubSpace of X st b1 is discrete holds
b1 is trivial
;
cluster non empty non trivial -> non empty non discrete SubSpace of X;
coherence
for b1 being non empty SubSpace of X st not b1 is trivial holds
not b1 is discrete
;
end;

registration
let X be non empty non trivial anti-discrete TopSpace;
cluster non empty proper -> non empty non closed non open proper SubSpace of X;
coherence
for b1 being non empty proper SubSpace of X holds
( not b1 is open & not b1 is closed )
proof end;
cluster non empty discrete -> non empty trivial discrete proper SubSpace of X;
coherence
for b1 being non empty discrete SubSpace of X holds
( b1 is trivial & b1 is proper )
;
end;

registration
let X be non empty non trivial anti-discrete TopSpace;
cluster strict TopSpace-like non closed non open anti-discrete almost_discrete proper SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is anti-discrete & not b1 is open & not b1 is closed & b1 is proper & b1 is strict )
proof end;
end;

registration
let X be non empty non trivial almost_discrete TopSpace;
cluster non empty strict TopSpace-like almost_discrete proper SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is almost_discrete & b1 is proper & b1 is strict & not b1 is empty )
proof end;
end;

begin

definition
let Y be TopStruct ;
let IT be Subset of Y;
attr IT is discrete means :Def5: :: TEX_2:def 5
for D being Subset of Y st D c= IT holds
ex G being Subset of Y st
( G is open & IT /\ G = D );
end;

:: deftheorem Def5 defines discrete TEX_2:def 5 :
for Y being TopStruct
for IT being Subset of Y holds
( IT is discrete iff for D being Subset of Y st D c= IT holds
ex G being Subset of Y st
( G is open & IT /\ G = D ) );

definition
let Y be TopStruct ;
let A be Subset of Y;
redefine attr A is discrete means :Def6: :: TEX_2:def 6
for D being Subset of Y st D c= A holds
ex F being Subset of Y st
( F is closed & A /\ F = D );
compatibility
( A is discrete iff for D being Subset of Y st D c= A holds
ex F being Subset of Y st
( F is closed & A /\ F = D ) )
proof end;
end;

:: deftheorem Def6 defines discrete TEX_2:def 6 :
for Y being TopStruct
for A being Subset of Y holds
( A is discrete iff for D being Subset of Y st D c= A holds
ex F being Subset of Y st
( F is closed & A /\ F = D ) );

theorem Th25: :: TEX_2:25
for Y0, Y1 being TopStruct
for D0 being Subset of Y0
for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is discrete holds
D1 is discrete
proof end;

theorem Th26: :: TEX_2:26
for Y being non empty TopStruct
for Y0 being non empty SubSpace of Y
for A being Subset of Y st A = the carrier of Y0 holds
( A is discrete iff Y0 is discrete )
proof end;

theorem Th27: :: TEX_2:27
for Y being non empty TopStruct
for A being Subset of Y st A = the carrier of Y holds
( A is discrete iff Y is discrete )
proof end;

theorem Th28: :: TEX_2:28
for Y being TopStruct
for A, B being Subset of Y st B c= A & A is discrete holds
B is discrete
proof end;

theorem :: TEX_2:29
for Y being TopStruct
for A, B being Subset of Y st ( A is discrete or B is discrete ) holds
A /\ B is discrete
proof end;

theorem Th30: :: TEX_2:30
for Y being TopStruct st ( for P, Q being Subset of Y st P is open & Q is open holds
( P /\ Q is open & P \/ Q is open ) ) holds
for A, B being Subset of Y st A is open & B is open & A is discrete & B is discrete holds
A \/ B is discrete
proof end;

theorem Th31: :: TEX_2:31
for Y being TopStruct st ( for P, Q being Subset of Y st P is closed & Q is closed holds
( P /\ Q is closed & P \/ Q is closed ) ) holds
for A, B being Subset of Y st A is closed & B is closed & A is discrete & B is discrete holds
A \/ B is discrete
proof end;

theorem Th32: :: TEX_2:32
for Y being TopStruct
for A being Subset of Y st A is discrete holds
for x being Point of Y st x in A holds
ex G being Subset of Y st
( G is open & A /\ G = {x} )
proof end;

theorem :: TEX_2:33
for Y being TopStruct
for A being Subset of Y st A is discrete holds
for x being Point of Y st x in A holds
ex F being Subset of Y st
( F is closed & A /\ F = {x} )
proof end;

theorem Th34: :: TEX_2:34
for X being non empty TopSpace
for A0 being non empty Subset of X st A0 is discrete holds
ex X0 being non empty strict discrete SubSpace of X st A0 = the carrier of X0
proof end;

theorem Th35: :: TEX_2:35
for X being non empty TopSpace
for A being empty Subset of X holds A is discrete
proof end;

theorem Th36: :: TEX_2:36
for X being non empty TopSpace
for x being Point of X holds {x} is discrete
proof end;

theorem Th37: :: TEX_2:37
for X being non empty TopSpace
for A being Subset of X st ( for x being Point of X st x in A holds
ex G being Subset of X st
( G is open & A /\ G = {x} ) ) holds
A is discrete
proof end;

theorem :: TEX_2:38
for X being non empty TopSpace
for A, B being Subset of X st A is open & B is open & A is discrete & B is discrete holds
A \/ B is discrete
proof end;

theorem :: TEX_2:39
for X being non empty TopSpace
for A, B being Subset of X st A is closed & B is closed & A is discrete & B is discrete holds
A \/ B is discrete
proof end;

Lm3: for P, Q being set st P c= Q & P <> Q holds
Q \ P <> {}
proof end;

theorem :: TEX_2:40
for X being non empty TopSpace
for A being Subset of X st A is everywhere_dense & A is discrete holds
A is open
proof end;

theorem Th41: :: TEX_2:41
for X being non empty TopSpace
for A being Subset of X holds
( A is discrete iff for D being Subset of X st D c= A holds
A /\ (Cl D) = D )
proof end;

theorem Th42: :: TEX_2:42
for X being non empty TopSpace
for A being Subset of X st A is discrete holds
for x being Point of X st x in A holds
A /\ (Cl {x}) = {x}
proof end;

theorem :: TEX_2:43
for X being non empty discrete TopSpace
for A being Subset of X holds A is discrete
proof end;

theorem Th44: :: TEX_2:44
for X being non empty anti-discrete TopSpace
for A being non empty Subset of X holds
( A is discrete iff A is trivial )
proof end;

definition
let Y be TopStruct ;
let IT be Subset of Y;
attr IT is maximal_discrete means :Def7: :: TEX_2:def 7
( IT is discrete & ( for D being Subset of Y st D is discrete & IT c= D holds
IT = D ) );
end;

:: deftheorem Def7 defines maximal_discrete TEX_2:def 7 :
for Y being TopStruct
for IT being Subset of Y holds
( IT is maximal_discrete iff ( IT is discrete & ( for D being Subset of Y st D is discrete & IT c= D holds
IT = D ) ) );

theorem :: TEX_2:45
for Y0, Y1 being TopStruct
for D0 being Subset of Y0
for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is maximal_discrete holds
D1 is maximal_discrete
proof end;

theorem Th46: :: TEX_2:46
for X being non empty TopSpace
for A being empty Subset of X holds not A is maximal_discrete
proof end;

theorem Th47: :: TEX_2:47
for X being non empty TopSpace
for A being Subset of X st A is open & A is maximal_discrete holds
A is dense
proof end;

theorem :: TEX_2:48
for X being non empty TopSpace
for A being Subset of X st A is dense & A is discrete holds
A is maximal_discrete
proof end;

theorem Th49: :: TEX_2:49
for X being non empty discrete TopSpace
for A being Subset of X holds
( A is maximal_discrete iff not A is proper )
proof end;

theorem Th50: :: TEX_2:50
for X being non empty anti-discrete TopSpace
for A being non empty Subset of X holds
( A is maximal_discrete iff A is trivial )
proof end;

definition
let Y be non empty TopStruct ;
let IT be SubSpace of Y;
attr IT is maximal_discrete means :Def8: :: TEX_2:def 8
for A being Subset of Y st A = the carrier of IT holds
A is maximal_discrete ;
end;

:: deftheorem Def8 defines maximal_discrete TEX_2:def 8 :
for Y being non empty TopStruct
for IT being SubSpace of Y holds
( IT is maximal_discrete iff for A being Subset of Y st A = the carrier of IT holds
A is maximal_discrete );

theorem Th51: :: TEX_2:51
for Y being non empty TopStruct
for Y0 being SubSpace of Y
for A being Subset of Y st A = the carrier of Y0 holds
( A is maximal_discrete iff Y0 is maximal_discrete )
proof end;

registration
let Y be non empty TopStruct ;
cluster non empty maximal_discrete -> non empty discrete SubSpace of Y;
coherence
for b1 being non empty SubSpace of Y st b1 is maximal_discrete holds
b1 is discrete
proof end;
cluster non empty non discrete -> non empty non maximal_discrete SubSpace of Y;
coherence
for b1 being non empty SubSpace of Y st not b1 is discrete holds
not b1 is maximal_discrete
;
end;

theorem :: TEX_2:52
for X being non empty TopSpace
for X0 being non empty SubSpace of X holds
( X0 is maximal_discrete iff ( X0 is discrete & ( for Y0 being non empty discrete SubSpace of X st X0 is SubSpace of Y0 holds
TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) ) )
proof end;

theorem Th53: :: TEX_2:53
for X being non empty TopSpace
for A0 being non empty Subset of X st A0 is maximal_discrete holds
ex X0 being non empty strict SubSpace of X st
( X0 is maximal_discrete & A0 = the carrier of X0 )
proof end;

registration
let X be non empty discrete TopSpace;
cluster maximal_discrete -> non proper SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is maximal_discrete holds
not b1 is proper
proof end;
cluster proper -> non maximal_discrete SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is proper holds
not b1 is maximal_discrete
;
cluster non proper -> maximal_discrete SubSpace of X;
coherence
for b1 being SubSpace of X st not b1 is proper holds
b1 is maximal_discrete
proof end;
cluster non maximal_discrete -> proper SubSpace of X;
coherence
for b1 being SubSpace of X st not b1 is maximal_discrete holds
b1 is proper
;
end;

registration
let X be non empty anti-discrete TopSpace;
cluster non empty maximal_discrete -> non empty trivial SubSpace of X;
coherence
for b1 being non empty SubSpace of X st b1 is maximal_discrete holds
b1 is trivial
;
cluster non empty non trivial -> non empty non maximal_discrete SubSpace of X;
coherence
for b1 being non empty SubSpace of X st not b1 is trivial holds
not b1 is maximal_discrete
;
cluster non empty trivial -> non empty maximal_discrete SubSpace of X;
coherence
for b1 being non empty SubSpace of X st b1 is trivial holds
b1 is maximal_discrete
proof end;
cluster non empty non maximal_discrete -> non empty non trivial SubSpace of X;
coherence
for b1 being non empty SubSpace of X st not b1 is maximal_discrete holds
not b1 is trivial
;
end;

begin

scheme :: TEX_2:sch 1
ExChoiceFCol{ F1() -> non empty TopStruct , F2() -> Subset-Family of F1(), P1[ set , set ] } :
ex f being Function of F2(), the carrier of F1() st
for S being Subset of F1() st S in F2() holds
P1[S,f . S]
provided
A1: for S being Subset of F1() st S in F2() holds
ex x being Point of F1() st P1[S,x]
proof end;

theorem Th54: :: TEX_2:54
for X being non empty almost_discrete TopSpace
for A being Subset of X holds Cl A = union { (Cl {a}) where a is Point of X : a in A }
proof end;

theorem Th55: :: TEX_2:55
for X being non empty almost_discrete TopSpace
for a, b being Point of X st a in Cl {b} holds
Cl {a} = Cl {b}
proof end;

theorem Th56: :: TEX_2:56
for X being non empty almost_discrete TopSpace
for a, b being Point of X holds
( Cl {a} misses Cl {b} or Cl {a} = Cl {b} )
proof end;

theorem Th57: :: TEX_2:57
for X being non empty almost_discrete TopSpace
for A being Subset of X st ( for x being Point of X st x in A holds
ex F being Subset of X st
( F is closed & A /\ F = {x} ) ) holds
A is discrete
proof end;

theorem Th58: :: TEX_2:58
for X being non empty almost_discrete TopSpace
for A being Subset of X st ( for x being Point of X st x in A holds
A /\ (Cl {x}) = {x} ) holds
A is discrete
proof end;

theorem :: TEX_2:59
for X being non empty almost_discrete TopSpace
for A being Subset of X holds
( A is discrete iff for a, b being Point of X st a in A & b in A & a <> b holds
Cl {a} misses Cl {b} )
proof end;

theorem Th60: :: TEX_2:60
for X being non empty almost_discrete TopSpace
for A being Subset of X holds
( A is discrete iff for x being Point of X st x in Cl A holds
ex a being Point of X st
( a in A & A /\ (Cl {x}) = {a} ) )
proof end;

theorem :: TEX_2:61
for X being non empty almost_discrete TopSpace
for A being Subset of X st ( A is open or A is closed ) & A is maximal_discrete holds
not A is proper
proof end;

theorem Th62: :: TEX_2:62
for X being non empty almost_discrete TopSpace
for A being Subset of X st A is maximal_discrete holds
A is dense
proof end;

theorem Th63: :: TEX_2:63
for X being non empty almost_discrete TopSpace
for A being Subset of X st A is maximal_discrete holds
union { (Cl {a}) where a is Point of X : a in A } = the carrier of X
proof end;

theorem Th64: :: TEX_2:64
for X being non empty almost_discrete TopSpace
for A being Subset of X holds
( A is maximal_discrete iff for x being Point of X ex a being Point of X st
( a in A & A /\ (Cl {x}) = {a} ) )
proof end;

theorem Th65: :: TEX_2:65
for X being non empty almost_discrete TopSpace
for A being Subset of X st A is discrete holds
ex M being Subset of X st
( A c= M & M is maximal_discrete )
proof end;

theorem Th66: :: TEX_2:66
for X being non empty almost_discrete TopSpace ex M being Subset of X st M is maximal_discrete
proof end;

theorem Th67: :: TEX_2:67
for X being non empty almost_discrete TopSpace
for Y0 being non empty discrete SubSpace of X ex X0 being non empty strict SubSpace of X st
( Y0 is SubSpace of X0 & X0 is maximal_discrete )
proof end;

registration
let X be non empty non discrete almost_discrete TopSpace;
cluster non empty maximal_discrete -> non empty proper SubSpace of X;
coherence
for b1 being non empty SubSpace of X st b1 is maximal_discrete holds
b1 is proper
proof end;
cluster non empty non proper -> non empty non maximal_discrete SubSpace of X;
coherence
for b1 being non empty SubSpace of X st not b1 is proper holds
not b1 is maximal_discrete
;
end;

registration
let X be non empty non anti-discrete almost_discrete TopSpace;
cluster non empty maximal_discrete -> non empty non trivial SubSpace of X;
coherence
for b1 being non empty SubSpace of X st b1 is maximal_discrete holds
not b1 is trivial
proof end;
cluster non empty trivial -> non empty non maximal_discrete SubSpace of X;
coherence
for b1 being non empty SubSpace of X st b1 is trivial holds
not b1 is maximal_discrete
;
end;

registration
let X be non empty almost_discrete TopSpace;
cluster non empty strict TopSpace-like maximal_discrete SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is maximal_discrete & b1 is strict & not b1 is empty & not b1 is empty )
proof end;
end;

begin

theorem Th68: :: TEX_2:68
for X being discrete TopSpace
for Y being TopSpace
for f being Function of X,Y holds f is continuous
proof end;

theorem :: TEX_2:69
for X being non empty TopSpace st ( for Y being non empty TopSpace
for f being Function of X,Y holds f is continuous ) holds
X is discrete
proof end;

theorem :: TEX_2:70
for X being non empty TopSpace
for Y being non empty anti-discrete TopSpace
for f being Function of X,Y holds f is continuous
proof end;

theorem :: TEX_2:71
for Y being non empty TopSpace st ( for X being non empty TopSpace
for f being Function of X,Y holds f is continuous ) holds
Y is anti-discrete
proof end;

theorem Th72: :: TEX_2:72
for X being non empty discrete TopSpace
for X0 being non empty SubSpace of X ex r being continuous Function of X,X0 st r is being_a_retraction
proof end;

theorem :: TEX_2:73
for X being non empty discrete TopSpace
for X0 being non empty SubSpace of X holds X0 is_a_retract_of X
proof end;

theorem Th74: :: TEX_2:74
for X being non empty almost_discrete TopSpace
for X0 being non empty maximal_discrete SubSpace of X ex r being continuous Function of X,X0 st r is being_a_retraction
proof end;

theorem :: TEX_2:75
for X being non empty almost_discrete TopSpace
for X0 being non empty maximal_discrete SubSpace of X holds X0 is_a_retract_of X
proof end;

Lm4: for X being non empty almost_discrete TopSpace
for X0 being non empty maximal_discrete SubSpace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for a being Point of X0
for b being Point of X st a = b holds
Cl {b} c= r " {a}
proof end;

theorem Th76: :: TEX_2:76
for X being non empty almost_discrete TopSpace
for X0 being non empty maximal_discrete SubSpace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for F being Subset of X0
for E being Subset of X st F = E holds
r " F = Cl E
proof end;

theorem :: TEX_2:77
for X being non empty almost_discrete TopSpace
for X0 being non empty maximal_discrete SubSpace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for a being Point of X0
for b being Point of X st a = b holds
r " {a} = Cl {b} by Th76;

theorem Th78: :: TEX_2:78
for X being non empty almost_discrete TopSpace
for X0 being non empty discrete SubSpace of X ex r being continuous Function of X,X0 st r is being_a_retraction
proof end;

theorem :: TEX_2:79
for X being non empty almost_discrete TopSpace
for X0 being non empty discrete SubSpace of X holds X0 is_a_retract_of X
proof end;