The abstract of the Mizar article:

Maximal Anti-Discrete Subspaces of Topological Spaces

by

Zbigniew Karno

Received July 26, 1994

MML identifier: TEX_4

[ Mizar article, MML identifier index ]

environ

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


begin
:: 1. Properties of the Closure and the Interior Operations.

definition
 let X be non empty TopSpace, A be non empty Subset of X;
 cluster Cl A -> non empty;
end;

definition let X be non empty TopSpace, A be empty Subset of X;
 cluster Cl A -> empty;
end;

definition
 let X be non empty TopSpace, A be non proper Subset of X;
 cluster Cl A -> non proper;
end;

definition let X be non trivial non empty TopSpace,
                A be non trivial (non empty Subset of X);
 cluster Cl A -> non trivial;
end;

reserve X for non empty TopSpace;

theorem :: TEX_4:1
 for A being Subset of X holds
   Cl A = meet {F where F is Subset of X : F is closed & A c= F};

theorem :: TEX_4:2
 for x being Point of X holds
   Cl {x} = meet {F where F is Subset of X : F is closed & x in F};

theorem :: TEX_4:3
 for A, B being Subset of X holds B c= Cl A implies Cl B c= Cl A;

definition
 let X be non empty TopSpace, A be non proper Subset of X;
 cluster Int A -> non proper;
end;

definition let X be non empty TopSpace, A be proper Subset of X;
 cluster Int A -> proper;
end;

definition let X be non empty TopSpace, A be empty Subset of X;
 cluster Int A -> empty;
end;

theorem :: TEX_4:4
   for A being Subset of X holds
   Int A = union {G where G is Subset of X : G is open & G c= A};

theorem :: TEX_4:5
   for A, B being Subset of X holds Int A c= B
  implies Int A c= Int B;

begin
:: 2. Anti-discrete Subsets of Topological Structures.

definition let Y be TopStruct;
  let IT be Subset of Y;
 attr IT is anti-discrete means
:: TEX_4:def 1
 for x being Point of Y, G being Subset of Y st
    G is open & x in G holds x in IT implies IT c= G;
end;

definition let Y be non empty TopStruct;
  let A be Subset of Y;
 redefine attr A is anti-discrete means
:: TEX_4:def 2
 for x being Point of Y, F being Subset of Y st
    F is closed & x in F holds x in A implies A c= F;
end;

definition let Y be TopStruct;
  let A be Subset of Y;
 redefine attr A is anti-discrete means
:: TEX_4:def 3
 for G being Subset of Y st G is open holds A misses G or A c= G;
end;

definition let Y be TopStruct;
  let A be Subset of Y;
 redefine attr A is anti-discrete means
:: TEX_4:def 4
 for F being Subset of Y st F is closed holds A misses F or A c= F;
end;

theorem :: TEX_4:6
 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 anti-discrete implies D1 is anti-discrete;

reserve Y for non empty TopStruct;

theorem :: TEX_4:7
 for A, B being Subset of Y st B c= A holds
    A is anti-discrete implies B is anti-discrete;

theorem :: TEX_4:8
 for x being Point of Y holds {x} is anti-discrete;

theorem :: TEX_4:9
 for A being empty Subset of Y holds A is anti-discrete;

definition let Y be TopStruct;
  let IT be Subset-Family of Y;
 attr IT is anti-discrete-set-family means
:: TEX_4:def 5
 for A being Subset of Y st A in IT holds A is anti-discrete;
end;

theorem :: TEX_4:10
 for F being Subset-Family of Y st F is anti-discrete-set-family holds
  meet F <> {} implies union F is anti-discrete;

theorem :: TEX_4:11
   for F being Subset-Family of Y st F is anti-discrete-set-family holds
  meet F is anti-discrete;

definition let Y be TopStruct, x be Point of Y;
 func MaxADSF(x) -> Subset-Family of Y equals
:: TEX_4:def 6
 {A where A is Subset of Y : A is anti-discrete & x in A};
end;

definition let Y be non empty TopStruct, x be Point of Y;
 cluster MaxADSF(x) -> non empty;
end;

reserve x for Point of Y;

theorem :: TEX_4:12
 MaxADSF(x) is anti-discrete-set-family;

theorem :: TEX_4:13
 {x} = meet MaxADSF(x);

theorem :: TEX_4:14
 {x} c= union MaxADSF(x);

