:: by Zbigniew Karno

::

:: Received November 9, 1993

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

theorem Th1: :: TEX_3:1

for X being non empty TopSpace

for A, B being Subset of X st A,B constitute_a_decomposition holds

( not A is empty iff B is proper )

for A, B being Subset of X st A,B constitute_a_decomposition holds

( not A is empty iff B is proper )

proof end;

Lm1: for X being non empty TopSpace

for A, B being Subset of X st A is everywhere_dense & B is everywhere_dense holds

A meets B

proof end;

Lm2: for X being non empty TopSpace

for A, B being Subset of X st ( ( A is everywhere_dense & B is dense ) or ( A is dense & B is everywhere_dense ) ) holds

A meets B

proof end;

theorem Th2: :: TEX_3:2

for X being non empty TopSpace

for A, B being Subset of X st A,B constitute_a_decomposition holds

( A is dense iff B is boundary )

for A, B being Subset of X st A,B constitute_a_decomposition holds

( A is dense iff B is boundary )

proof end;

theorem :: TEX_3:3

theorem Th4: :: TEX_3:4

for X being non empty TopSpace

for A, B being Subset of X st A,B constitute_a_decomposition holds

( A is everywhere_dense iff B is nowhere_dense )

for A, B being Subset of X st A,B constitute_a_decomposition holds

( A is everywhere_dense iff B is nowhere_dense )

proof end;

theorem :: TEX_3:5

for X being non empty TopSpace

for A, B being Subset of X st A,B constitute_a_decomposition holds

( A is nowhere_dense iff B is everywhere_dense ) by Th4;

for A, B being Subset of X st A,B constitute_a_decomposition holds

( A is nowhere_dense iff B is everywhere_dense ) by Th4;

theorem Th6: :: TEX_3:6

for X being non empty TopSpace

for Y1, Y2 being non empty SubSpace of X st Y1,Y2 constitute_a_decomposition holds

( Y1 is proper & Y2 is proper )

for Y1, Y2 being non empty SubSpace of X st Y1,Y2 constitute_a_decomposition holds

( Y1 is proper & Y2 is proper )

proof end;

theorem :: TEX_3:7

for X being non trivial TopSpace

for D being non empty proper Subset of X ex Y0 being non empty strict proper SubSpace of X st D = the carrier of Y0

for D being non empty proper Subset of X ex Y0 being non empty strict proper SubSpace of X st D = the carrier of Y0

proof end;

theorem Th8: :: TEX_3:8

for X being non trivial TopSpace

for Y1 being non empty proper SubSpace of X ex Y2 being non empty strict proper SubSpace of X st Y1,Y2 constitute_a_decomposition

for Y1 being non empty proper SubSpace of X ex Y2 being non empty strict proper SubSpace of X st Y1,Y2 constitute_a_decomposition

proof end;

:: 2. Dense and Everywhere Dense Subspaces.

:: deftheorem Def1 defines dense TEX_3:def 1 :

for X being non empty TopSpace

for IT being SubSpace of X holds

( IT is dense iff for A being Subset of X st A = the carrier of IT holds

A is dense );

for X being non empty TopSpace

for IT being SubSpace of X holds

( IT is dense iff for A being Subset of X st A = the carrier of IT holds

A is dense );

registration

let X be non empty TopSpace;

coherence

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

not b_{1} is proper

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

not b_{1} is closed
;

coherence

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

not b_{1} is dense
;

end;
coherence

for b

not b

proof end;

coherence for b

not b

coherence

for b

not b

registration

let X be non empty TopSpace;

existence

ex b_{1} being SubSpace of X st

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

end;
existence

ex b

