The abstract of the Mizar article:

On Nowhere and Everywhere Dense Subspaces of Topological Spaces

by

Zbigniew Karno

Received November 9, 1993

MML identifier: TEX_3

[ Mizar article, MML identifier index ]

environ

 vocabulary PRE_TOPC, TSEP_2, COLLSP, TOPS_3, BOOLE, TOPS_1, REALSET1,
      SUBSET_1, TARSKI, SETFAM_1, NATTRA_1, TDLAT_3;
 notation TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1,
      TSEP_1, TSEP_2, TDLAT_3, TOPS_3, TEX_1, TEX_2;
 constructors REALSET1, TOPS_1, BORSUK_1, TSEP_1, TSEP_2, TDLAT_3, TOPS_3,
      TEX_2, MEMBERED;
 clusters PRE_TOPC, BORSUK_1, TDLAT_3, TEX_1, TEX_2, STRUCT_0, MEMBERED,
      ZFMISC_1;
 requirements BOOLE, SUBSET;


begin
:: 1. Some Properties of Subsets of a Topological Space.
reserve X for non empty TopSpace, A,B for Subset of X;

theorem :: TEX_3:1
 A,B constitute_a_decomposition implies (A is non empty iff B is proper);

theorem :: TEX_3:2
 A,B constitute_a_decomposition implies (A is dense iff B is boundary);

theorem :: TEX_3:3
   A,B constitute_a_decomposition implies (A is boundary iff B is dense)
;

theorem :: TEX_3:4
 A,B constitute_a_decomposition implies
  (A is everywhere_dense iff B is nowhere_dense);

theorem :: TEX_3:5
   A,B constitute_a_decomposition implies
  (A is nowhere_dense iff B is everywhere_dense);

reserve Y1,Y2 for non empty SubSpace of X;

theorem :: TEX_3:6
 Y1,Y2 constitute_a_decomposition implies Y1 is proper & Y2 is proper;

theorem :: TEX_3:7
   for X being non trivial (non empty TopSpace),
     D being non empty proper Subset of X
  ex Y0 being proper strict non empty SubSpace of X st D = the carrier of Y0;

theorem :: TEX_3:8
 for X being non trivial (non empty TopSpace),
     Y1 being proper non empty SubSpace of X
  ex Y2 being proper strict non empty SubSpace of X st
    Y1,Y2 constitute_a_decomposition;


begin
:: 2. Dense and Everywhere Dense Subspaces.

definition let X be non empty TopSpace;
  let IT be SubSpace of X;
 attr IT is dense means
:: TEX_3:def 1
 for A being Subset of X st
  A = the carrier of IT holds A is dense;
end;

theorem :: TEX_3:9
 for X0 being SubSpace of X, A being Subset of X
   st A = the carrier of X0 holds
  X0 is dense iff A is dense;

definition let X be non empty TopSpace;
 cluster dense closed -> non proper SubSpace of X;
 cluster dense proper -> non closed SubSpace of X;
 cluster proper closed -> non dense SubSpace of X;
end;

definition let X be non empty TopSpace;
 cluster dense strict non empty SubSpace of X;
end;

::Properties of Dense Subspaces.
theorem :: TEX_3:10
 for A0 being non empty Subset of X st A0 is dense
  ex X0 being dense strict non empty SubSpace of X st A0 = the carrier of X0;

theorem :: TEX_3:11
   for X0 being dense non empty SubSpace of X,
     A being Subset of X,
     B being Subset of X0
  st A = B holds B is dense iff A is dense;

theorem :: TEX_3:12
   for X1 being dense SubSpace of X, X2 being SubSpace of X holds
  X1 is SubSpace of X2 implies X2 is dense;

theorem :: TEX_3:13
   for X1 being dense non empty SubSpace of X,
     X2 being non empty SubSpace of X holds
  X1 is SubSpace of X2 implies X1 is dense SubSpace of X2;

theorem :: TEX_3:14
   for X1 being dense non empty SubSpace of X,
     X2 being dense non empty SubSpace of X1
 holds X2 is dense non empty SubSpace of X;

