The abstract of the Mizar article:

Maximal Discrete Subspaces of Almost Discrete Topological Spaces

by

Zbigniew Karno

Received November 5, 1993

MML identifier: TEX_2

[ Mizar article, MML identifier index ]

environ

 vocabulary REALSET1, BOOLE, COLLSP, TARSKI, SUBSET_1, PRE_TOPC, SETFAM_1,
      RELAT_1, NATTRA_1, TDLAT_3, TOPS_3, TOPS_1, FUNCT_1, ORDINAL2, TEX_1,
      BORSUK_1, TEX_2, PCOMPS_1;
 notation TARSKI, XBOOLE_0, SUBSET_1, DOMAIN_1, RELAT_1, FUNCT_1, PARTFUN1,
      FUNCT_2, REALSET1, STRUCT_0, PRE_TOPC, TOPS_1, TOPS_2, BORSUK_1, TSEP_1,
      TDLAT_3, TOPS_3, PCOMPS_1, TEX_1;
 constructors DOMAIN_1, REALSET1, TOPS_1, TOPS_2, TMAP_1, BORSUK_1, TOPS_3,
      TEX_1, TDLAT_3, MEMBERED, PARTFUN1;
 clusters PRE_TOPC, TDLAT_3, TEX_1, REALSET1, STRUCT_0, RELSET_1, PCOMPS_1,
      SUBSET_1, BORSUK_1, MEMBERED, ZFMISC_1, FUNCT_2, PARTFUN1;
 requirements BOOLE, SUBSET;


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

definition let X be non empty set;
redefine attr X is trivial means
:: TEX_2:def 1
 ex s being Element of X st X = {s};
end;

definition
 cluster trivial non empty set;
end;

theorem :: TEX_2:1
 for A being non empty set, B being trivial non empty set st
  A c= B holds A = B;

theorem :: TEX_2:2
  for A being trivial non empty set, B being set st
   A /\ B is non empty holds A c= B;

canceled;

theorem :: TEX_2:4
 for S, T being 1-sorted st the carrier of S = the carrier of T
  holds S is trivial implies T is trivial;

definition let S be set;
  let IT be Element of S;
 attr IT is proper means
:: TEX_2:def 2
 IT <> union S;
end;

definition let S be set;
 cluster non proper Subset of S;
end;

theorem :: TEX_2:5
 for S being set, A being Subset of S holds A is proper iff A <> S;

definition let S be non empty set;
 cluster non proper -> non empty Subset of S;
 cluster empty -> proper Subset of S;
end;

definition let S be trivial non empty set;
 cluster proper -> empty Subset of S;
 cluster non empty -> non proper Subset of S;
end;

definition let S be non empty set;
 cluster proper Subset of S;
 cluster non proper Subset of S;
end;

definition let S be non empty set;
 cluster trivial (non empty Subset of S);
end;

definition let y be set;
 cluster {y} -> trivial;
end;

theorem :: TEX_2:6
   for S being non empty set, y being Element of S holds
  {y} is proper implies S is non trivial;

theorem :: TEX_2:7
  for S being non trivial non empty set, y being Element of S holds
  {y} is proper;

definition let S be trivial non empty set;
 cluster non proper -> trivial (non empty Subset of S);
end;

definition let S be non trivial non empty set;
 cluster trivial -> proper (non empty Subset of S);
 cluster non proper -> non trivial (non empty Subset of S);
end;

definition let S be non trivial non empty set;
 cluster trivial proper (non empty Subset of S);
 cluster non trivial non proper (non empty Subset of S);
end;

theorem :: TEX_2:8
 for Y being non empty 1-sorted, y being Element of Y holds
  {y} is proper implies Y is non trivial;

theorem :: TEX_2:9
 for Y being non trivial non empty 1-sorted,
     y being Element of Y holds
  {y} is proper;

definition let Y be trivial non empty 1-sorted;
 cluster -> non proper (non empty Subset of Y);
 cluster non proper -> trivial (non empty Subset of Y);
end;

definition let Y be non trivial non empty 1-sorted;
 cluster trivial -> proper (non empty Subset of Y);
 cluster non proper -> non trivial (non empty Subset of Y);
end;

definition let Y be non trivial non empty 1-sorted;
 cluster trivial proper (non empty Subset of Y);
 cluster non trivial non proper (non empty Subset of Y);
end;

definition let Y be non trivial non empty 1-sorted;
  cluster non empty trivial proper Subset of Y;
