:: by Zbigniew Karno

::

:: Received November 5, 1993

:: Copyright (c) 1993-2016 Association of Mizar Users

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

registration

let S be 1 -element set ;

coherence

for b_{1} being Subset of S st b_{1} is proper holds

b_{1} is empty

for b_{1} being Subset of S st not b_{1} is empty holds

not b_{1} is proper
;

end;
coherence

for b

b

proof end;

coherence for b

not b

theorem :: TEX_2:3

registration

let S be 1 -element set ;

coherence

for b_{1} being non empty Subset of S st not b_{1} is proper holds

b_{1} is trivial
;

end;
coherence

for b

b

registration

let S be non trivial set ;

coherence

for b_{1} being non empty Subset of S st b_{1} is trivial holds

b_{1} is proper
;

coherence

for b_{1} being non empty Subset of S st not b_{1} is proper holds

not b_{1} is trivial
;

end;
coherence

for b

b

coherence

for b

not b

registration

let S be non trivial set ;

existence

ex b_{1} being non empty Subset of S st

( b_{1} is trivial & b_{1} is proper )

ex b_{1} being non empty Subset of S st

( not b_{1} is trivial & not b_{1} is proper )

end;
existence

ex b

( b

proof end;

existence ex b

( not b

proof end;

theorem :: TEX_2:5

registration

let Y be 1 -element 1-sorted ;

coherence

for b_{1} being non empty Subset of Y holds not b_{1} is proper
;

coherence

for b_{1} being non empty Subset of Y st not b_{1} is proper holds

b_{1} is trivial
;

end;
coherence

for b

coherence

for b

b

registration

let Y be non trivial 1-sorted ;

coherence

for b_{1} being non empty Subset of Y st b_{1} is trivial holds

b_{1} is proper
;

coherence

for b_{1} being non empty Subset of Y st not b_{1} is proper holds

not b_{1} is trivial
;

end;
coherence

for b

b

coherence

for b

not b

registration

let Y be non trivial 1-sorted ;

existence

ex b_{1} being non empty Subset of Y st

( b_{1} is trivial & b_{1} is proper )

ex b_{1} being non empty Subset of Y st

( not b_{1} is trivial & not b_{1} is proper )

end;
existence

ex b

( b

proof end;

existence ex b

( not b

proof end;

registration

let Y be non trivial 1-sorted ;

existence

ex b_{1} being Subset of Y st

( not b_{1} is empty & b_{1} is trivial & b_{1} is proper )

end;
existence

ex b

( not b

proof end;

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

Y1 is TopSpace-like ;

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

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

Lm1: now :: thesis: for Z being TopStruct

for Z0 being SubSpace of Z holds the carrier of Z0 is Subset of Z

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

theorem :: TEX_2:9

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

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 ;

coherence

for b_{1} being non empty SubSpace of Y holds not b_{1} is proper

for b_{1} being non empty SubSpace of Y st not b_{1} is proper holds

b_{1} is trivial
;

end;
coherence

for b

proof end;

coherence for b

b

registration

let Y be non trivial TopStruct ;

coherence

for b_{1} being non empty SubSpace of Y st b_{1} is trivial holds

b_{1} is proper
;

coherence

for b_{1} being non empty SubSpace of Y st not b_{1} is proper holds

not b_{1} is trivial
;

end;
coherence

for b

b

coherence

for b

not b

registration

let Y be non empty TopStruct ;

existence

ex b_{1} being SubSpace of Y st

( not b_{1} is proper & b_{1} is strict & not b_{1} is empty )

end;
existence

ex b

( not b

proof 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 #)

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 ;

coherence

for b_{1} being SubSpace of Y st b_{1} is discrete holds

b_{1} is TopSpace-like
;

coherence

for b_{1} being SubSpace of Y st b_{1} is anti-discrete holds

b_{1} is TopSpace-like
;

coherence

for b_{1} being SubSpace of Y st not b_{1} is TopSpace-like holds

not b_{1} is discrete
;

coherence

for b_{1} being SubSpace of Y st not b_{1} is TopSpace-like holds

not b_{1} is anti-discrete
;

end;
coherence

for b

b

coherence

for b

b

coherence

for b

not b

coherence

for b

not b

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

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

Y1 is anti-discrete

proof end;

registration

let Y be non empty TopStruct ;

coherence

for b_{1} being SubSpace of Y st b_{1} is discrete holds

b_{1} is almost_discrete
;

coherence

for b_{1} being SubSpace of Y st not b_{1} is almost_discrete holds

not b_{1} is discrete
;

coherence

for b_{1} being SubSpace of Y st b_{1} is anti-discrete holds

b_{1} is almost_discrete
;

coherence

for b_{1} being SubSpace of Y st not b_{1} is almost_discrete holds

not b_{1} is anti-discrete
;

end;
coherence

for b

b

coherence

for b

not b

coherence

for b

b

coherence

for b

not b

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

Y1 is almost_discrete

proof end;

registration

let Y be non empty TopStruct ;

coherence

for b_{1} being non empty SubSpace of Y st b_{1} is discrete & b_{1} is anti-discrete holds

b_{1} is trivial
;

coherence

for b_{1} being non empty SubSpace of Y st b_{1} is anti-discrete & not b_{1} is trivial holds

not b_{1} is discrete
;

coherence

for b_{1} being non empty SubSpace of Y st b_{1} is discrete & not b_{1} is trivial holds

not b_{1} is anti-discrete
;

end;
coherence

for b

b

coherence

for b

not b

coherence

for b

not b

definition

let Y be non empty TopStruct ;

let y be Point of Y;

ex b_{1} being non empty strict SubSpace of Y st the carrier of b_{1} = {y}

for b_{1}, b_{2} being non empty strict SubSpace of Y st the carrier of b_{1} = {y} & the carrier of b_{2} = {y} holds

b_{1} = b_{2}

end;
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 the carrier of it = {y};

ex b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines Sspace TEX_2:def 2 :

for Y being non empty TopStruct

for y being Point of Y

for b_{3} being non empty strict SubSpace of Y holds

( b_{3} = Sspace y iff the carrier of b_{3} = {y} );

for Y being non empty TopStruct

for y being Point of Y

for b

( b

Lm2: now :: thesis: for Y being non empty TopStruct

for y being Point of Y holds Sspace y is 1 -element

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

registration

let Y be non empty TopStruct ;

existence

ex b_{1} being SubSpace of Y st

( b_{1} is strict & b_{1} is 1 -element )

end;
existence

ex b

( b

proof end;

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

for y being Point of Y holds

( Sspace y is proper iff {y} is proper )

proof end;

theorem :: TEX_2:16

registration

let Y be non trivial TopStruct ;

existence

ex b_{1} being non empty SubSpace of Y st

( b_{1} is proper & b_{1} is trivial & b_{1} is strict )

end;
existence

ex b

( b

proof end;

registration

let Y be non empty TopStruct ;

existence

ex b_{1} being SubSpace of Y st b_{1} is 1 -element

end;
existence

ex b

proof 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) #)

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

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 ;

coherence

for b_{1} being non empty SubSpace of Y st b_{1} is trivial & b_{1} is TopSpace-like holds

( b_{1} is discrete & b_{1} is anti-discrete )
;

end;
coherence

for b

( b

registration

let X be non empty TopSpace;

existence

ex b_{1} being SubSpace of X st

( b_{1} is trivial & b_{1} is strict & b_{1} is TopSpace-like & not b_{1} is empty )

end;
existence

ex b

( b

proof end;

registration
end;

registration

let X be non empty TopSpace;

existence

ex b_{1} being SubSpace of X st

( b_{1} is discrete & b_{1} is anti-discrete & b_{1} is strict & not b_{1} is empty )

end;
existence

ex b

( b

proof end;

registration

let X be non empty TopSpace;

let x be Point of X;

coherence

( Sspace x is discrete & Sspace x is anti-discrete ) ;

end;
let x be Point of X;

coherence

( Sspace x is discrete & Sspace x is anti-discrete ) ;

registration

let X be non empty TopSpace;

coherence

for b_{1} being SubSpace of X st not b_{1} is proper holds

( b_{1} is open & b_{1} is closed )

for b_{1} being SubSpace of X st not b_{1} is open holds

b_{1} is proper
;

coherence

for b_{1} being SubSpace of X st not b_{1} is closed holds

b_{1} is proper
;

end;
coherence

for b

( b

proof end;

coherence for b

b

coherence

for b

b

registration

let X be non empty TopSpace;

existence

ex b_{1} being SubSpace of X st

( b_{1} is open & b_{1} is closed & b_{1} is strict )

end;
existence

ex b

( b

proof end;

registration

let X be non empty discrete TopSpace;

coherence

for b_{1} being non empty SubSpace of X st b_{1} is anti-discrete holds

b_{1} is trivial
;

coherence

for b_{1} being non empty SubSpace of X st not b_{1} is trivial holds

not b_{1} is anti-discrete
;

end;
coherence

for b

b

coherence

for b

not b

registration

let X be non trivial discrete TopSpace;

existence

ex b_{1} being SubSpace of X st

( b_{1} is discrete & b_{1} is open & b_{1} is closed & b_{1} is proper & b_{1} is strict )

end;
existence

ex b

( b

proof end;

registration

let X be non empty anti-discrete TopSpace;

coherence

for b_{1} being non empty SubSpace of X st b_{1} is discrete holds

b_{1} is trivial
;

coherence

for b_{1} being non empty SubSpace of X st not b_{1} is trivial holds

not b_{1} is discrete
;

end;
coherence

for b

b

coherence

for b

not b

registration

let X be non trivial anti-discrete TopSpace;

coherence

for b_{1} being non empty proper SubSpace of X holds

( not b_{1} is open & not b_{1} is closed )

for b_{1} being non empty discrete SubSpace of X holds

( b_{1} is trivial & b_{1} is proper )
;

end;
coherence

for b

( not b

proof end;

coherence for b

( b

registration

let X be non trivial anti-discrete TopSpace;

ex b_{1} being SubSpace of X st

( b_{1} is anti-discrete & not b_{1} is open & not b_{1} is closed & b_{1} is proper & b_{1} is strict )

end;
cluster strict TopSpace-like non closed non open anti-discrete almost_discrete proper for SubSpace of X;

existence ex b

( b

proof end;

registration

let X be non trivial almost_discrete TopSpace;

existence

ex b_{1} being SubSpace of X st

( b_{1} is almost_discrete & b_{1} is proper & b_{1} is strict & not b_{1} is empty )

end;
existence

ex b

( b

proof end;

:: 3. Maximal Discrete Subsets and Subspaces.

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

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;

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

end;
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 for D being Subset of Y st D c= A holds

ex F being Subset of Y st

( F is closed & A /\ F = D );

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

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

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

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 )

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 )

for A being Subset of Y st A = the carrier of Y holds

( A is discrete iff Y 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

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

( 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

( 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} )

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

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

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

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

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

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

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 )

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

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;

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

( IT is discrete & ( for D being Subset of Y st D is discrete & IT c= D holds

IT = D ) );

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

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

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

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

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 )

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 )

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;

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

for A being Subset of Y st A = the carrier of IT holds

A is maximal_discrete ;

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

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

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 ;

coherence

for b_{1} being non empty SubSpace of Y st b_{1} is maximal_discrete holds

b_{1} is discrete

for b_{1} being non empty SubSpace of Y st not b_{1} is discrete holds

not b_{1} is maximal_discrete
;

end;
coherence

for b

b

proof end;

coherence for b

not b

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

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 )

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;

coherence

for b_{1} being SubSpace of X st b_{1} is maximal_discrete holds

not b_{1} is proper

for b_{1} being SubSpace of X st b_{1} is proper holds

not b_{1} is maximal_discrete
;

coherence

for b_{1} being SubSpace of X st not b_{1} is proper holds

b_{1} is maximal_discrete
by Th43;

coherence

for b_{1} being SubSpace of X st not b_{1} is maximal_discrete holds

b_{1} is proper
;

end;
coherence

for b

not b

proof end;

coherence for b

not b

coherence

for b

b

coherence

for b

b

registration

let X be non empty anti-discrete TopSpace;

coherence

for b_{1} being non empty SubSpace of X st b_{1} is maximal_discrete holds

b_{1} is trivial
;

coherence

for b_{1} being non empty SubSpace of X st not b_{1} is trivial holds

not b_{1} is maximal_discrete
;

coherence

for b_{1} being non empty SubSpace of X st b_{1} is trivial holds

b_{1} is maximal_discrete
by Th44;

coherence

for b_{1} being non empty SubSpace of X st not b_{1} is maximal_discrete holds

not b_{1} is trivial
;

end;
coherence

for b

b

coherence

for b

not b

coherence

for b

b

coherence

for b

not b

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 }

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}

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

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

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

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

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

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

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

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

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

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 )

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

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;

coherence

for b_{1} being non empty SubSpace of X st b_{1} is maximal_discrete holds

b_{1} is proper

for b_{1} being non empty SubSpace of X st not b_{1} is proper holds

not b_{1} is maximal_discrete
;

end;
coherence

for b

b

proof end;

coherence for b

not b

registration

let X be non empty non anti-discrete almost_discrete TopSpace;

coherence

for b_{1} being non empty SubSpace of X st b_{1} is maximal_discrete holds

not b_{1} is trivial

for b_{1} being non empty SubSpace of X st b_{1} is trivial holds

not b_{1} is maximal_discrete
;

end;
coherence

for b

not b

proof end;

coherence for b

not b

registration

let X be non empty almost_discrete TopSpace;

existence

ex b_{1} being SubSpace of X st

( b_{1} is maximal_discrete & b_{1} is strict & not b_{1} is empty & not b_{1} is empty )

end;
existence

ex b

( b

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

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

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

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

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

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

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

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

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

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;

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

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

for X0 being non empty discrete SubSpace of X holds X0 is_a_retract_of X

proof end;