theorem :: TEX_4:15
 union MaxADSF(x) is anti-discrete;


begin
:: 3. Maximal Anti-discrete Subsets of Topological Structures.

definition let Y be TopStruct;
  let IT be Subset of Y;
 attr IT is maximal_anti-discrete means
:: TEX_4:def 7
 IT is anti-discrete &
   for D being Subset of Y st D is anti-discrete & IT c= D holds IT = D;
end;

theorem :: TEX_4:16
   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_anti-discrete implies D1 is maximal_anti-discrete;

reserve Y for non empty TopStruct;

theorem :: TEX_4:17
 for A being empty Subset of Y holds A is not maximal_anti-discrete;

theorem :: TEX_4:18
 for A being non empty Subset of Y holds
  A is anti-discrete & A is open implies A is maximal_anti-discrete;

theorem :: TEX_4:19
 for A being non empty Subset of Y holds
  A is anti-discrete & A is closed implies A is maximal_anti-discrete;

definition let Y be TopStruct, x be Point of Y;
 func MaxADSet(x) -> Subset of Y equals
:: TEX_4:def 8
 union MaxADSF(x);
end;

definition let Y be non empty TopStruct, x be Point of Y;
 cluster MaxADSet(x) -> non empty;
end;

theorem :: TEX_4:20
 for x being Point of Y holds {x} c= MaxADSet(x);

theorem :: TEX_4:21
 for D being Subset of Y, x being Point of Y st
    D is anti-discrete & x in D holds D c= MaxADSet(x);

theorem :: TEX_4:22
 for x being Point of Y holds
   MaxADSet(x) is maximal_anti-discrete;

theorem :: TEX_4:23
 for x, y being Point of Y holds
   y in MaxADSet(x) iff MaxADSet(y) = MaxADSet(x);

theorem :: TEX_4:24
 for x, y being Point of Y holds
   MaxADSet(x) misses MaxADSet(y) or MaxADSet(x) = MaxADSet(y);

theorem :: TEX_4:25
 for F being Subset of Y, x being Point of Y st F is closed & x in F holds
   MaxADSet(x) c= F;

theorem :: TEX_4:26
 for G being Subset of Y, x being Point of Y st G is open & x in G holds
   MaxADSet(x) c= G;

theorem :: TEX_4:27
   for x being Point of Y holds
   {F where F is Subset of Y : F is closed & x in F} <> {} implies
  MaxADSet(x) c= meet {F where F is Subset of Y : F is closed & x in F};

theorem :: TEX_4:28
   for x being Point of Y holds
   {G where G is Subset of Y : G is open & x in G} <> {} implies
  MaxADSet(x) c= meet {G where G is Subset of Y : G is open & x in G};

definition let Y be non empty TopStruct;
  let A be Subset of Y;
 redefine attr A is maximal_anti-discrete means
:: TEX_4:def 9
 ex x being Point of Y st x in A & A = MaxADSet(x);
end;

theorem :: TEX_4:29
 for A being Subset of Y, x being Point of Y st x in A holds
   A is maximal_anti-discrete implies A = MaxADSet(x);

definition let Y be non empty TopStruct;
  let A be non empty Subset of Y;
 redefine attr A is maximal_anti-discrete means
:: TEX_4:def 10
   for x being Point of Y st x in A holds A = MaxADSet(x);
end;

definition let Y be non empty TopStruct, A be Subset of Y;
 func MaxADSet(A) -> Subset of Y equals
:: TEX_4:def 11
 union {MaxADSet(a) where a is Point of Y : a in A};
end;

theorem :: TEX_4:30
 for x being Point of Y holds MaxADSet(x) = MaxADSet({x});

theorem :: TEX_4:31
 for A being Subset of Y, x being Point of Y holds
  MaxADSet(x) meets MaxADSet(A) implies MaxADSet(x) meets A;

theorem :: TEX_4:32
 for A being Subset of Y, x being Point of Y holds
  MaxADSet(x) meets MaxADSet(A) implies MaxADSet(x) c= MaxADSet(A);

theorem :: TEX_4:33
 for A, B being Subset of Y holds A c= B
   implies MaxADSet(A) c= MaxADSet(B);

theorem :: TEX_4:34
 for A being Subset of Y holds A c= MaxADSet(A);

theorem :: TEX_4:35
 for A being Subset of Y
   holds MaxADSet(A) = MaxADSet(MaxADSet(A));

