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

:: 1. Proper Subsets of 1-sorted Structures.

theorem Th1: :: TEX_2:1

for A being non empty set
for B being 1 -element set st A c= B holds
A = B

proof end;

theorem :: TEX_2:2

for A being 1 -element set
for B being set st not A /\ B is empty holds
A c= B

proof end;

registration

let S be 1 -element set ;

cluster proper -> empty for Element of bool S;

coherence
for b₁ being Subset of S st b₁ is proper holds
b₁ is empty

proof end;

cluster non empty -> non proper for Element of bool S;

coherence
for b₁ being Subset of S st not b₁ is empty holds
not b₁ is proper ;

end;

theorem :: TEX_2:3

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

theorem :: TEX_2:4

for S being non trivial set
for y being Element of S holds {y} is proper ;

registration

let S be 1 -element set ;

cluster non empty non proper -> non empty trivial for Element of bool 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 trivial set ;

cluster non empty trivial -> non empty proper for Element of bool S;

coherence
for b₁ being non empty Subset of S st b₁ is trivial holds
b₁ is proper ;

cluster non empty non proper -> non empty non trivial for Element of bool 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 trivial set ;

cluster non empty trivial proper for Element of bool 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 for Element of bool 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:5

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

for Y being non trivial 1-sorted
for y being Element of Y holds {y} is proper ;

registration

let Y be 1 -element 1-sorted ;

cluster non empty -> non empty non proper for Element of bool 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 for Element of bool 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 trivial 1-sorted ;

cluster non empty trivial -> non empty proper for Element of bool 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 for Element of bool 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 trivial 1-sorted ;

cluster non empty trivial proper for Element of bool 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 for Element of bool 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 trivial 1-sorted ;

cluster non empty trivial proper for Element of bool 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;

:: 2. Proper Subspaces of Topological Spaces.

theorem :: TEX_2:7

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 ;

definition

let Y be TopStruct ;
let IT be SubSpace of Y;

attr IT is proper means :Def1: :: TEX_2:def 1
for A being Subset of Y st A = the carrier of IT holds
A is proper ;

end;

:: deftheorem Def1 defines proper TEX_2:def 1 :
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 :: TEX_2:8

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

Lm1: now :: thesis: for Z being TopStruct
for Z0 being SubSpace of Z holds the carrier of Z0 is Subset of Z

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 4;
hence the carrier of Z0 is Subset of Z ; :: thesis: verum

end;

theorem :: TEX_2:9

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 ;

theorem :: TEX_2:10

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 1 -element TopStruct ;

cluster non empty -> non empty non proper for 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 for SubSpace of Y;

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

end;

registration

let Y be non trivial TopStruct ;

cluster non empty trivial -> non empty proper for SubSpace of Y;

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

cluster non empty non proper -> non empty non trivial for 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 for 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:11

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 for SubSpace of Y;

coherence
for b₁ being SubSpace of Y st b₁ is discrete holds
b₁ is TopSpace-like ;

cluster anti-discrete -> TopSpace-like for 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 for 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 for SubSpace of Y;

coherence
for b₁ being SubSpace of Y st not b₁ is TopSpace-like holds
not b₁ is anti-discrete ;

end;

theorem Th12: :: 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 discrete holds
Y1 is discrete

proof end;

theorem :: TEX_2:13

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 for 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 for 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 for 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 for 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:14

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 for 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 for 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 for 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 :Def2: :: TEX_2:def 2
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 Def2 defines Sspace TEX_2:def 2 :
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 :: thesis: for Y being non empty TopStruct
for y being Point of Y holds Sspace y is 1 -element

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

end;

registration

let Y be non empty TopStruct ;

cluster 1 -element strict for SubSpace of Y;

existence
ex b₁ being SubSpace of Y st
( b₁ is strict & b₁ is 1 -element )

proof end;

end;

registration

let Y be non empty TopStruct ;
let y be Point of Y;

cluster Sspace y -> non empty 1 -element strict ;

coherence
Sspace y is 1 -element by Lm2;

end;

theorem :: TEX_2:15

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

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 trivial TopStruct ;

cluster non empty trivial strict proper for 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;

registration

let Y be non empty TopStruct ;

cluster 1 -element for SubSpace of Y;

existence
ex b₁ being SubSpace of Y st b₁ is 1 -element

proof end;

end;

theorem :: TEX_2:17

for Y being non empty TopStruct
for Y0 being 1 -element 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:18

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 for 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 for 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 for 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 for 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 for SubSpace of X;