end;

begin
:: 2. Proper Subspaces of Topological Spaces.

theorem :: TEX_2:10
    for X being non empty TopStruct, X0 being SubSpace of X holds
               the TopStruct of X0 is strict SubSpace of X;

canceled;

theorem :: TEX_2:12
 for Y0, Y1 being TopStruct st
    the TopStruct of Y0 = the TopStruct of Y1 holds
   Y0 is TopSpace-like implies Y1 is TopSpace-like;

definition let Y be TopStruct;
  let IT be SubSpace of Y;
 attr IT is proper means
:: TEX_2:def 3
 for A being Subset of Y st A = the carrier of IT
  holds A is proper;
end;

reserve Y for TopStruct;

theorem :: TEX_2:13
 for Y0 being SubSpace of Y, A being Subset of Y st
   A = the carrier of Y0 holds A is proper iff Y0 is proper;

theorem :: TEX_2:14
   for Y0, Y1 being SubSpace of Y st
    the TopStruct of Y0 = the TopStruct of Y1 holds
   Y0 is proper implies Y1 is proper;

theorem :: TEX_2:15
 for Y0 being SubSpace of Y holds
  the carrier of Y0 = the carrier of Y implies Y0 is non proper;

definition let Y be trivial non empty TopStruct;
 cluster -> non proper (non empty SubSpace of Y);
 cluster non proper -> trivial (non empty SubSpace of Y);
end;

definition let Y be non trivial non empty TopStruct;
 cluster trivial -> proper (non empty SubSpace of Y);
 cluster non proper -> non trivial (non empty SubSpace of Y);
end;

definition let Y be non empty TopStruct;
 cluster non proper strict non empty SubSpace of Y;
end;

theorem :: TEX_2:16
   for Y being non empty TopStruct,
     Y0 being non proper SubSpace of Y holds
   the TopStruct of Y0 = the TopStruct of Y;

definition let Y be non empty TopStruct;
 cluster discrete -> TopSpace-like SubSpace of Y;
 cluster anti-discrete -> TopSpace-like SubSpace of Y;
 cluster non TopSpace-like -> non discrete SubSpace of Y;
 cluster non TopSpace-like -> non anti-discrete SubSpace of Y;
end;

theorem :: TEX_2:17
 for Y0, Y1 being TopStruct st
    the TopStruct of Y0 = the TopStruct of Y1 holds
   Y0 is discrete implies Y1 is discrete;

theorem :: TEX_2:18
 for Y0, Y1 being TopStruct st
    the TopStruct of Y0 = the TopStruct of Y1 holds
   Y0 is anti-discrete implies Y1 is anti-discrete;

definition let Y be non empty TopStruct;
 cluster discrete -> almost_discrete SubSpace of Y;
 cluster non almost_discrete -> non discrete SubSpace of Y;
 cluster anti-discrete -> almost_discrete SubSpace of Y;
 cluster non almost_discrete -> non anti-discrete SubSpace of Y;
end;

theorem :: TEX_2:19
   for Y0, Y1 being TopStruct st
    the TopStruct of Y0 = the TopStruct of Y1 holds
   Y0 is almost_discrete implies Y1 is almost_discrete;

definition let Y be non empty TopStruct;
 cluster discrete anti-discrete -> trivial (non empty SubSpace of Y);
 cluster anti-discrete non trivial -> non discrete (non empty SubSpace of Y);
 cluster discrete non trivial -> non anti-discrete (non empty SubSpace of Y);
end;

definition let Y be non empty TopStruct, y be Point of Y;
 func Sspace(y) -> strict non empty SubSpace of Y means
:: TEX_2:def 4
 the carrier of it = {y};
end;

definition let Y be non empty TopStruct;
 cluster trivial strict non empty SubSpace of Y;
end;

definition let Y be non empty TopStruct, y be Point of Y;
 cluster Sspace(y) -> trivial;
end;

theorem :: TEX_2:20
 for Y being non empty TopStruct, y being Point of Y holds
  Sspace(y) is proper iff {y} is proper;

theorem :: TEX_2:21
   for Y being non empty TopStruct, y being Point of Y holds
  Sspace(y) is proper implies Y is non trivial;

theorem :: TEX_2:22
   for Y being non trivial non empty TopStruct, y being Point of Y holds
  Sspace(y) is proper;

definition let Y be non trivial non empty TopStruct;
 cluster proper trivial strict (non empty SubSpace of Y);
end;