( b

proof end;

::Properties of Dense Subspaces.

theorem Th10: :: TEX_3:10

for X being non empty TopSpace

for A0 being non empty Subset of X st A0 is dense holds

ex X0 being non empty strict dense SubSpace of X st A0 = the carrier of X0

for A0 being non empty Subset of X st A0 is dense holds

ex X0 being non empty strict dense SubSpace of X st A0 = the carrier of X0

proof end;

theorem :: TEX_3:11

for X being non empty TopSpace

for X0 being non empty dense SubSpace of X

for A being Subset of X

for B being Subset of X0 st A = B holds

( B is dense iff A is dense )

for X0 being non empty dense SubSpace of X

for A being Subset of X

for B being Subset of X0 st A = B holds

( B is dense iff A is dense )

proof end;

theorem :: TEX_3:12

for X being non empty TopSpace

for X1 being dense SubSpace of X

for X2 being SubSpace of X st X1 is SubSpace of X2 holds

X2 is dense

for X1 being dense SubSpace of X

for X2 being SubSpace of X st X1 is SubSpace of X2 holds

X2 is dense

proof end;

theorem :: TEX_3:13

for X being non empty TopSpace

for X1 being non empty dense SubSpace of X

for X2 being non empty SubSpace of X st X1 is SubSpace of X2 holds

X1 is dense SubSpace of X2

for X1 being non empty dense SubSpace of X

for X2 being non empty SubSpace of X st X1 is SubSpace of X2 holds

X1 is dense SubSpace of X2

proof end;

theorem :: TEX_3:14

for X being non empty TopSpace

for X1 being non empty dense SubSpace of X

for X2 being non empty dense SubSpace of X1 holds X2 is non empty dense SubSpace of X

for X1 being non empty dense SubSpace of X

for X2 being non empty dense SubSpace of X1 holds X2 is non empty dense SubSpace of X

proof end;

theorem :: TEX_3:15

for X, Y1, Y2 being non empty TopSpace st Y2 = TopStruct(# the carrier of Y1, the topology of Y1 #) holds

( Y1 is dense SubSpace of X iff Y2 is dense SubSpace of X )

( Y1 is dense SubSpace of X iff Y2 is dense SubSpace of X )

proof end;

definition

let X be non empty TopSpace;

let IT be SubSpace of X;

end;
let IT be SubSpace of X;

attr IT is everywhere_dense means :Def2: :: TEX_3:def 2

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

A is everywhere_dense ;

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

A is everywhere_dense ;

:: deftheorem Def2 defines everywhere_dense TEX_3:def 2 :

for X being non empty TopSpace

for IT being SubSpace of X holds

( IT is everywhere_dense iff for A being Subset of X st A = the carrier of IT holds

A is everywhere_dense );

for X being non empty TopSpace

for IT being SubSpace of X holds

( IT is everywhere_dense iff for A being Subset of X st A = the carrier of IT holds

A is everywhere_dense );

theorem Th16: :: TEX_3:16

for X being non empty TopSpace

for X0 being SubSpace of X

for A being Subset of X st A = the carrier of X0 holds

( X0 is everywhere_dense iff A is everywhere_dense ) ;

for X0 being SubSpace of X

for A being Subset of X st A = the carrier of X0 holds

( X0 is everywhere_dense iff A is everywhere_dense ) ;

registration

let X be non empty TopSpace;

coherence

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

b_{1} is dense
by TOPS_3:33;

coherence

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

not b_{1} is everywhere_dense
;

coherence

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

b_{1} is everywhere_dense

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

b_{1} is proper
;

end;
coherence

for b

b

coherence

for b

not b

coherence

for b

b

proof end;

coherence for b

b

registration

let X be non empty TopSpace;

existence

ex b_{1} being SubSpace of X st

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

end;
existence

ex b

( b

proof end;

::Properties of Everywhere Dense Subspaces.

theorem Th17: :: TEX_3:17

for X being non empty TopSpace

for A0 being non empty Subset of X st A0 is everywhere_dense holds

ex X0 being non empty strict everywhere_dense SubSpace of X st A0 = the carrier of X0

for A0 being non empty Subset of X st A0 is everywhere_dense holds

ex X0 being non empty strict everywhere_dense SubSpace of X st A0 = the carrier of X0

proof end;

theorem :: TEX_3:18

for X being non empty TopSpace

for X0 being non empty everywhere_dense SubSpace of X

for A being Subset of X

for B being Subset of X0 st A = B holds

( B is everywhere_dense iff A is everywhere_dense )

for X0 being non empty everywhere_dense SubSpace of X

for A being Subset of X

for B being Subset of X0 st A = B holds

( B is everywhere_dense iff A is everywhere_dense )

proof end;

theorem :: TEX_3:19

for X being non empty TopSpace

for X1 being everywhere_dense SubSpace of X

for X2 being SubSpace of X st X1 is SubSpace of X2 holds

X2 is everywhere_dense

for X1 being everywhere_dense SubSpace of X

for X2 being SubSpace of X st X1 is SubSpace of X2 holds

X2 is everywhere_dense

proof end;

theorem :: TEX_3:20

for X being non empty TopSpace

for X1 being non empty everywhere_dense SubSpace of X

for X2 being non empty SubSpace of X st X1 is SubSpace of X2 holds

X1 is everywhere_dense SubSpace of X2

for X1 being non empty everywhere_dense SubSpace of X

for X2 being non empty SubSpace of X st X1 is SubSpace of X2 holds

X1 is everywhere_dense SubSpace of X2

proof end;

theorem :: TEX_3:21

for X being non empty TopSpace

for X1 being non empty everywhere_dense SubSpace of X

for X2 being non empty everywhere_dense SubSpace of X1 holds X2 is everywhere_dense SubSpace of X

for X1 being non empty everywhere_dense SubSpace of X

for X2 being non empty everywhere_dense SubSpace of X1 holds X2 is everywhere_dense SubSpace of X

proof end;

theorem :: TEX_3:22

for X, Y1, Y2 being non empty TopSpace st Y2 = TopStruct(# the carrier of Y1, the topology of Y1 #) holds

( Y1 is everywhere_dense SubSpace of X iff Y2 is everywhere_dense SubSpace of X )

( Y1 is everywhere_dense SubSpace of X iff Y2 is everywhere_dense SubSpace of X )

proof end;

registration

let X be non empty TopSpace;

coherence

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

b_{1} is everywhere_dense

for b_{1} being SubSpace of X st b_{1} is dense & not b_{1} is everywhere_dense holds

not b_{1} is open
;

coherence

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

not b_{1} is dense
;

end;
coherence

for b

b

proof end;

coherence for b

not b

coherence

for b

not b

registration

let X be non empty TopSpace;

existence

ex b_{1} being SubSpace of X st

( b_{1} is dense & b_{1} is open & b_{1} is strict & not b_{1} is empty )

end;
existence

ex b

( b

proof end;

::Properties of Dense Open Subspaces.

theorem Th23: :: TEX_3:23

for X being non empty TopSpace

for A0 being non empty Subset of X st A0 is dense & A0 is open holds

ex X0 being non empty strict open dense SubSpace of X st A0 = the carrier of X0

for A0 being non empty Subset of X st A0 is dense & A0 is open holds

ex X0 being non empty strict open dense SubSpace of X st A0 = the carrier of X0

proof end;

theorem :: TEX_3:24

for X being non empty TopSpace

for X0 being SubSpace of X holds

( X0 is everywhere_dense iff ex X1 being strict open dense SubSpace of X st X1 is SubSpace of X0 )

for X0 being SubSpace of X holds

( X0 is everywhere_dense iff ex X1 being strict open dense SubSpace of X st X1 is SubSpace of X0 )

proof end;

theorem :: TEX_3:25

for X being non empty TopSpace

for X1, X2 being non empty SubSpace of X st ( X1 is dense or X2 is dense ) holds

X1 union X2 is dense SubSpace of X

for X1, X2 being non empty SubSpace of X st ( X1 is dense or X2 is dense ) holds

X1 union X2 is dense SubSpace of X

proof end;

theorem :: TEX_3:26

for X being non empty TopSpace

for X1, X2 being non empty SubSpace of X st ( X1 is everywhere_dense or X2 is everywhere_dense ) holds

X1 union X2 is everywhere_dense SubSpace of X

for X1, X2 being non empty SubSpace of X st ( X1 is everywhere_dense or X2 is everywhere_dense ) holds

X1 union X2 is everywhere_dense SubSpace of X

proof end;

theorem :: TEX_3:27

for X being non empty TopSpace

for X1, X2 being non empty SubSpace of X st X1 is everywhere_dense & X2 is everywhere_dense holds

X1 meet X2 is everywhere_dense SubSpace of X

for X1, X2 being non empty SubSpace of X st X1 is everywhere_dense & X2 is everywhere_dense holds

X1 meet X2 is everywhere_dense SubSpace of X

proof end;

theorem :: TEX_3:28

for X being non empty TopSpace

for X1, X2 being non empty SubSpace of X st ( ( X1 is everywhere_dense & X2 is dense ) or ( X1 is dense & X2 is everywhere_dense ) ) holds

X1 meet X2 is dense SubSpace of X

for X1, X2 being non empty SubSpace of X st ( ( X1 is everywhere_dense & X2 is dense ) or ( X1 is dense & X2 is everywhere_dense ) ) holds

X1 meet X2 is dense SubSpace of X

proof end;

:: 3. Boundary and Nowhere Dense Subspaces.

:: deftheorem Def3 defines boundary TEX_3:def 3 :

for X being non empty TopSpace

for IT being SubSpace of X holds

( IT is boundary iff for A being Subset of X st A = the carrier of IT holds

A is boundary );

for X being non empty TopSpace

for IT being SubSpace of X holds

( IT is boundary iff for A being Subset of X st A = the carrier of IT holds

A is boundary );

registration

let X be non empty TopSpace;

coherence

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

not b_{1} is boundary

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

not b_{1} is open
;

coherence

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

not b_{1} is boundary

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

not b_{1} is everywhere_dense
;

end;
coherence

for b

not b

proof end;

coherence for b

not b

coherence

for b

not b

proof end;

coherence for b

not b

::Properties of Boundary Subspaces.

theorem Th30: :: TEX_3:30

for X being non empty TopSpace

for A0 being non empty Subset of X st A0 is boundary holds

ex X0 being strict SubSpace of X st

( X0 is boundary & A0 = the carrier of X0 )

for A0 being non empty Subset of X st A0 is boundary holds

ex X0 being strict SubSpace of X st

( X0 is boundary & A0 = the carrier of X0 )

proof end;

theorem Th31: :: TEX_3:31

for X being non empty TopSpace

for X1, X2 being SubSpace of X st X1,X2 constitute_a_decomposition holds

( X1 is dense iff X2 is boundary )

for X1, X2 being SubSpace of X st X1,X2 constitute_a_decomposition holds

( X1 is dense iff X2 is boundary )

proof end;

theorem :: TEX_3:32

theorem Th33: :: TEX_3:33

for X being non empty TopSpace

for X0 being SubSpace of X st X0 is boundary holds

for A being Subset of X st A c= the carrier of X0 holds

A is boundary

for X0 being SubSpace of X st X0 is boundary holds

for A being Subset of X st A c= the carrier of X0 holds

A is boundary

proof end;

definition

let X be non empty TopSpace;

let IT be SubSpace of X;

end;
let IT be SubSpace of X;

attr IT is nowhere_dense means :Def4: :: TEX_3:def 4

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

A is nowhere_dense ;

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

A is nowhere_dense ;

:: deftheorem Def4 defines nowhere_dense TEX_3:def 4 :

for X being non empty TopSpace

for IT being SubSpace of X holds

( IT is nowhere_dense iff for A being Subset of X st A = the carrier of IT holds

A is nowhere_dense );

for X being non empty TopSpace

for IT being SubSpace of X holds

( IT is nowhere_dense iff for A being Subset of X st A = the carrier of IT holds

A is nowhere_dense );

theorem Th35: :: TEX_3:35

for X being non empty TopSpace

for X0 being SubSpace of X

for A being Subset of X st A = the carrier of X0 holds

( X0 is nowhere_dense iff A is nowhere_dense ) ;

for X0 being SubSpace of X

for A being Subset of X st A = the carrier of X0 holds

( X0 is nowhere_dense iff A is nowhere_dense ) ;

registration

let X be non empty TopSpace;

coherence

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

b_{1} is boundary

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

not b_{1} is nowhere_dense
;

coherence

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

not b_{1} is dense

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

not b_{1} is nowhere_dense
;

end;
coherence

for b

b

proof end;

coherence for b

not b

coherence

for b

not b

proof end;

coherence for b

not b

::Properties of Nowhere Dense Subspaces.

theorem :: TEX_3:36

for X being non empty TopSpace

for A0 being non empty Subset of X st A0 is nowhere_dense holds

ex X0 being strict SubSpace of X st

( X0 is nowhere_dense & A0 = the carrier of X0 )

for A0 being non empty Subset of X st A0 is nowhere_dense holds

ex X0 being strict SubSpace of X st

( X0 is nowhere_dense & A0 = the carrier of X0 )

proof end;

theorem Th37: :: TEX_3:37

for X being non empty TopSpace

for X1, X2 being SubSpace of X st X1,X2 constitute_a_decomposition holds

( X1 is everywhere_dense iff X2 is nowhere_dense )

for X1, X2 being SubSpace of X st X1,X2 constitute_a_decomposition holds

( X1 is everywhere_dense iff X2 is nowhere_dense )

proof end;

theorem :: TEX_3:38

for X being non empty TopSpace

for X1, X2 being non empty SubSpace of X st X1,X2 constitute_a_decomposition holds

( X1 is nowhere_dense iff X2 is everywhere_dense ) by Th37;

for X1, X2 being non empty SubSpace of X st X1,X2 constitute_a_decomposition holds

( X1 is nowhere_dense iff X2 is everywhere_dense ) by Th37;

theorem Th39: :: TEX_3:39

for X being non empty TopSpace

for X0 being SubSpace of X st X0 is nowhere_dense holds

for A being Subset of X st A c= the carrier of X0 holds

A is nowhere_dense

for X0 being SubSpace of X st X0 is nowhere_dense holds

for A being Subset of X st A c= the carrier of X0 holds

A is nowhere_dense

proof end;

theorem Th40: :: TEX_3:40

for X being non empty TopSpace

for X1, X2 being SubSpace of X st X1 is nowhere_dense & X2 is SubSpace of X1 holds

X2 is nowhere_dense by TSEP_1:4, Th39;

for X1, X2 being SubSpace of X st X1 is nowhere_dense & X2 is SubSpace of X1 holds

X2 is nowhere_dense by TSEP_1:4, Th39;

registration

let X be non empty TopSpace;

coherence

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

b_{1} is nowhere_dense

for b_{1} being SubSpace of X st b_{1} is boundary & not b_{1} is nowhere_dense holds

not b_{1} is closed
;

coherence

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

not b_{1} is boundary
;

end;
coherence

for b

b

proof end;

coherence for b

not b

coherence

for b

not b

::Properties of Boundary Closed Subspaces.

theorem Th41: :: TEX_3:41

for X being non empty TopSpace

for A0 being non empty Subset of X st A0 is boundary & A0 is closed holds

ex X0 being non empty strict closed SubSpace of X st

( X0 is boundary & A0 = the carrier of X0 )

for A0 being non empty Subset of X st A0 is boundary & A0 is closed holds

ex X0 being non empty strict closed SubSpace of X st

( X0 is boundary & A0 = the carrier of X0 )

proof end;

theorem :: TEX_3:42

for X being non empty TopSpace

for X0 being non empty SubSpace of X holds

( X0 is nowhere_dense iff ex X1 being non empty strict closed SubSpace of X st

( X1 is boundary & X0 is SubSpace of X1 ) )

for X0 being non empty SubSpace of X holds

( X0 is nowhere_dense iff ex X1 being non empty strict closed SubSpace of X st

( X1 is boundary & X0 is SubSpace of X1 ) )

proof end;

theorem :: TEX_3:43

for X being non empty TopSpace

for X1, X2 being non empty SubSpace of X st ( X1 is boundary or X2 is boundary ) & X1 meets X2 holds

X1 meet X2 is boundary

for X1, X2 being non empty SubSpace of X st ( X1 is boundary or X2 is boundary ) & X1 meets X2 holds

X1 meet X2 is boundary

proof end;

theorem :: TEX_3:44

for X being non empty TopSpace

for X1, X2 being non empty SubSpace of X st X1 is nowhere_dense & X2 is nowhere_dense holds

X1 union X2 is nowhere_dense

for X1, X2 being non empty SubSpace of X st X1 is nowhere_dense & X2 is nowhere_dense holds

X1 union X2 is nowhere_dense

proof end;

theorem :: TEX_3:45

for X being non empty TopSpace

for X1, X2 being non empty SubSpace of X st ( ( X1 is nowhere_dense & X2 is boundary ) or ( X1 is boundary & X2 is nowhere_dense ) ) holds

X1 union X2 is boundary

for X1, X2 being non empty SubSpace of X st ( ( X1 is nowhere_dense & X2 is boundary ) or ( X1 is boundary & X2 is nowhere_dense ) ) holds

X1 union X2 is boundary

proof end;

theorem :: TEX_3:46

for X being non empty TopSpace

for X1, X2 being non empty SubSpace of X st ( X1 is nowhere_dense or X2 is nowhere_dense ) & X1 meets X2 holds

X1 meet X2 is nowhere_dense

for X1, X2 being non empty SubSpace of X st ( X1 is nowhere_dense or X2 is nowhere_dense ) & X1 meets X2 holds

X1 meet X2 is nowhere_dense

proof end;

:: 4. Dense and Boundary Subspaces of non Discrete Spaces.

theorem :: TEX_3:47

for X being non empty TopSpace st ( for X0 being SubSpace of X holds not X0 is boundary ) holds

X is discrete

X is discrete

proof end;

theorem :: TEX_3:48

for X being non trivial TopSpace st ( for X0 being proper SubSpace of X holds not X0 is dense ) holds

X is discrete

X is discrete

proof end;

registration

let X be non empty discrete TopSpace;

coherence

for b_{1} being non empty SubSpace of X holds not b_{1} is boundary
;

coherence

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

not b_{1} is dense
;

coherence

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

not b_{1} is proper
;

end;
coherence

for b

coherence

for b

not b

coherence

for b

not b

registration

let X be non empty discrete TopSpace;

ex b_{1} being SubSpace of X st

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

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

existence ex b

( not b

proof end;

registration

let X be non trivial discrete TopSpace;

existence

ex b_{1} being SubSpace of X st

( not b_{1} is dense & b_{1} is strict )

end;
existence

ex b

( not b

proof end;

theorem :: TEX_3:49

theorem :: TEX_3:50

registration

let X be non empty non discrete TopSpace;

existence

ex b_{1} being SubSpace of X st

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

ex b_{1} being SubSpace of X st

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

end;
existence

ex b

( b

proof end;

existence ex b

( b

proof end;

theorem :: TEX_3:51

for X being non empty non discrete TopSpace

for A0 being non empty Subset of X st A0 is boundary holds

ex X0 being strict boundary SubSpace of X st A0 = the carrier of X0

for A0 being non empty Subset of X st A0 is boundary holds

ex X0 being strict boundary SubSpace of X st A0 = the carrier of X0

proof end;

theorem :: TEX_3:52

for X being non empty non discrete TopSpace

for A0 being non empty proper Subset of X st A0 is dense holds

ex X0 being strict proper dense SubSpace of X st A0 = the carrier of X0

for A0 being non empty proper Subset of X st A0 is dense holds

ex X0 being strict proper dense SubSpace of X st A0 = the carrier of X0

proof end;

theorem :: TEX_3:53

for X being non empty non discrete TopSpace

for X1 being non empty boundary SubSpace of X ex X2 being non empty strict proper dense SubSpace of X st X1,X2 constitute_a_decomposition

for X1 being non empty boundary SubSpace of X ex X2 being non empty strict proper dense SubSpace of X st X1,X2 constitute_a_decomposition

proof end;

theorem :: TEX_3:54

for X being non empty non discrete TopSpace

for X1 being non empty proper dense SubSpace of X ex X2 being non empty strict boundary SubSpace of X st X1,X2 constitute_a_decomposition

for X1 being non empty proper dense SubSpace of X ex X2 being non empty strict boundary SubSpace of X st X1,X2 constitute_a_decomposition

proof end;

theorem :: TEX_3:55

for X being non empty non discrete TopSpace

for Y1, Y2 being non empty TopSpace st Y2 = TopStruct(# the carrier of Y1, the topology of Y1 #) holds

( Y1 is boundary SubSpace of X iff Y2 is boundary SubSpace of X )

for Y1, Y2 being non empty TopSpace st Y2 = TopStruct(# the carrier of Y1, the topology of Y1 #) holds

( Y1 is boundary SubSpace of X iff Y2 is boundary SubSpace of X )

proof end;

:: 5. Everywhere and Nowhere Dense Subspaces of non Almost Discrete Spaces.

theorem :: TEX_3:56

for X being non empty TopSpace st ( for X0 being SubSpace of X holds not X0 is nowhere_dense ) holds

X is almost_discrete

X is almost_discrete

proof end;

theorem :: TEX_3:57

for X being non trivial TopSpace st ( for X0 being proper SubSpace of X holds not X0 is everywhere_dense ) holds

X is almost_discrete

X is almost_discrete

proof end;

registration

let X be non empty almost_discrete TopSpace;

coherence

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

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

not b_{1} is everywhere_dense

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

not b_{1} is proper
;

coherence

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

not b_{1} is closed
;

coherence

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

not b_{1} is boundary
;

coherence

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

not b_{1} is open
;

coherence

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

not b_{1} is proper
;

coherence

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

not b_{1} is dense
;

end;
coherence

for b

proof end;

coherence for b

not b

proof end;

coherence for b

not b

coherence

for b

not b

coherence

for b

not b

coherence

for b

not b

coherence

for b

not b

coherence

for b

not b

registration

let X be non empty almost_discrete TopSpace;

existence

ex b_{1} being SubSpace of X st

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

end;
existence

ex b

( not b

proof end;

registration

let X be non trivial almost_discrete TopSpace;

existence

ex b_{1} being SubSpace of X st

( not b_{1} is everywhere_dense & b_{1} is strict )

end;
existence

ex b

( not b

proof end;

theorem :: TEX_3:58

for X being non empty TopSpace st ex X0 being non empty SubSpace of X st X0 is nowhere_dense holds

not X is almost_discrete ;

not X is almost_discrete ;

theorem :: TEX_3:59

theorem :: TEX_3:60

for X being non empty TopSpace st ex X0 being non empty SubSpace of X st

( X0 is everywhere_dense & X0 is proper ) holds

not X is almost_discrete ;

( X0 is everywhere_dense & X0 is proper ) holds

not X is almost_discrete ;

theorem :: TEX_3:61

registration

let X be non empty non almost_discrete TopSpace;

existence

ex b_{1} being SubSpace of X st

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

ex b_{1} being SubSpace of X st

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

end;
existence

ex b

( b

proof end;

existence ex b

( b

proof end;

theorem Th62: :: TEX_3:62

for X being non empty non almost_discrete TopSpace

for A0 being non empty Subset of X st A0 is nowhere_dense holds

ex X0 being non empty strict nowhere_dense SubSpace of X st A0 = the carrier of X0

for A0 being non empty Subset of X st A0 is nowhere_dense holds

ex X0 being non empty strict nowhere_dense SubSpace of X st A0 = the carrier of X0

proof end;

theorem :: TEX_3:63

for X being non empty non almost_discrete TopSpace

for A0 being non empty proper Subset of X st A0 is everywhere_dense holds

ex X0 being strict proper everywhere_dense SubSpace of X st A0 = the carrier of X0

for A0 being non empty proper Subset of X st A0 is everywhere_dense holds

ex X0 being strict proper everywhere_dense SubSpace of X st A0 = the carrier of X0

proof end;

theorem :: TEX_3:64

for X being non empty non almost_discrete TopSpace

for X1 being non empty nowhere_dense SubSpace of X ex X2 being non empty strict proper everywhere_dense SubSpace of X st X1,X2 constitute_a_decomposition

for X1 being non empty nowhere_dense SubSpace of X ex X2 being non empty strict proper everywhere_dense SubSpace of X st X1,X2 constitute_a_decomposition

proof end;

theorem :: TEX_3:65

for X being non empty non almost_discrete TopSpace

for X1 being non empty proper everywhere_dense SubSpace of X ex X2 being non empty strict nowhere_dense SubSpace of X st X1,X2 constitute_a_decomposition

for X1 being non empty proper everywhere_dense SubSpace of X ex X2 being non empty strict nowhere_dense SubSpace of X st X1,X2 constitute_a_decomposition

proof end;

theorem :: TEX_3:66

for X being non empty non almost_discrete TopSpace

for Y1, Y2 being non empty TopSpace st Y2 = TopStruct(# the carrier of Y1, the topology of Y1 #) holds

( Y1 is nowhere_dense SubSpace of X iff Y2 is nowhere_dense SubSpace of X )

for Y1, Y2 being non empty TopSpace st Y2 = TopStruct(# the carrier of Y1, the topology of Y1 #) holds

( Y1 is nowhere_dense SubSpace of X iff Y2 is nowhere_dense SubSpace of X )

proof end;

registration

let X be non empty non almost_discrete TopSpace;

existence

ex b_{1} being SubSpace of X st

( b_{1} is boundary & b_{1} is closed & b_{1} is strict & not b_{1} is empty )

ex b_{1} being SubSpace of X st

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

end;
existence

ex b

( b

proof end;

existence ex b

( b

proof end;

theorem Th67: :: TEX_3:67

for X being non empty non almost_discrete TopSpace

for A0 being non empty Subset of X st A0 is boundary & A0 is closed holds

ex X0 being non empty strict closed boundary SubSpace of X st A0 = the carrier of X0

for A0 being non empty Subset of X st A0 is boundary & A0 is closed holds

ex X0 being non empty strict closed boundary SubSpace of X st A0 = the carrier of X0

proof end;

theorem :: TEX_3:68

for X being non empty non almost_discrete TopSpace

for A0 being non empty proper Subset of X st A0 is dense & A0 is open holds

ex X0 being strict open proper dense SubSpace of X st A0 = the carrier of X0

for A0 being non empty proper Subset of X st A0 is dense & A0 is open holds

ex X0 being strict open proper dense SubSpace of X st A0 = the carrier of X0

proof end;

theorem :: TEX_3:69

for X being non empty non almost_discrete TopSpace

for X1 being non empty closed boundary SubSpace of X ex X2 being non empty strict open proper dense SubSpace of X st X1,X2 constitute_a_decomposition

for X1 being non empty closed boundary SubSpace of X ex X2 being non empty strict open proper dense SubSpace of X st X1,X2 constitute_a_decomposition

proof end;

theorem :: TEX_3:70

for X being non empty non almost_discrete TopSpace

for X1 being non empty open proper dense SubSpace of X ex X2 being non empty strict closed boundary SubSpace of X st X1,X2 constitute_a_decomposition

for X1 being non empty open proper dense SubSpace of X ex X2 being non empty strict closed boundary SubSpace of X st X1,X2 constitute_a_decomposition

proof end;

theorem :: TEX_3:71

for X being non empty non almost_discrete TopSpace

for X0 being non empty SubSpace of X holds

( X0 is nowhere_dense iff ex X1 being non empty strict closed boundary SubSpace of X st X0 is SubSpace of X1 )

for X0 being non empty SubSpace of X holds

( X0 is nowhere_dense iff ex X1 being non empty strict closed boundary SubSpace of X st X0 is SubSpace of X1 )

proof end;

theorem :: TEX_3:72

for X being non empty non almost_discrete TopSpace

for X0 being non empty nowhere_dense SubSpace of X holds

( ( X0 is boundary & X0 is closed ) or ex X1 being non empty strict proper everywhere_dense SubSpace of X ex X2 being non empty strict closed boundary SubSpace of X st

( X1 meet X2 = TopStruct(# the carrier of X0, the topology of X0 #) & X1 union X2 = TopStruct(# the carrier of X, the topology of X #) ) )

for X0 being non empty nowhere_dense SubSpace of X holds

( ( X0 is boundary & X0 is closed ) or ex X1 being non empty strict proper everywhere_dense SubSpace of X ex X2 being non empty strict closed boundary SubSpace of X st

( X1 meet X2 = TopStruct(# the carrier of X0, the topology of X0 #) & X1 union X2 = TopStruct(# the carrier of X, the topology of X #) ) )

proof end;

theorem :: TEX_3:73

for X being non empty non almost_discrete TopSpace

for X0 being non empty everywhere_dense SubSpace of X holds

( ( X0 is dense & X0 is open ) or ex X1 being non empty strict open proper dense SubSpace of X ex X2 being non empty strict nowhere_dense SubSpace of X st

( X1 misses X2 & X1 union X2 = TopStruct(# the carrier of X0, the topology of X0 #) ) )

for X0 being non empty everywhere_dense SubSpace of X holds

( ( X0 is dense & X0 is open ) or ex X1 being non empty strict open proper dense SubSpace of X ex X2 being non empty strict nowhere_dense SubSpace of X st

( X1 misses X2 & X1 union X2 = TopStruct(# the carrier of X0, the topology of X0 #) ) )

proof end;

theorem :: TEX_3:74

for X being non empty non almost_discrete TopSpace

for X0 being non empty nowhere_dense SubSpace of X ex X1 being non empty strict open proper dense SubSpace of X ex X2 being non empty strict closed boundary SubSpace of X st

( X1,X2 constitute_a_decomposition & X0 is SubSpace of X2 )

for X0 being non empty nowhere_dense SubSpace of X ex X1 being non empty strict open proper dense SubSpace of X ex X2 being non empty strict closed boundary SubSpace of X st

( X1,X2 constitute_a_decomposition & X0 is SubSpace of X2 )

proof end;

theorem :: TEX_3:75

for X being non empty non almost_discrete TopSpace

for X0 being proper everywhere_dense SubSpace of X ex X1 being strict open proper dense SubSpace of X ex X2 being strict closed boundary SubSpace of X st

( X1,X2 constitute_a_decomposition & X1 is SubSpace of X0 )

for X0 being proper everywhere_dense SubSpace of X ex X1 being strict open proper dense SubSpace of X ex X2 being strict closed boundary SubSpace of X st

( X1,X2 constitute_a_decomposition & X1 is SubSpace of X0 )

proof end;