:: 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 b₁ being Subset of S st b₁ is proper holds
b₁ is empty

proof end;

cluster non empty -> non proper Element of K10(S);
coherence
for b₁ being Subset of S st not b₁ is empty holds
not b₁ is proper ;

end;

registration

let S be non empty set ;
cluster non empty trivial Element of K10(S);
existence
ex b₁ being non empty Subset of S st b₁ 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 b₁ being non empty Subset of S st not b₁ is proper holds
b₁ 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 b₁ being non empty Subset of S st b₁ is trivial holds
b₁ is proper by SUBSET_1:def 7;
cluster non empty non proper -> non empty non trivial Element of K10(S);
coherence
for b₁ being non empty Subset of S st not b₁ is proper holds
not b₁ is trivial ;

end;

registration

let S be non empty non trivial set ;
cluster non empty trivial proper Element of K10(S);
existence
ex b₁ being non empty Subset of S st
( b₁ is trivial & b₁ is proper )

proof end;

cluster non empty non trivial non proper Element of K10(S);
existence
ex b₁ being non empty Subset of S st
( not b₁ is trivial & not b₁ 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 b₁ being non empty Subset of Y holds not b₁ is proper ;
cluster non empty non proper -> non empty trivial Element of K10( the carrier of Y);
coherence
for b₁ being non empty Subset of Y st not b₁ is proper holds
b₁ 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 b₁ being non empty Subset of Y st b₁ is trivial holds
b₁ is proper ;
cluster non empty non proper -> non empty non trivial Element of K10( the carrier of Y);
coherence
for b₁ being non empty Subset of Y st not b₁ is proper holds
not b₁ 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 b₁ being non empty Subset of Y st
( b₁ is trivial & b₁ is proper )

proof end;

cluster non empty non trivial non proper Element of K10( the carrier of Y);
existence
ex b₁ being non empty Subset of Y st
( not b₁ is trivial & not b₁ 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 b₁ being Subset of Y st
( not b₁ is empty & b₁ is trivial & b₁ 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 b₁ being non empty SubSpace of Y holds not b₁ is proper

proof end;

cluster non empty non proper -> non empty trivial SubSpace of Y;
coherence
for b₁ being non empty SubSpace of Y st not b₁ is proper holds
b₁ 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 b₁ being non empty SubSpace of Y st b₁ is trivial holds
b₁ is proper

proof end;

cluster non empty non proper -> non empty non trivial SubSpace of Y;
coherence
for b₁ being non empty SubSpace of Y st not b₁ is proper holds
not b₁ is trivial ;

end;

registration

let Y be non empty TopStruct ;
cluster non empty strict non proper SubSpace of Y;
existence
ex b₁ being SubSpace of Y st
( not b₁ is proper & b₁ is strict & not b₁ 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 b₁ being SubSpace of Y st b₁ is discrete holds
b₁ is TopSpace-like ;
cluster anti-discrete -> TopSpace-like SubSpace of Y;
coherence
for b₁ being SubSpace of Y st b₁ is anti-discrete holds
b₁ is TopSpace-like ;
cluster non TopSpace-like -> non discrete SubSpace of Y;
coherence
for b₁ being SubSpace of Y st not b₁ is TopSpace-like holds
not b₁ is discrete ;
cluster non TopSpace-like -> non anti-discrete SubSpace of Y;
coherence
for b₁ being SubSpace of Y st not b₁ is TopSpace-like holds
not b₁ 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 b₁ being SubSpace of Y st b₁ is discrete holds
b₁ is almost_discrete ;
cluster non almost_discrete -> non discrete SubSpace of Y;
coherence
for b₁ being SubSpace of Y st not b₁ is almost_discrete holds
not b₁ is discrete ;
cluster anti-discrete -> almost_discrete SubSpace of Y;
coherence
for b₁ being SubSpace of Y st b₁ is anti-discrete holds
b₁ is almost_discrete ;
cluster non almost_discrete -> non anti-discrete SubSpace of Y;
coherence
for b₁ being SubSpace of Y st not b₁ is almost_discrete holds
not b₁ 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 b₁ being non empty SubSpace of Y st b₁ is discrete & b₁ is anti-discrete holds
b₁ is trivial ;
cluster non empty non trivial anti-discrete -> non empty non discrete SubSpace of Y;
coherence
for b₁ being non empty SubSpace of Y st b₁ is anti-discrete & not b₁ is trivial holds
not b₁ is discrete ;
cluster non empty non trivial discrete -> non empty non anti-discrete SubSpace of Y;
coherence
for b₁ being non empty SubSpace of Y st b₁ is discrete & not b₁ is trivial holds
not b₁ 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 b₁ being non empty strict SubSpace of Y st the carrier of b₁ = {y}

proof end;

uniqueness
for b₁, b₂ being non empty strict SubSpace of Y st the carrier of b₁ = {y} & the carrier of b₂ = {y} holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines Sspace TEX_2:def 4 :
for Y being non empty TopStruct
for y being Point of Y
for b₃ being non empty strict SubSpace of Y holds
( b₃ = Sspace y iff the carrier of b₃ = {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 b₁ being SubSpace of Y st
( b₁ is trivial & b₁ is strict & not b₁ 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 b₁ being non empty SubSpace of Y st
( b₁ is proper & b₁ is trivial & b₁ 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 b₁ being non empty SubSpace of Y st b₁ is trivial & b₁ is TopSpace-like holds
( b₁ is discrete & b₁ is anti-discrete ) ;

end;

registration

let X be non empty TopSpace;
cluster non empty trivial strict TopSpace-like SubSpace of X;
existence
ex b₁ being SubSpace of X st
( b₁ is trivial & b₁ is strict & b₁ is TopSpace-like & not b₁ 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 b₁ being SubSpace of X st
( b₁ is discrete & b₁ is anti-discrete & b₁ is strict & not b₁ 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 b₁ being SubSpace of X st not b₁ is proper holds
( b₁ is open & b₁ is closed )

proof end;

cluster non open -> proper SubSpace of X;
coherence
for b₁ being SubSpace of X st not b₁ is open holds
b₁ is proper ;
cluster non closed -> proper SubSpace of X;
coherence
for b₁ being SubSpace of X st not b₁ is closed holds
b₁ is proper ;

end;

registration

let X be non empty TopSpace;
cluster strict TopSpace-like closed open SubSpace of X;
existence
ex b₁ being SubSpace of X st
( b₁ is open & b₁ is closed & b₁ 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 b₁ being non empty SubSpace of X st b₁ is anti-discrete holds
b₁ is trivial ;
cluster non empty non trivial -> non empty non anti-discrete SubSpace of X;
coherence
for b₁ being non empty SubSpace of X st not b₁ is trivial holds
not b₁ 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 b₁ being SubSpace of X st
( b₁ is discrete & b₁ is open & b₁ is closed & b₁ is proper & b₁ 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 b₁ being non empty SubSpace of X st b₁ is discrete holds
b₁ is trivial ;
cluster non empty non trivial -> non empty non discrete SubSpace of X;
coherence
for b₁ being non empty SubSpace of X st not b₁ is trivial holds
not b₁ 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 b₁ being non empty proper SubSpace of X holds
( not b₁ is open & not b₁ is closed )

proof end;

cluster non empty discrete -> non empty trivial discrete proper SubSpace of X;
coherence
for b₁ being non empty discrete SubSpace of X holds
( b₁ is trivial & b₁ 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 b₁ being SubSpace of X st
( b₁ is anti-discrete & not b₁ is open & not b₁ is closed & b₁ is proper & b₁ 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 b₁ being SubSpace of X st
( b₁ is almost_discrete & b₁ is proper & b₁ is strict & not b₁ 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 b₁ being non empty SubSpace of Y st b₁ is maximal_discrete holds
b₁ is discrete

proof end;

cluster non empty non discrete -> non empty non maximal_discrete SubSpace of Y;
coherence
for b₁ being non empty SubSpace of Y st not b₁ is discrete holds
not b₁ 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 b₁ being SubSpace of X st b₁ is maximal_discrete holds
not b₁ is proper

proof end;

cluster proper -> non maximal_discrete SubSpace of X;
coherence
for b₁ being SubSpace of X st b₁ is proper holds
not b₁ is maximal_discrete ;
cluster non proper -> maximal_discrete SubSpace of X;
coherence
for b₁ being SubSpace of X st not b₁ is proper holds
b₁ is maximal_discrete

proof end;

cluster non maximal_discrete -> proper SubSpace of X;
coherence
for b₁ being SubSpace of X st not b₁ is maximal_discrete holds
b₁ 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 b₁ being non empty SubSpace of X st b₁ is maximal_discrete holds
b₁ is trivial ;
cluster non empty non trivial -> non empty non maximal_discrete SubSpace of X;
coherence
for b₁ being non empty SubSpace of X st not b₁ is trivial holds
not b₁ is maximal_discrete ;
cluster non empty trivial -> non empty maximal_discrete SubSpace of X;
coherence
for b₁ being non empty SubSpace of X st b₁ is trivial holds
b₁ is maximal_discrete

proof end;

cluster non empty non maximal_discrete -> non empty non trivial SubSpace of X;
coherence
for b₁ being non empty SubSpace of X st not b₁ is maximal_discrete holds
not b₁ is trivial ;

end;

begin

scheme :: TEX_2:sch 1
ExChoiceFCol{ F₁() -> non empty TopStruct , F₂() -> Subset-Family of F₁(), P₁[ set , set ] } :

ex f being Function of F₂(), the carrier of F₁() st
for S being Subset of F₁() st S in F₂() holds
P₁[S,f . S]

provided

A1: for S being Subset of F₁() st S in F₂() holds
ex x being Point of F₁() st P₁[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 b₁ being non empty SubSpace of X st b₁ is maximal_discrete holds
b₁ is proper

proof end;

cluster non empty non proper -> non empty non maximal_discrete SubSpace of X;
coherence
for b₁ being non empty SubSpace of X st not b₁ is proper holds
not b₁ 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 b₁ being non empty SubSpace of X st b₁ is maximal_discrete holds
not b₁ is trivial

proof end;

cluster non empty trivial -> non empty non maximal_discrete SubSpace of X;
coherence
for b₁ being non empty SubSpace of X st b₁ is trivial holds
not b₁ 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 b₁ being SubSpace of X st
( b₁ is maximal_discrete & b₁ is strict & not b₁ is empty & not b₁ 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;