theorem :: TEX_2:23
 for Y being non empty TopStruct, Y0 be trivial non empty SubSpace of Y holds
   ex y being Point of Y st the TopStruct of Y0 = the TopStruct of Sspace(y);

theorem :: TEX_2:24
 for Y being non empty TopStruct, y being Point of Y holds
  Sspace(y) is TopSpace-like implies Sspace(y) is discrete anti-discrete;

definition let Y be non empty TopStruct;
 cluster trivial TopSpace-like ->
      discrete anti-discrete (non empty SubSpace of Y);
end;

definition let X be non empty TopSpace;
 cluster trivial strict TopSpace-like non empty SubSpace of X;
end;

definition let X be non empty TopSpace, x be Point of X;
 cluster Sspace(x) -> TopSpace-like;
end;

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

definition let X be non empty TopSpace, x be Point of X;
 cluster Sspace(x) -> discrete anti-discrete;
end;

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

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

definition let X be discrete non empty TopSpace;
 cluster anti-discrete -> trivial (non empty SubSpace of X);
 cluster non trivial -> non anti-discrete (non empty SubSpace of X);
end;

definition let X be discrete non trivial non empty TopSpace;
 cluster discrete open closed proper strict SubSpace of X;
end;

definition let X be anti-discrete non empty TopSpace;
 cluster discrete -> trivial (non empty SubSpace of X);
 cluster non trivial -> non discrete (non empty SubSpace of X);
end;

definition let X be anti-discrete non trivial non empty TopSpace;
 cluster -> non open non closed (proper non empty SubSpace of X);
 cluster -> trivial proper (discrete non empty SubSpace of X);
end;

definition let X be anti-discrete non trivial non empty TopSpace;
 cluster anti-discrete non open non closed proper strict SubSpace of X;
end;

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


begin
:: 3. Maximal Discrete Subsets and Subspaces.

definition let Y be TopStruct,
               IT be Subset of Y;
 attr IT is discrete means
:: TEX_2:def 5
 for D being Subset of Y st D c= IT
   ex G being Subset of Y st G is open & IT /\ G = D;
end;

definition let Y be TopStruct;
  let A be Subset of Y;
 redefine attr A is discrete means
:: TEX_2:def 6
 for D being Subset of Y st D c= A
   ex F being Subset of Y st F is closed & A /\ F = D;
end;

theorem :: TEX_2:25
 for Y0, Y1 being TopStruct, D0 being Subset of Y0,
     D1 being Subset of Y1 st
    the TopStruct of Y0 = the TopStruct of Y1 & D0 = D1 holds
   D0 is discrete implies D1 is discrete;

theorem :: TEX_2:26
 for Y being non empty TopStruct,
  Y0 being non empty SubSpace of Y, A being Subset of Y
  st A = the carrier of Y0 holds
    A is discrete iff Y0 is discrete;

theorem :: TEX_2:27
 for Y being non empty TopStruct, A being Subset of Y
  st A = the carrier of Y
  holds A is discrete iff Y is discrete;

theorem :: TEX_2:28
 for A, B being Subset of Y st B c= A holds
    A is discrete implies B is discrete;

theorem :: TEX_2:29
   for A, B being Subset of Y holds
    A is discrete or B is discrete implies A /\ B is discrete;

theorem :: TEX_2:30
 (for P, Q being Subset of Y st P is open & Q is open holds
     P /\ Q is open & P \/ Q is open)
   implies
       for A, B being Subset of Y st A is open & B is open holds
        A is discrete & B is discrete implies A \/ B is discrete;

theorem :: TEX_2:31
  (for P, Q being Subset of Y st P is closed & Q is closed holds
     P /\ Q is closed & P \/ Q is closed)
   implies
       for A, B being Subset of Y st A is closed & B is closed
       holds
        A is discrete & B is discrete implies A \/ B is discrete;

theorem :: TEX_2:32
 for A being Subset of Y holds A is discrete implies
    for x being Point of Y st x in A
   ex G being Subset of Y st G is open & A /\ G = {x};

theorem :: TEX_2:33
   for A being Subset of Y holds A is discrete implies
    for x being Point of Y st x in A
   ex F being Subset of Y st F is closed & A /\ F = {x};

reserve X for non empty TopSpace;

theorem :: TEX_2:34
 for A0 being non empty Subset of X st A0 is discrete
  ex X0 being discrete strict non empty SubSpace of X st A0 = the carrier of X0
;