theorem :: TEX_4:36
 for A, B being Subset of Y holds
    A c= MaxADSet(B) implies MaxADSet(A) c= MaxADSet(B);

theorem :: TEX_4:37
 for A, B being Subset of Y holds
   B c= MaxADSet(A) & A c= MaxADSet(B) iff MaxADSet(A) = MaxADSet(B);

theorem :: TEX_4:38
   for A, B being Subset of Y
   holds MaxADSet(A \/ B) = MaxADSet(A) \/ MaxADSet(B);

theorem :: TEX_4:39
 for A, B being Subset of Y
  holds MaxADSet(A /\ B) c= MaxADSet(A) /\ MaxADSet(B);

definition let Y be non empty TopStruct,
  A be non empty Subset of Y;
 cluster MaxADSet(A) -> non empty;
end;

definition let Y be non empty TopStruct, A be empty Subset of Y;
 cluster MaxADSet(A) -> empty;
end;

definition let Y be non empty TopStruct,
   A be non proper Subset of Y;
 cluster MaxADSet(A) -> non proper;
end;

definition let Y be non trivial non empty TopStruct,
                A be non trivial (non empty Subset of Y);
 cluster MaxADSet(A) -> non trivial;
end;

theorem :: TEX_4:40
 for G being Subset of Y, A being Subset of Y
    st G is open & A c= G holds MaxADSet(A) c= G;

theorem :: TEX_4:41
 for A being Subset of Y holds
   {G where G is Subset of Y : G is open & A c= G} <> {} implies
  MaxADSet(A) c= meet {G where G is Subset of Y : G is open & A c= G};

theorem :: TEX_4:42
 for F being Subset of Y, A being Subset of Y
    st F is closed & A c= F holds
   MaxADSet(A) c= F;

theorem :: TEX_4:43
 for A being Subset of Y holds
   {F where F is Subset of Y : F is closed & A c= F} <> {}
   implies
  MaxADSet(A) c= meet {F where F is Subset of Y : F is closed & A c= F};


begin
:: 4. Anti-discrete and Maximal Anti-discrete Subsets of Topological Spaces.

definition let X be non empty TopSpace;
  let A be Subset of X;
 redefine attr A is anti-discrete means
:: TEX_4:def 12
 for x being Point of X st x in A holds A c= Cl {x};
end;

definition let X be non empty TopSpace;
  let A be Subset of X;
 redefine attr A is anti-discrete means
:: TEX_4:def 13
   for x being Point of X st x in A holds Cl A = Cl {x};
end;

definition let X be non empty TopSpace;
  let A be Subset of X;
 redefine attr A is anti-discrete means
:: TEX_4:def 14
 for x, y being Point of X st x in A & y in A holds Cl {x} = Cl {y};
end;

reserve X for non empty TopSpace;

theorem :: TEX_4:44
   for x being Point of X, D being Subset of X st
   D is anti-discrete & Cl {x} c= D holds D = Cl {x};

theorem :: TEX_4:45
   for A being Subset of X holds
    A is anti-discrete & A is closed iff
   for x being Point of X st x in A holds A = Cl {x};

theorem :: TEX_4:46
   for A being Subset of X holds
    A is anti-discrete & A is not open implies A is boundary;

theorem :: TEX_4:47
 for x being Point of X st Cl {x} = {x} holds
   {x} is maximal_anti-discrete;

reserve x,y for Point of X;

theorem :: TEX_4:48
 MaxADSet(x) c= meet {G where G is Subset of X : G is open & x in G};

theorem :: TEX_4:49
 MaxADSet(x) c= meet {F where F is Subset of X : F is closed & x in F};

theorem :: TEX_4:50
 MaxADSet(x) c= Cl {x};

theorem :: TEX_4:51
 MaxADSet(x) = MaxADSet(y) iff Cl {x} = Cl {y};

theorem :: TEX_4:52
   MaxADSet(x) misses MaxADSet(y) iff Cl {x} <> Cl {y};

definition let X be non empty TopSpace, x be Point of X;
 redefine func MaxADSet(x) -> non empty Subset of X equals
:: TEX_4:def 15
 (Cl {x}) /\ meet {G where G is Subset of X : G is open & x in G};
end;