theorem :: TEX_3:15
   for Y1, Y2 being non empty TopSpace st Y2 = the TopStruct of Y1 holds
  Y1 is dense SubSpace of X iff Y2 is dense SubSpace of X;

definition let X be non empty TopSpace;
  let IT be SubSpace of X;
 attr IT is everywhere_dense means
:: TEX_3:def 2
 for A being Subset of X st
   A = the carrier of IT holds A is everywhere_dense;
end;

theorem :: TEX_3:16
 for X0 being SubSpace of X, A being Subset of X
   st A = the carrier of X0 holds
  X0 is everywhere_dense iff A is everywhere_dense;

definition let X be non empty TopSpace;
 cluster everywhere_dense -> dense SubSpace of X;
 cluster non dense -> non everywhere_dense SubSpace of X;
 cluster non proper -> everywhere_dense SubSpace of X;
 cluster non everywhere_dense -> proper SubSpace of X;
end;

definition let X be non empty TopSpace;
 cluster everywhere_dense strict non empty SubSpace of X;
end;

::Properties of Everywhere Dense Subspaces.
theorem :: TEX_3:17
 for A0 being non empty Subset of X st A0 is everywhere_dense
  ex X0 being everywhere_dense strict non empty SubSpace of X
    st A0 = the carrier of X0;

theorem :: TEX_3:18
   for X0 being everywhere_dense non empty SubSpace of X,
   A being Subset of X, B being Subset of X0
   st A = B holds
  B is everywhere_dense iff A is everywhere_dense;

theorem :: TEX_3:19
   for X1 being everywhere_dense SubSpace of X, X2 being SubSpace of X holds
  X1 is SubSpace of X2 implies X2 is everywhere_dense;

theorem :: TEX_3:20
   for X1 being everywhere_dense non empty SubSpace of X,
     X2 being non empty SubSpace of X holds
  X1 is SubSpace of X2 implies X1 is everywhere_dense SubSpace of X2;

theorem :: TEX_3:21
   for X1 being everywhere_dense non empty SubSpace of X,
      X2 being everywhere_dense non empty SubSpace of X1 holds
  X2 is everywhere_dense SubSpace of X;

theorem :: TEX_3:22
   for Y1, Y2 being non empty TopSpace st Y2 = the TopStruct of Y1 holds
 Y1 is everywhere_dense SubSpace of X iff Y2 is everywhere_dense SubSpace of X;

definition let X be non empty TopSpace;
 cluster dense open -> everywhere_dense SubSpace of X;
 cluster dense non everywhere_dense -> non open SubSpace of X;
 cluster open non everywhere_dense -> non dense SubSpace of X;
end;

definition let X be non empty TopSpace;
 cluster dense open strict non empty SubSpace of X;
end;

::Properties of Dense Open Subspaces.
theorem :: TEX_3:23
 for A0 being non empty Subset of X st A0 is dense open
  ex X0 being dense open strict non empty SubSpace of X
   st A0 = the carrier of X0;

theorem :: TEX_3:24
   for X0 being SubSpace of X holds X0 is everywhere_dense iff
  ex X1 being dense open strict SubSpace of X st X1 is SubSpace of X0;

reserve X1, X2 for non empty SubSpace of X;

theorem :: TEX_3:25
    X1 is dense or X2 is dense implies
   X1 union X2 is dense SubSpace of X;

theorem :: TEX_3:26
    X1 is everywhere_dense or X2 is everywhere_dense implies
   X1 union X2 is everywhere_dense SubSpace of X;

theorem :: TEX_3:27
   X1 is everywhere_dense & X2 is everywhere_dense implies
  X1 meet X2 is everywhere_dense SubSpace of X;

theorem :: TEX_3:28
    X1 is everywhere_dense & X2 is dense or
       X1 is dense & X2 is everywhere_dense implies
  X1 meet X2 is dense SubSpace of X;

begin
:: 3. Boundary and Nowhere Dense Subspaces.

definition let X be non empty TopSpace;
  let IT be SubSpace of X;
 attr IT is boundary means
:: TEX_3:def 3
 for A being Subset of X st
  A = the carrier of IT holds A is boundary;
end;