theorem :: TEX_2:35
 for A being empty Subset of X holds A is discrete;

theorem :: TEX_2:36
 for x being Point of X holds {x} is discrete;

theorem :: TEX_2:37
 for A being Subset of X holds
    (for x being Point of X st x in A
       ex G being Subset of X st G is open & A /\ G = {x})
       implies
   A is discrete;

theorem :: TEX_2:38
   for A, B being Subset of X st A is open & B is open holds
    A is discrete & B is discrete implies A \/ B is discrete;

theorem :: TEX_2:39
   for A, B being Subset of X st A is closed & B is closed holds
    A is discrete & B is discrete implies A \/ B is discrete;

theorem :: TEX_2:40
   for A being Subset of X st A is everywhere_dense holds
   A is discrete implies A is open;

theorem :: TEX_2:41
 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;

theorem :: TEX_2:42
 for A being Subset of X holds A is discrete implies
    for x being Point of X st x in A holds A /\ Cl {x} = {x};

theorem :: TEX_2:43
   for X being discrete non empty TopSpace, A being Subset of X
 holds A is discrete;

theorem :: TEX_2:44
 for X being anti-discrete non empty TopSpace,
     A being non empty Subset of X holds
   A is discrete iff A is trivial;

definition let Y be TopStruct,
               IT be Subset of Y;
 attr IT is maximal_discrete means
:: TEX_2:def 7
 IT is discrete &
   for D being Subset of Y st D is discrete & IT c= D holds IT = D;
end;

theorem :: TEX_2:45
   for Y0, Y1 being TopStruct, D0 being Subset of Y0,
     D1 being Subset of Y1 st
    the TopStruct of Y0 = the TopStruct of Y1 & D0 = D1 holds
   D0 is maximal_discrete implies D1 is maximal_discrete;

theorem :: TEX_2:46
 for A being empty Subset of X holds A is not maximal_discrete;

theorem :: TEX_2:47
 for A being Subset of X st A is open holds
   A is maximal_discrete implies A is dense;

theorem :: TEX_2:48
   for A being Subset of X st A is dense holds
   A is discrete implies A is maximal_discrete;

theorem :: TEX_2:49
 for X being discrete non empty TopSpace, A being Subset of X
 holds A is maximal_discrete iff A is non proper;

theorem :: TEX_2:50
 for X being anti-discrete non empty TopSpace,
     A being non empty Subset of X holds
   A is maximal_discrete iff A is trivial;

definition let Y be non empty TopStruct;
  let IT be SubSpace of Y;
 attr IT is maximal_discrete means
:: TEX_2:def 8
 for A being Subset of Y st A = the carrier of IT holds
    A is maximal_discrete;
end;

theorem :: TEX_2:51
 for Y being non empty TopStruct, Y0 being SubSpace of Y,
     A being Subset of Y st
   A = the carrier of Y0 holds
      A is maximal_discrete iff Y0 is maximal_discrete;

definition let Y be non empty TopStruct;
 cluster maximal_discrete -> discrete (non empty SubSpace of Y);
 cluster non discrete -> non maximal_discrete (non empty SubSpace of Y);
end;

theorem :: TEX_2:52
   for X0 being non empty SubSpace of X holds
  X0 is maximal_discrete iff
     X0 is discrete &
    for Y0 being discrete non empty SubSpace of X st X0 is SubSpace of Y0 holds
                              the TopStruct of X0 = the TopStruct of Y0;

theorem :: TEX_2:53
 for A0 being non empty Subset of X st A0 is maximal_discrete
  ex X0 being strict non empty SubSpace of X st
            X0 is maximal_discrete & A0 = the carrier of X0;

definition let X be discrete non empty TopSpace;
 cluster maximal_discrete -> non proper SubSpace of X;
 cluster proper -> non maximal_discrete SubSpace of X;
 cluster non proper -> maximal_discrete SubSpace of X;
 cluster non maximal_discrete -> proper SubSpace of X;
end;

definition let X be anti-discrete non empty TopSpace;
 cluster maximal_discrete -> trivial (non empty SubSpace of X);
 cluster non trivial -> non maximal_discrete (non empty SubSpace of X);
 cluster trivial -> maximal_discrete (non empty SubSpace of X);
 cluster non maximal_discrete -> non trivial (non empty SubSpace of X);
end;


begin
:: 4. Maximal Discrete Subspaces of Almost Discrete Spaces.