coherence
for b₁ being SubSpace of X st not b₁ is open holds
b₁ is proper ;

cluster non closed -> proper for 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 for 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 for 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 for 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 trivial discrete TopSpace;

cluster strict TopSpace-like closed open discrete almost_discrete proper for 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 for 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 for 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 trivial anti-discrete TopSpace;

cluster non empty proper -> non empty non closed non open proper for 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 for 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 trivial anti-discrete TopSpace;

cluster strict TopSpace-like non closed non open anti-discrete almost_discrete proper for 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 trivial almost_discrete TopSpace;

cluster non empty strict TopSpace-like almost_discrete proper for 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;

:: 3. Maximal Discrete Subsets and Subspaces.

definition

let Y be TopStruct ;
let IT be Subset of Y;

attr IT is discrete means :: TEX_2:def 3
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 defines discrete TEX_2:def 3 :
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 :: TEX_2:def 4
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 defines discrete TEX_2:def 4 :
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 Th19: :: TEX_2:19

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 Th20: :: TEX_2:20

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 Th21: :: TEX_2:21

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 Th22: :: TEX_2:22

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

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 Th24: :: TEX_2:24

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 Th25: :: TEX_2:25

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 Th26: :: TEX_2:26

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

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 Th28: :: TEX_2:28

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 Th29: :: TEX_2:29

for X being non empty TopSpace
for A being empty Subset of X holds A is discrete

proof end;

theorem Th30: :: TEX_2:30

for X being non empty TopSpace
for x being Point of X holds {x} is discrete

proof end;

theorem Th31: :: TEX_2:31

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

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

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

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 Th35: :: TEX_2:35

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 Th36: :: TEX_2:36

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} by ZFMISC_1:31, Th35;

theorem :: TEX_2:37

for X being non empty discrete TopSpace
for A being Subset of X holds A is discrete

proof end;

theorem Th38: :: TEX_2:38

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 :: TEX_2:def 5
( IT is discrete & ( for D being Subset of Y st D is discrete & IT c= D holds
IT = D ) );

end;

:: deftheorem defines maximal_discrete TEX_2:def 5 :
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:39

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 Th40: :: TEX_2:40

for X being non empty TopSpace
for A being empty Subset of X holds not A is maximal_discrete

proof end;

theorem Th41: :: TEX_2:41

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

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 Th43: :: TEX_2:43

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 Th44: :: TEX_2:44

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 :: TEX_2:def 6
for A being Subset of Y st A = the carrier of IT holds
A is maximal_discrete ;

end;

:: deftheorem defines maximal_discrete TEX_2:def 6 :
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 Th45: :: TEX_2:45

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

registration

let Y be non empty TopStruct ;

cluster non empty maximal_discrete -> non empty discrete for 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 for 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:46

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 Th47: :: TEX_2:47

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 for 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 for 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 for SubSpace of X;

coherence
for b₁ being SubSpace of X st not b₁ is proper holds
b₁ is maximal_discrete by Th43;

cluster non maximal_discrete -> proper for 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 for 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 for 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 for SubSpace of X;

coherence
for b₁ being non empty SubSpace of X st b₁ is trivial holds
b₁ is maximal_discrete by Th44;

cluster non empty non maximal_discrete -> non empty non trivial for SubSpace of X;

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

end;

:: 4. Maximal Discrete Subspaces of Almost Discrete Spaces.

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

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 Th48: :: TEX_2:48

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 Th49: :: TEX_2:49

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 Th50: :: TEX_2:50

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 Th51: :: TEX_2:51

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 Th52: :: TEX_2:52

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

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 Th54: :: TEX_2:54

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

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 Th56: :: TEX_2:56

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 Th57: :: TEX_2:57

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 Th58: :: TEX_2:58

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 Th59: :: TEX_2:59

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 Th60: :: TEX_2:60

for X being non empty almost_discrete TopSpace ex M being Subset of X st M is maximal_discrete

proof end;

theorem Th61: :: TEX_2:61

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

theorem Th62: :: TEX_2:62

for X being discrete TopSpace
for Y being TopSpace
for f being Function of X,Y holds f is continuous by TDLAT_3:16;

theorem :: TEX_2:63

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

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

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 Th66: :: TEX_2:66

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

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 Th68: :: TEX_2:68

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

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 Th70: :: TEX_2:70

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

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

theorem Th72: :: TEX_2:72

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

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;