:: On Nowhere and Everywhere Dense Subspaces of Topological Spaces
:: by Zbigniew Karno
::
:: Received November 9, 1993
:: Copyright (c) 1993-2021 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 )

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 )

proof end;

theorem :: TEX_3:3

for X being non empty TopSpace
for A, B being Subset of X st A,B constitute_a_decomposition holds
( A is boundary iff B is dense ) by Th2;

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 )

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;

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 )

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

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

proof end;

:: 2. Dense and Everywhere Dense Subspaces.

definition

let X be non empty TopSpace;
let IT be SubSpace of X;

attr IT is dense means :Def1: :: TEX_3:def 1
for A being Subset of X st A = the carrier of IT holds
A is dense ;

end;

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

theorem Th9: :: TEX_3:9

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 dense iff A is dense ) ;

registration

let X be non empty TopSpace;

cluster closed dense -> non proper for SubSpace of X;

coherence
for b₁ being SubSpace of X st b₁ is dense & b₁ is closed holds
not b₁ is proper

proof end;

cluster proper dense -> non closed for SubSpace of X;

coherence
for b₁ being SubSpace of X st b₁ is dense & b₁ is proper holds
not b₁ is closed ;

cluster closed proper -> non dense for SubSpace of X;

coherence
for b₁ being SubSpace of X st b₁ is proper & b₁ is closed holds
not b₁ is dense ;

end;

registration

let X be non empty TopSpace;

cluster non empty strict TopSpace-like dense for SubSpace of X;

existence
ex b₁ being SubSpace of X st
( b₁ is dense & b₁ is strict & not b₁ is empty )

proof end;

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

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 )

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

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

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

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 )

proof end;

definition

let X be non empty TopSpace;
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 ;

end;

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

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

registration

let X be non empty TopSpace;

cluster everywhere_dense -> dense for SubSpace of X;

coherence
for b₁ being SubSpace of X st b₁ is everywhere_dense holds
b₁ is dense by TOPS_3:33;

cluster non dense -> non everywhere_dense for SubSpace of X;

coherence
for b₁ being SubSpace of X st not b₁ is dense holds
not b₁ is everywhere_dense ;

cluster non proper -> everywhere_dense for SubSpace of X;

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

proof end;

cluster non everywhere_dense -> proper for SubSpace of X;

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

end;

registration

let X be non empty TopSpace;

cluster non empty strict TopSpace-like everywhere_dense for SubSpace of X;

existence
ex b₁ being SubSpace of X st
( b₁ is everywhere_dense & b₁ is strict & not b₁ is empty )

proof end;

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

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 )

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

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

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

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 )

proof end;

registration

let X be non empty TopSpace;

cluster open dense -> everywhere_dense for SubSpace of X;

coherence
for b₁ being SubSpace of X st b₁ is dense & b₁ is open holds
b₁ is everywhere_dense

proof end;

cluster dense non everywhere_dense -> non open for SubSpace of X;

coherence
for b₁ being SubSpace of X st b₁ is dense & not b₁ is everywhere_dense holds
not b₁ is open ;

cluster open non everywhere_dense -> non dense for SubSpace of X;

coherence
for b₁ being SubSpace of X st b₁ is open & not b₁ is everywhere_dense holds
not b₁ is dense ;

end;

registration

let X be non empty TopSpace;

cluster non empty strict TopSpace-like open dense for SubSpace of X;

existence
ex b₁ being SubSpace of X st
( b₁ is dense & b₁ is open & b₁ is strict & not b₁ is empty )

proof end;

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

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 )

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

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

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

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

proof end;

:: 3. Boundary and Nowhere Dense Subspaces.

definition

let X be non empty TopSpace;
let IT be SubSpace of X;

attr IT is boundary means :Def3: :: TEX_3:def 3
for A being Subset of X st A = the carrier of IT holds
A is boundary ;

end;

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

theorem Th29: :: TEX_3:29

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 boundary iff A is boundary ) ;

registration

let X be non empty TopSpace;

cluster non empty open -> non empty non boundary for SubSpace of X;

coherence
for b₁ being non empty SubSpace of X st b₁ is open holds
not b₁ is boundary

proof end;

cluster non empty boundary -> non empty non open for SubSpace of X;

coherence
for b₁ being non empty SubSpace of X st b₁ is boundary holds
not b₁ is open ;

cluster everywhere_dense -> non boundary for SubSpace of X;

coherence
for b₁ being SubSpace of X st b₁ is everywhere_dense holds
not b₁ is boundary

proof end;

cluster boundary -> non everywhere_dense for SubSpace of X;

coherence
for b₁ being SubSpace of X st b₁ is boundary holds
not b₁ is everywhere_dense ;

end;

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

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 )

proof end;

theorem :: TEX_3:32

for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1,X2 constitute_a_decomposition holds
( X1 is boundary iff X2 is dense ) by Th31;

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

proof end;

theorem Th34: :: TEX_3:34

for X being non empty TopSpace
for X1, X2 being SubSpace of X st X1 is boundary & X2 is SubSpace of X1 holds
X2 is boundary by TSEP_1:4, Th33;

definition

let X be non empty TopSpace;
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 ;

end;

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

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

registration

let X be non empty TopSpace;

cluster nowhere_dense -> boundary for SubSpace of X;

coherence
for b₁ being SubSpace of X st b₁ is nowhere_dense holds
b₁ is boundary

proof end;

cluster non boundary -> non nowhere_dense for SubSpace of X;

coherence
for b₁ being SubSpace of X st not b₁ is boundary holds
not b₁ is nowhere_dense ;

cluster nowhere_dense -> non dense for SubSpace of X;