theorem :: TEX_3:29
 for X0 being SubSpace of X, A being Subset of X
 st A = the carrier of X0 holds
   X0 is boundary iff A is boundary;

definition let X be non empty TopSpace;
 cluster open -> non boundary (non empty SubSpace of X);
 cluster boundary -> non open (non empty SubSpace of X);
 cluster everywhere_dense -> non boundary SubSpace of X;
 cluster boundary -> non everywhere_dense SubSpace of X;
end;

::Properties of Boundary Subspaces.
theorem :: TEX_3:30
   for A0 being non empty Subset of X st A0 is boundary
  ex X0 being strict SubSpace of X st X0 is boundary & A0 = the carrier of X0;

theorem :: TEX_3:31
 for X1,X2 being SubSpace of X st X1,X2 constitute_a_decomposition holds
  X1 is dense iff X2 is boundary;

theorem :: TEX_3:32
  for X1,X2 being non empty SubSpace of X st X1,X2 constitute_a_decomposition
 holds X1 is boundary iff X2 is dense;

theorem :: TEX_3:33
 for X0 being SubSpace of X st X0 is boundary
  for A being Subset of X st A c= the carrier of X0 holds A is boundary;

theorem :: TEX_3:34
 for X1,X2 being SubSpace of X st X1 is boundary holds
  X2 is SubSpace of X1 implies X2 is boundary;

definition let X be non empty TopSpace;
  let IT be SubSpace of X;
 attr IT is nowhere_dense means
:: TEX_3:def 4
 for A being Subset of X st
  A = the carrier of IT holds A is nowhere_dense;
end;

theorem :: TEX_3:35
 for X0 being SubSpace of X, A being Subset of X
 st A = the carrier of X0 holds
   X0 is nowhere_dense iff A is nowhere_dense;

definition let X be non empty TopSpace;
 cluster nowhere_dense -> boundary SubSpace of X;
 cluster non boundary -> non nowhere_dense SubSpace of X;
 cluster nowhere_dense -> non dense SubSpace of X;
 cluster dense -> non nowhere_dense SubSpace of X;
end;

reserve X for non empty TopSpace;

::Properties of Nowhere Dense Subspaces.
theorem :: TEX_3:36
   for A0 being non empty Subset of X st A0 is nowhere_dense
  ex X0 being strict SubSpace of X st
      X0 is nowhere_dense & A0 = the carrier of X0;

theorem :: TEX_3:37
 for X1,X2 being SubSpace of X st X1,X2 constitute_a_decomposition holds
  X1 is everywhere_dense iff X2 is nowhere_dense;

theorem :: TEX_3:38
  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;

theorem :: TEX_3:39
 for X0 being SubSpace of X st X0 is nowhere_dense
  for A being Subset of X st A c= the carrier of X0
  holds A is nowhere_dense;

theorem :: TEX_3:40
 for X1,X2 being SubSpace of X st X1 is nowhere_dense holds
  X2 is SubSpace of X1 implies X2 is nowhere_dense;

definition let X be non empty TopSpace;
 cluster boundary closed -> nowhere_dense SubSpace of X;
 cluster boundary non nowhere_dense -> non closed SubSpace of X;
 cluster closed non nowhere_dense -> non boundary SubSpace of X;
end;

::Properties of Boundary Closed Subspaces.
theorem :: TEX_3:41
 for A0 being non empty Subset of X st A0 is boundary closed
  ex X0 being closed strict non empty SubSpace of X st
      X0 is boundary & A0 = the carrier of X0;

theorem :: TEX_3:42
   for X0 being non empty SubSpace of X holds X0 is nowhere_dense iff
  ex X1 being closed strict non empty SubSpace of X st
      X1 is boundary & X0 is SubSpace of X1;

reserve X1, X2 for non empty SubSpace of X;

theorem :: TEX_3:43
   (X1 is boundary or X2 is boundary) & X1 meets X2 implies
   X1 meet X2 is boundary;

theorem :: TEX_3:44
   X1 is nowhere_dense & X2 is nowhere_dense implies
   X1 union X2 is nowhere_dense;

theorem :: TEX_3:45
   X1 is nowhere_dense & X2 is boundary or X1 is boundary & X2 is nowhere_dense
   implies X1 union X2 is boundary;

