The abstract of the Mizar article:

On Discrete and Almost Discrete Topological Spaces

by

Zbigniew Karno

Received April 6, 1993

MML identifier: TEX_1

[ Mizar article, MML identifier index ]

environ

 vocabulary PRE_TOPC, TMAP_1, SUBSET_1, BOOLE, TOPS_1, TOPS_3, REALSET1,
      SETFAM_1, TDLAT_3, NATTRA_1, TARSKI, TEX_1, PCOMPS_1;
 notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, SETFAM_1, STRUCT_0, REALSET1,
      PRE_TOPC, TOPS_1, TMAP_1, TDLAT_3, TOPS_3, PCOMPS_1;
 constructors REALSET1, TOPS_1, TMAP_1, TDLAT_3, TOPS_3, DOMAIN_1, PCOMPS_1,
      MEMBERED;
 clusters TDLAT_3, STRUCT_0, COMPLSP1, TMAP_1, SUBSET_1, TOPS_1, PCOMPS_1,
      XBOOLE_0, ZFMISC_1;
 requirements BOOLE, SUBSET;


begin
:: 1. Properties of Subsets of a Topological Space with Modified Topology.
reserve X for non empty TopSpace, D for Subset of X;

theorem :: TEX_1:1
 for B being Subset of X,
     C being Subset of X modified_with_respect_to D st
  B = C holds B is open implies C is open;

theorem :: TEX_1:2
   for B being Subset of X,
     C being Subset of X modified_with_respect_to D st
  B = C holds B is closed implies C is closed;

theorem :: TEX_1:3
 for C being Subset of X modified_with_respect_to  D` st C = D holds
  C is closed;

theorem :: TEX_1:4
 for C being Subset of X modified_with_respect_to D
   st C = D holds
  D is dense implies C is dense & C is open;

theorem :: TEX_1:5
 for C being Subset of X modified_with_respect_to D
   st D c= C holds
  D is dense implies C is everywhere_dense;

theorem :: TEX_1:6
 for C being Subset of X modified_with_respect_to  D`
   st C = D holds
  D is boundary implies C is boundary & C is closed;