coherence
for b₁ being SubSpace of X st b₁ is nowhere_dense holds
not b₁ is dense

proof end;

cluster dense -> non nowhere_dense for SubSpace of X;

coherence
for b₁ being SubSpace of X st b₁ is dense holds
not b₁ is nowhere_dense ;

end;

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

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 )

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;

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

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;

registration

let X be non empty TopSpace;

cluster closed boundary -> nowhere_dense for SubSpace of X;

coherence
for b₁ being SubSpace of X st b₁ is boundary & b₁ is closed holds
b₁ is nowhere_dense

proof end;

cluster boundary non nowhere_dense -> non closed for SubSpace of X;

coherence
for b₁ being SubSpace of X st b₁ is boundary & not b₁ is nowhere_dense holds
not b₁ is closed ;

cluster closed non nowhere_dense -> non boundary for SubSpace of X;

coherence
for b₁ being SubSpace of X st b₁ is closed & not b₁ is nowhere_dense holds
not b₁ is boundary ;

end;

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

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

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

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

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

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

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

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

proof end;

registration

let X be non empty discrete TopSpace;

cluster non empty -> non empty non boundary for SubSpace of X;

coherence
for b₁ being non empty SubSpace of X holds not b₁ is boundary ;

cluster proper -> non dense for SubSpace of X;

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

cluster dense -> non proper for SubSpace of X;

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

end;

registration

let X be non empty discrete TopSpace;

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

existence
ex b₁ being SubSpace of X st
( not b₁ is boundary & b₁ is strict & not b₁ is empty )

proof end;

end;

registration

let X be non trivial discrete TopSpace;

cluster strict TopSpace-like closed open discrete almost_discrete non dense for SubSpace of X;

existence
ex b₁ being SubSpace of X st
( not b₁ is dense & b₁ is strict )

proof end;

end;

theorem :: TEX_3:49

for X being non empty TopSpace st ex X0 being non empty SubSpace of X st X0 is boundary holds
not X is discrete ;

theorem :: TEX_3:50

for X being non empty TopSpace st ex X0 being non empty SubSpace of X st
( X0 is dense & X0 is proper ) holds
not X is discrete ;

registration

let X be non empty non discrete TopSpace;

cluster non empty strict TopSpace-like boundary for SubSpace of X;

existence
ex b₁ being SubSpace of X st
( b₁ is boundary & b₁ is strict & not b₁ is empty )

proof end;

cluster non empty strict TopSpace-like proper dense for SubSpace of X;

existence
ex b₁ being SubSpace of X st
( b₁ is dense & b₁ is proper & b₁ is strict & not b₁ is empty )

proof end;

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

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

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

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

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 )

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

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

proof end;

registration

let X be non empty almost_discrete TopSpace;

cluster non empty -> non empty non nowhere_dense for SubSpace of X;

coherence
for b₁ being non empty SubSpace of X holds not b₁ is nowhere_dense

proof end;

cluster proper -> non everywhere_dense for SubSpace of X;

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

proof end;

cluster everywhere_dense -> non proper for SubSpace of X;

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

cluster non empty boundary -> non empty non closed for SubSpace of X;

coherence
for b₁ being non empty SubSpace of X st b₁ is boundary holds
not b₁ is closed ;

cluster non empty closed -> non empty non boundary for SubSpace of X;

coherence
for b₁ being non empty SubSpace of X st b₁ is closed holds
not b₁ is boundary ;

cluster proper dense -> non open for SubSpace of X;

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

cluster open dense -> non proper for SubSpace of X;

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

cluster open proper -> non dense for SubSpace of X;

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

end;

registration

let X be non empty almost_discrete TopSpace;

cluster non empty strict TopSpace-like non nowhere_dense for SubSpace of X;

existence
ex b₁ being SubSpace of X st
( not b₁ is nowhere_dense & b₁ is strict & not b₁ is empty )

proof end;

end;

registration

let X be non trivial almost_discrete TopSpace;

cluster strict TopSpace-like non everywhere_dense for SubSpace of X;

existence
ex b₁ being SubSpace of X st
( not b₁ is everywhere_dense & b₁ is strict )

proof end;

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 ;

theorem :: TEX_3:59

for X being non empty TopSpace st ex X0 being non empty SubSpace of X st
( X0 is boundary & X0 is closed ) holds
not X is almost_discrete ;

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 ;

theorem :: TEX_3:61

for X being non empty TopSpace st ex X0 being non empty SubSpace of X st
( X0 is dense & X0 is open & X0 is proper ) holds
not X is almost_discrete ;

registration

let X be non empty non almost_discrete TopSpace;

cluster non empty strict TopSpace-like nowhere_dense for SubSpace of X;

existence
ex b₁ being SubSpace of X st
( b₁ is nowhere_dense & b₁ is strict & not b₁ is empty )

proof end;

cluster non empty strict TopSpace-like proper everywhere_dense for SubSpace of X;

existence
ex b₁ being SubSpace of X st
( b₁ is everywhere_dense & b₁ is proper & b₁ is strict & not b₁ is empty )

proof end;

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

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

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

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

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 )

proof end;

registration

let X be non empty non almost_discrete TopSpace;

cluster non empty strict TopSpace-like closed boundary for SubSpace of X;

existence
ex b₁ being SubSpace of X st
( b₁ is boundary & b₁ is closed & b₁ is strict & not b₁ is empty )

proof end;

cluster non empty strict TopSpace-like open proper dense for SubSpace of X;

existence
ex b₁ being SubSpace of X st
( b₁ is dense & b₁ is open & b₁ is proper & b₁ is strict & not b₁ is empty )

proof end;

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

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

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

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

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 )

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

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

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 )

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 )

proof end;