theorem :: TEX_4:53
 for x, y being Point of X holds
  Cl {x} c= Cl {y} iff
      meet {G where G is Subset of X : G is open & y in G} c=
         meet {G where G is Subset of X : G is open & x in G};

theorem :: TEX_4:54
   for x, y being Point of X holds
  Cl {x} c= Cl {y} iff
     MaxADSet(y) c=
       meet {G where G is Subset of X : G is open & x in G};

theorem :: TEX_4:55
 for x, y being Point of X holds
  MaxADSet(x) misses MaxADSet(y) iff
   (ex V being Subset of X st
        V is open & MaxADSet(x) c= V & V misses MaxADSet(y)) or
    (ex W being Subset of X st
         W is open & W misses MaxADSet(x) & MaxADSet(y) c= W);

theorem :: TEX_4:56
   for x, y being Point of X holds
  MaxADSet(x) misses MaxADSet(y) iff
   (ex E being Subset of X st
        E is closed & MaxADSet(x) c= E & E misses MaxADSet(y)) or
    (ex F being Subset of X st
         F is closed & F misses MaxADSet(x) & MaxADSet(y) c= F);

reserve A, B for Subset of X;
reserve P, Q for Subset of X;

theorem :: TEX_4:57
 MaxADSet(A) c= meet {G where G is Subset of X : G is open & A c= G};

theorem :: TEX_4:58
 P is open implies MaxADSet(P) = P;

theorem :: TEX_4:59
   MaxADSet(Int A) = Int A;

theorem :: TEX_4:60
 MaxADSet(A) c= meet {F where F is Subset of X : F is closed & A c= F};

theorem :: TEX_4:61
 MaxADSet(A) c= Cl A;

theorem :: TEX_4:62
 P is closed implies MaxADSet(P) = P;

theorem :: TEX_4:63
   MaxADSet(Cl A) = Cl A;

theorem :: TEX_4:64
   Cl MaxADSet(A) = Cl A;

theorem :: TEX_4:65
   MaxADSet(A) = MaxADSet(B) implies Cl A = Cl B;

theorem :: TEX_4:66
   P is closed or Q is closed implies
    MaxADSet(P /\ Q) = MaxADSet(P) /\ MaxADSet(Q);

theorem :: TEX_4:67
   P is open or Q is open implies
    MaxADSet(P /\ Q) = MaxADSet(P) /\ MaxADSet(Q);


begin
:: 5. Maximal Anti-discrete Subspaces.
reserve Y for non empty TopStruct;

theorem :: TEX_4:68
 for Y0 being SubSpace of Y, A being Subset of Y
    st A = the carrier of Y0 holds
  Y0 is anti-discrete implies A is anti-discrete;

theorem :: TEX_4:69
 for Y0 being SubSpace of Y st Y0 is TopSpace-like
  for A being Subset of Y st A = the carrier of Y0 holds
               A is anti-discrete implies Y0 is anti-discrete;

reserve X for non empty TopSpace, Y0 for non empty SubSpace of X;

theorem :: TEX_4:70
   (for X0 being open SubSpace of X holds
      Y0 misses X0 or Y0 is SubSpace of X0) implies Y0 is anti-discrete;

theorem :: TEX_4:71
   (for X0 being closed SubSpace of X holds
      Y0 misses X0 or Y0 is SubSpace of X0) implies Y0 is anti-discrete;

theorem :: TEX_4:72
   for Y0 being anti-discrete SubSpace of X
  for X0 being open SubSpace of X holds Y0 misses X0 or Y0 is SubSpace of X0;

theorem :: TEX_4:73
   for Y0 being anti-discrete SubSpace of X
  for X0 being closed SubSpace of X holds Y0 misses X0 or Y0 is SubSpace of X0;

definition let Y be non empty TopStruct;
  let IT be SubSpace of Y;
 attr IT is maximal_anti-discrete means
:: TEX_4:def 16
 IT is anti-discrete &
   for Y0 being SubSpace of Y st Y0 is anti-discrete holds
              the carrier of IT c= the carrier of Y0 implies
                           the carrier of IT = the carrier of Y0;
end;

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

theorem :: TEX_4:74
 for Y0 being non empty SubSpace of X, A being Subset of X
    st A = the carrier of Y0 holds
  Y0 is maximal_anti-discrete iff A is maximal_anti-discrete;

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

definition let Y be TopStruct, x be Point of Y;
 func MaxADSspace(x) -> strict SubSpace of Y means