theorem :: TEX_1:7
 for C being Subset of X modified_with_respect_to  D`
   st C c= D holds
  D is boundary implies C is nowhere_dense;

begin
:: 2. Trivial Topological Spaces.

definition let Y be non empty 1-sorted;
 redefine attr Y is trivial means
:: TEX_1:def 1
 ex d being Element of Y st the carrier of Y = {d};
end;

definition let A be non empty set;
 cluster 1-sorted(#A#) -> non empty;
end;

definition
 cluster trivial strict non empty 1-sorted;
 cluster non trivial strict non empty 1-sorted;
end;

definition
 cluster trivial strict non empty TopStruct;
 cluster non trivial strict non empty TopStruct;
end;

theorem :: TEX_1:8
   for Y being trivial non empty TopStruct st the topology of Y is non empty
  holds Y is almost_discrete implies Y is TopSpace-like;

definition
 cluster trivial strict non empty TopSpace;
end;

definition
 cluster trivial -> anti-discrete discrete (non empty TopSpace);
 cluster discrete anti-discrete -> trivial (non empty TopSpace);
end;

definition
 cluster non trivial strict non empty TopSpace;
end;

definition
 cluster non discrete -> non trivial (non empty TopSpace);
 cluster non anti-discrete -> non trivial (non empty TopSpace);
end;

begin
:: 3. Examples of Discrete and Anti-discrete Topological Spaces.

definition let D be set;
 func cobool D -> Subset-Family of D equals
:: TEX_1:def 2
 {{},D};
end;

definition let D be set;
 cluster cobool D -> non empty;
end;

definition let D be set;
 func ADTS(D) -> TopStruct equals
:: TEX_1:def 3
 TopStruct(#D,cobool D#);
end;

definition let D be set;
 cluster ADTS(D) -> strict anti-discrete TopSpace-like;
end;

definition let D be non empty set;
 cluster ADTS(D) -> non empty;
end;

theorem :: TEX_1:9
 for X being anti-discrete non empty TopSpace holds
   the TopStruct of X = ADTS(the carrier of X);

theorem :: TEX_1:10
   for X being non empty TopSpace st
  the TopStruct of X = the TopStruct of ADTS(the carrier of X) holds
     X is anti-discrete;

theorem :: TEX_1:11
 for X being anti-discrete non empty TopSpace
  for A being Subset of X holds (A is empty implies Cl A = {}) &
                     (A is non empty implies Cl A = the carrier of X);

theorem :: TEX_1:12
 for X being anti-discrete non empty TopSpace
  for A being Subset of X holds (A <> the carrier of X
    implies Int A = {}) &
                     (A = the carrier of X implies Int A = the carrier of X);

theorem :: TEX_1:13
 for X being non empty TopSpace holds
    (for A being Subset of X holds
        (A is non empty implies Cl A = the carrier of X))
  implies X is anti-discrete;

theorem :: TEX_1:14
 for X being non empty TopSpace holds
    (for A being Subset of X
      holds (A <> the carrier of X implies Int A = {}))
  implies X is anti-discrete;

theorem :: TEX_1:15
   for X being anti-discrete non empty TopSpace
  for A being Subset of X holds (A <> {} implies A is dense) &
                  (A <> the carrier of X implies A is boundary);

theorem :: TEX_1:16
   for X being non empty TopSpace holds
   (for A being Subset of X holds (A <> {} implies A is dense))
  implies X is anti-discrete;

theorem :: TEX_1:17
   for X being non empty TopSpace holds
  (for A being Subset of X
    holds (A <> the carrier of X implies A is boundary))
  implies X is anti-discrete;

definition let D be set;
 cluster 1TopSp D -> discrete;
end;

theorem :: TEX_1:18
 for X being discrete non empty TopSpace holds
   the TopStruct of X = 1TopSp (the carrier of X);

theorem :: TEX_1:19
   for X being non empty TopSpace st
  the TopStruct of X = the TopStruct of 1TopSp(the carrier of X) holds
     X is discrete;

theorem :: TEX_1:20
   for X being discrete non empty TopSpace
  for A being Subset of X holds Cl A = A & Int A = A;

theorem :: TEX_1:21
   for X being non empty TopSpace holds
  (for A being Subset of X holds Cl A = A) implies X is discrete;

theorem :: TEX_1:22
   for X being non empty TopSpace holds
  (for A being Subset of X
     holds Int A = A) implies X is discrete;

theorem :: TEX_1:23
 for D being non empty set holds
  ADTS(D) = 1TopSp(D) iff ex d0 being Element of D st D = {d0};

definition
 cluster discrete non anti-discrete strict non empty TopSpace;
 cluster anti-discrete non discrete strict non empty TopSpace;
end;

begin
:: 4. An Example of a Topological Space.

definition let D be set, F be Subset-Family of D, S be set;
 redefine func F \ S -> Subset-Family of D;
end;

definition let D be set, d0 be Element of D;
 canceled;

 func STS(D,d0) -> TopStruct equals
:: TEX_1:def 5
    TopStruct (#D,(bool D) \ {A where A is Subset of D : d0 in A & A <> D}#);
end;

definition let D be set, d0 be Element of D;
 cluster STS(D,d0) -> strict TopSpace-like;
end;

definition let D be non empty set, d0 be Element of D;
 cluster STS(D,d0) -> non empty;
end;

reserve D for non empty set, d0 for Element of D;

theorem :: TEX_1:24
 for A being Subset of STS(D,d0) holds
   ({d0} c= A implies A is closed) &
     (A is non empty & A is closed implies {d0} c= A);

theorem :: TEX_1:25
 D \ {d0} is non empty implies
   for A being Subset of STS(D,d0) holds
      (A = {d0} implies A is closed & A is boundary) &
     (A is non empty & A is closed & A is boundary implies A = {d0});

theorem :: TEX_1:26
 for A being Subset of STS(D,d0) holds
   (A c= D \ {d0} implies A is open) &
      (A <> D & A is open implies A c= D \ {d0});

theorem :: TEX_1:27
   D \ {d0} is non empty implies
   for A being Subset of STS(D,d0) holds
      (A = D \ {d0} implies A is open & A is dense) &
     (A <> D & A is open & A is dense implies A = D \ {d0});

definition
 cluster non anti-discrete non discrete strict non empty TopSpace;
end;

theorem :: TEX_1:28
 for Y being non empty TopSpace holds
  the TopStruct of Y = the TopStruct of STS(D,d0) iff
    the carrier of Y = D &
   for A being Subset of Y
     holds ({d0} c= A implies A is closed) &
                     (A is non empty & A is closed implies {d0} c= A);

theorem :: TEX_1:29
 for Y being non empty TopSpace holds
  the TopStruct of Y = the TopStruct of STS(D,d0) iff
    the carrier of Y = D &
   for A being Subset of Y
      holds (A c= D \ {d0} implies A is open) &
                            (A <> D & A is open implies A c= D \ {d0});

theorem :: TEX_1:30
   for Y being non empty TopSpace holds
   the TopStruct of Y = the TopStruct of STS(D,d0) iff
      the carrier of Y = D &
     for A being non empty Subset of Y holds Cl A = A \/ {d0};

theorem :: TEX_1:31
   for Y being non empty TopSpace holds
   the TopStruct of Y = the TopStruct of STS(D,d0) iff
      the carrier of Y = D &
     for A being Subset of Y st A <> D holds Int A = A \ {d0};

theorem :: TEX_1:32
   STS(D,d0) = ADTS(D) iff D = {d0};

theorem :: TEX_1:33
   STS(D,d0) = 1TopSp(D) iff D = {d0};

theorem :: TEX_1:34
   for D being non empty set, d0 being Element of D
   for A being Subset of STS(D,d0) st A = {d0} holds
     1TopSp(D) = STS(D,d0) modified_with_respect_to A;


begin
:: 5. Discrete and Almost Discrete Spaces.

definition let X be non empty TopSpace;
 redefine attr X is discrete means
:: TEX_1:def 6
 for A being non empty Subset of X holds A is not boundary;
end;

theorem :: TEX_1:35
   X is discrete iff
  for A being Subset of X
    holds A <> the carrier of X implies A is not dense;

definition
 cluster non almost_discrete ->
    non discrete non anti-discrete (non empty TopSpace);
end;

definition let X be non empty TopSpace;
 redefine attr X is almost_discrete means
:: TEX_1:def 7
 for A being non empty Subset of X holds A is not nowhere_dense;
end;

theorem :: TEX_1:36
 X is almost_discrete iff
   for A being Subset of X holds
    A <> the carrier of X implies A is not everywhere_dense;

theorem :: TEX_1:37
 X is non almost_discrete iff
  ex A being non empty Subset of X st A is boundary & A is closed;

theorem :: TEX_1:38
   X is non almost_discrete iff
  ex A being Subset of X st A <> the carrier of X & A is dense & A is open;

definition
 cluster
  almost_discrete non discrete non anti-discrete strict non empty TopSpace;
end;

theorem :: TEX_1:39
 for C being non empty set, c0 being Element of C holds
  C \ {c0} is non empty iff STS(C,c0) is non almost_discrete;

definition
 cluster non almost_discrete strict non empty TopSpace;
end;

theorem :: TEX_1:40
   for A being non empty Subset of X st A is boundary holds
   X modified_with_respect_to  A` is non almost_discrete;

theorem :: TEX_1:41
   for A being Subset of X st A <> the carrier of X & A is dense holds
  X modified_with_respect_to A is non almost_discrete;