theorem :: TEX_3:46
   (X1 is nowhere_dense or X2 is nowhere_dense) & X1 meets X2 implies
    X1 meet X2 is nowhere_dense;


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

theorem :: TEX_3:47
   for X being non empty TopSpace holds
   (for X0 being SubSpace of X holds X0 is non boundary) implies
  X is discrete;

theorem :: TEX_3:48
   for X being non trivial (non empty TopSpace) holds
   (for X0 being proper SubSpace of X holds X0 is non dense) implies
  X is discrete;

definition let X be discrete non empty TopSpace;
 cluster -> non boundary (non empty SubSpace of X);
 cluster proper -> non dense SubSpace of X;
 cluster dense -> non proper SubSpace of X;
end;

definition let X be discrete non empty TopSpace;
 cluster non boundary strict non empty SubSpace of X;
end;

definition let X be discrete non trivial (non empty TopSpace);
 cluster non dense strict SubSpace of X;
end;

theorem :: TEX_3:49
   for X being non empty TopSpace holds
   (ex X0 being non empty SubSpace of X st X0 is boundary) implies
  X is non discrete;

theorem :: TEX_3:50
   for X being non empty TopSpace holds
   (ex X0 being non empty SubSpace of X st X0 is dense proper) implies
  X is non discrete;

definition let X be non discrete non empty TopSpace;
 cluster boundary strict non empty SubSpace of X;
 cluster dense proper strict non empty SubSpace of X;
end;

reserve X for non discrete non empty TopSpace;

theorem :: TEX_3:51
   for A0 being non empty Subset of X st A0 is boundary
  ex X0 being boundary strict SubSpace of X st A0 = the carrier of X0;

theorem :: TEX_3:52
   for A0 being non empty proper Subset of X st A0 is dense
  ex X0 being dense proper strict SubSpace of X st A0 = the carrier of X0;

theorem :: TEX_3:53
   for X1 being boundary non empty SubSpace of X
  ex X2 being dense proper strict non empty SubSpace of X st
    X1,X2 constitute_a_decomposition;

theorem :: TEX_3:54
   for X1 being dense proper non empty SubSpace of X
  ex X2 being boundary strict non empty SubSpace of X st
    X1,X2 constitute_a_decomposition;

theorem :: TEX_3:55
   for Y1, Y2 being non empty TopSpace st Y2 = the TopStruct of Y1 holds
  Y1 is boundary SubSpace of X iff Y2 is boundary SubSpace of X;


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

theorem :: TEX_3:56
   for X being non empty TopSpace holds
   (for X0 being SubSpace of X holds X0 is non nowhere_dense) implies
  X is almost_discrete;

theorem :: TEX_3:57
   for X being non trivial (non empty TopSpace) holds
   (for X0 being proper SubSpace of X holds X0 is non everywhere_dense) implies
  X is almost_discrete;

definition let X be almost_discrete non empty TopSpace;
 cluster -> non nowhere_dense (non empty SubSpace of X);
 cluster proper -> non everywhere_dense SubSpace of X;
 cluster everywhere_dense -> non proper SubSpace of X;
 cluster boundary -> non closed (non empty SubSpace of X);
 cluster closed -> non boundary (non empty SubSpace of X);
 cluster dense proper -> non open SubSpace of X;
 cluster dense open -> non proper SubSpace of X;
 cluster open proper -> non dense SubSpace of X;
end;

definition let X be almost_discrete non empty TopSpace;
 cluster non nowhere_dense strict non empty SubSpace of X;
end;

definition let X be almost_discrete non trivial (non empty TopSpace);
 cluster non everywhere_dense strict SubSpace of X;
end;

theorem :: TEX_3:58
   for X being non empty TopSpace holds
   (ex X0 being non empty SubSpace of X st X0 is nowhere_dense) implies
  X is non almost_discrete;

theorem :: TEX_3:59
   for X being non empty TopSpace holds
   (ex X0 being non empty SubSpace of X st X0 is boundary closed) implies
  X is non almost_discrete;