:: TEX_4:def 17
 the carrier of it = MaxADSet(x);
end;

definition let Y be non empty TopStruct, x be Point of Y;
 cluster MaxADSspace(x) -> non empty;
end;

theorem :: TEX_4:75
   for x being Point of Y holds Sspace(x) is SubSpace of MaxADSspace(x);

theorem :: TEX_4:76
   for x, y being Point of Y holds
   y is Point of MaxADSspace(x) iff
      the TopStruct of MaxADSspace(y) = the TopStruct of MaxADSspace(x);

theorem :: TEX_4:77
   for x, y being Point of Y holds
   the carrier of MaxADSspace(x) misses the carrier of MaxADSspace(y) or
     the TopStruct of MaxADSspace(x) = the TopStruct of MaxADSspace(y);

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

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

theorem :: TEX_4:78
   for X0 being closed non empty SubSpace of X, x being Point of X holds
  x is Point of X0 implies MaxADSspace(x) is SubSpace of X0;

theorem :: TEX_4:79
   for X0 being open non empty SubSpace of X, x being Point of X holds
  x is Point of X0 implies MaxADSspace(x) is SubSpace of X0;

theorem :: TEX_4:80
   for x being Point of X st Cl {x} = {x} holds
   Sspace(x) is maximal_anti-discrete;

definition let Y be TopStruct,
  A be Subset of Y;
 func Sspace(A) -> strict SubSpace of Y means
:: TEX_4:def 18
 the carrier of it = A;
end;

definition let Y be non empty TopStruct,
  A be non empty Subset of Y;
 cluster Sspace(A) -> non empty;
end;

theorem :: TEX_4:81
   for A being non empty Subset of Y
   holds A is Subset of Sspace(A);

theorem :: TEX_4:82
   for Y0 being SubSpace of Y, A being non empty Subset of Y
holds
              A is Subset of Y0
              implies Sspace(A) is SubSpace of Y0;

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

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

definition let Y be non empty TopStruct,
  A be non proper non empty Subset of Y;
 cluster Sspace(A) -> non proper;
end;

definition let Y be non empty TopStruct,
   A be Subset of Y;
 func MaxADSspace(A) -> strict SubSpace of Y means
:: TEX_4:def 19
 the carrier of it = MaxADSet(A);
end;

definition let Y be non empty TopStruct,
   A be non empty Subset of Y;
 cluster MaxADSspace(A) -> non empty;
end;

theorem :: TEX_4:83
   for A being non empty Subset of Y
   holds A is Subset of MaxADSspace(A);

theorem :: TEX_4:84
   for A being non empty Subset of Y holds
   Sspace(A) is SubSpace of MaxADSspace(A);

theorem :: TEX_4:85
   for x being Point of Y holds
   the TopStruct of MaxADSspace(x) = the TopStruct of MaxADSspace({x});

theorem :: TEX_4:86
   for A, B being non empty Subset of Y holds
   A c= B implies MaxADSspace(A) is SubSpace of MaxADSspace(B);

theorem :: TEX_4:87
   for A being non empty Subset of Y holds
  the TopStruct of MaxADSspace(A) = the TopStruct of MaxADSspace(MaxADSet(A));

theorem :: TEX_4:88
   for A, B being non empty Subset of Y holds
  A is Subset of MaxADSspace(B) implies
    MaxADSspace(A) is SubSpace of MaxADSspace(B);

theorem :: TEX_4:89
   for A, B being non empty Subset of Y holds
   B is Subset of MaxADSspace(A) &
   A is Subset of MaxADSspace(B) iff
    the TopStruct of MaxADSspace(A) = the TopStruct of MaxADSspace(B);

definition let Y be non trivial non empty TopStruct,
                A be non trivial (non empty Subset of Y);
 cluster MaxADSspace(A) -> non trivial;
end;

definition let Y be non empty TopStruct,
   A be non proper non empty Subset of Y;
 cluster MaxADSspace(A) -> non proper;
end;

theorem :: TEX_4:90
   for X0 being open SubSpace of X, A being non empty Subset of
X
   holds A is Subset of X0
     implies MaxADSspace(A) is SubSpace of X0;

theorem :: TEX_4:91
   for X0 being closed SubSpace of X,
     A being non empty Subset of X holds
     A is Subset of X0 implies MaxADSspace(A) is SubSpace of X0;