scheme
 ExChoiceFCol{X()->non empty TopStruct,F()->Subset-Family of X(),P[set,set]}:
 ex f being Function of F(),the carrier of X() st
  for S being Subset of X() st S in F() holds P[S,f.S]
 provided
   for S being Subset of X() st S in F()
                   ex x being Point of X() st P[S,x];

reserve X for almost_discrete non empty TopSpace;

theorem :: TEX_2:54
 for A being Subset of X holds
   Cl A = union {Cl {a} where a is Point of X : a in A};

theorem :: TEX_2:55
 for a, b being Point of X holds
   a in Cl {b} implies Cl {a} = Cl {b};

theorem :: TEX_2:56
 for a, b being Point of X holds
   Cl {a} misses Cl {b} or Cl {a} = Cl {b};

theorem :: TEX_2:57
 for A being Subset of X holds
    (for x being Point of X st x in A
       ex F being Subset of X st F is closed & A /\ F = {x})
       implies
   A is discrete;

theorem :: TEX_2:58
 for A being Subset of X holds
    (for x being Point of X st x in A holds A /\ Cl {x} = {x}) implies
   A is discrete;

theorem :: TEX_2:59
   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 holds
                          a <> b implies Cl {a} misses Cl {b};

theorem :: TEX_2:60
 for A being Subset of X holds
   A is discrete iff
      for x being Point of X st x in Cl A
        ex a being Point of X st a in A & A /\ Cl {x} = {a};

theorem :: TEX_2:61
   for A being Subset of X st A is open or A is closed holds
   A is maximal_discrete implies A is not proper;

theorem :: TEX_2:62
 for A being Subset of X holds
   A is maximal_discrete implies A is dense;

theorem :: TEX_2:63
 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;

theorem :: TEX_2:64
 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};

theorem :: TEX_2:65
 for A being Subset of X holds A is discrete implies
   ex M being Subset of X st A c= M & M is maximal_discrete;

theorem :: TEX_2:66
 ex M being Subset of X st M is maximal_discrete;

theorem :: TEX_2:67
 for Y0 being discrete non empty SubSpace of X
   ex X0 being strict non empty SubSpace of X st
                       Y0 is SubSpace of X0 & X0 is maximal_discrete;

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

definition let X be almost_discrete non anti-discrete non empty TopSpace;
 cluster maximal_discrete -> non trivial (non empty SubSpace of X);
 cluster trivial -> non maximal_discrete (non empty SubSpace of X);
end;

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


begin
:: 5. Continuous Mappings and Almost Discrete Spaces.

scheme MapExChoiceF{X,Y()->non empty TopStruct,P[set,set]}:
 ex f being map of X(),Y() st
  for x being Point of X() holds P[x,f.x]
 provided
   for x being Point of X() ex y being Point of Y() st P[x,y];

reserve X,Y for non empty TopSpace;

theorem :: TEX_2:68
 for X being discrete non empty TopSpace, f being map of X,Y holds
   f is continuous;

theorem :: TEX_2:69
   (for Y being non empty TopSpace, f being map of X,Y holds f is continuous)
    implies X is discrete;

theorem :: TEX_2:70
   for Y being anti-discrete non empty TopSpace, f being map of X,Y holds
   f is continuous;

theorem :: TEX_2:71
   (for X being non empty TopSpace, f being map of X,Y holds f is continuous)
    implies Y is anti-discrete;

reserve X for discrete non empty TopSpace, X0 for non empty SubSpace of X;

theorem :: TEX_2:72
 ex r being continuous map of X,X0 st r is_a_retraction;

theorem :: TEX_2:73
   X0 is_a_retract_of X;

reserve X for almost_discrete non empty TopSpace,
        X0 for maximal_discrete non empty SubSpace of X;

theorem :: TEX_2:74
 ex r being continuous map of X,X0 st r is_a_retraction;

theorem :: TEX_2:75
   X0 is_a_retract_of X;

theorem :: TEX_2:76
 for r being continuous map of X,X0 holds
   r is_a_retraction implies
  for F being Subset of X0, E being Subset of X
  st F = E holds r" F = Cl E;

theorem :: TEX_2:77
   for r being continuous map of X,X0 holds
   r is_a_retraction implies
  for a being Point of X0, b being Point of X st a = b holds r" {a} = Cl {b};

reserve X0 for discrete non empty SubSpace of X;

theorem :: TEX_2:78
 ex r being continuous map of X,X0 st r is_a_retraction;

theorem :: TEX_2:79
   X0 is_a_retract_of X;