theorem :: TEX_3:60
   for X being non empty TopSpace holds
   (ex X0 being non empty SubSpace of X st X0 is everywhere_dense proper)
   implies
  X is non almost_discrete;

theorem :: TEX_3:61
   for X being non empty TopSpace holds
   (ex X0 being non empty SubSpace of X st X0 is dense open proper) implies
  X is non almost_discrete;

definition let X be non almost_discrete non empty TopSpace;
 cluster nowhere_dense strict non empty SubSpace of X;
 cluster everywhere_dense proper strict non empty SubSpace of X;
end;

reserve X for non almost_discrete non empty TopSpace;

theorem :: TEX_3:62
 for A0 being non empty Subset of X st A0 is nowhere_dense
  ex X0 being nowhere_dense strict non empty SubSpace of X
    st A0 = the carrier of X0;

theorem :: TEX_3:63
   for A0 being non empty proper Subset of X
 st A0 is everywhere_dense
  ex X0 being everywhere_dense proper strict SubSpace of X st
     A0 = the carrier of X0;

theorem :: TEX_3:64
   for X1 being nowhere_dense non empty SubSpace of X
  ex X2 being everywhere_dense proper strict non empty SubSpace of X st
    X1,X2 constitute_a_decomposition;

theorem :: TEX_3:65
   for X1 being everywhere_dense proper non empty SubSpace of X
  ex X2 being nowhere_dense strict non empty SubSpace of X st
    X1,X2 constitute_a_decomposition;

theorem :: TEX_3:66
   for Y1, Y2 being non empty TopSpace st Y2 = the TopStruct of Y1 holds
  Y1 is nowhere_dense SubSpace of X iff Y2 is nowhere_dense SubSpace of X;

definition let X be non almost_discrete non empty TopSpace;
 cluster boundary closed strict non empty SubSpace of X;
 cluster dense open proper strict non empty SubSpace of X;
end;

theorem :: TEX_3:67
 for A0 being non empty Subset of X st A0 is boundary closed
  ex X0 being boundary closed strict non empty SubSpace of X
    st A0 = the carrier of X0;

theorem :: TEX_3:68
   for A0 being non empty proper Subset of X st A0 is dense open
  ex X0 being dense open proper strict SubSpace of X st
     A0 = the carrier of X0;

theorem :: TEX_3:69
   for X1 being boundary closed non empty SubSpace of X
  ex X2 being dense open proper strict non empty SubSpace of X st
    X1,X2 constitute_a_decomposition;

theorem :: TEX_3:70
   for X1 being dense open proper non empty SubSpace of X
  ex X2 being boundary closed strict non empty SubSpace of X st
    X1,X2 constitute_a_decomposition;

theorem :: TEX_3:71
   for X0 being non empty SubSpace of X holds X0 is nowhere_dense iff
  ex X1 being boundary closed strict non empty SubSpace of X
    st X0 is SubSpace of X1;

theorem :: TEX_3:72
   for X0 being nowhere_dense non empty SubSpace of X holds
  X0 is boundary closed or
   ex X1 being everywhere_dense proper strict non empty SubSpace of X,
       X2 being boundary closed strict non empty SubSpace of X st
     X1 meet X2 = the TopStruct of X0 & X1 union X2 = the TopStruct of X;

theorem :: TEX_3:73
   for X0 being everywhere_dense non empty SubSpace of X holds
  X0 is dense open or
   ex X1 being dense open proper strict non empty SubSpace of X,
       X2 being nowhere_dense strict non empty SubSpace of X st
     X1 misses X2 & X1 union X2 = the TopStruct of X0;

theorem :: TEX_3:74
   for X0 being nowhere_dense non empty SubSpace of X
  ex X1 being dense open proper strict non empty SubSpace of X,
      X2 being boundary closed strict non empty SubSpace of X st
    X1,X2 constitute_a_decomposition & X0 is SubSpace of X2;

theorem :: TEX_3:75
   for X0 being everywhere_dense proper SubSpace of X
  ex X1 being dense open proper strict SubSpace of X,
      X2 being boundary closed strict SubSpace of X st
    X1,X2 constitute_a_decomposition & X1 is SubSpace of X0;