The abstract of the Mizar article:

On Kolmogorov Topological Spaces

by

Zbigniew Karno

Received July 26, 1994

MML identifier: TSP_1

[ Mizar article, MML identifier index ]

environ

 vocabulary PRE_TOPC, BOOLE, SUBSET_1, METRIC_1, REALSET1, TDLAT_3, NATTRA_1,
      SETFAM_1, TARSKI, COLLSP, TSP_1;
 notation TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, BORSUK_1, TSEP_1,
      TDLAT_3, TEX_1, TEX_2, T_0TOPSP, TEX_4;
 constructors REALSET1, TSEP_1, TDLAT_3, TEX_2, T_0TOPSP, TEX_4, BORSUK_1,
      MEMBERED;
 clusters TDLAT_3, TEX_1, TEX_2, STRUCT_0, MEMBERED, ZFMISC_1;
 requirements SUBSET, BOOLE;


begin
:: 1. Subspaces.

definition let Y be TopStruct;
 redefine mode SubSpace of Y -> TopStruct means
:: TSP_1:def 1
 the carrier of it c= the carrier of Y &
 for G0 being Subset of it holds G0 is open iff
   ex G being Subset of Y
      st G is open & G0 = G /\ the carrier of it;
end;

canceled;

theorem :: TSP_1:2
 for Y being TopStruct, Y0 being SubSpace of Y
  for G being Subset of Y st G is open holds
    ex G0 being Subset of Y0
    st G0 is open & G0 = G /\ the carrier of Y0;

definition let Y be TopStruct;
 redefine
 mode SubSpace of Y -> TopStruct means
:: TSP_1:def 2
 the carrier of it c= the carrier of Y &
 for F0 being Subset of it holds F0 is closed iff
   ex F being Subset of Y
   st F is closed & F0 = F /\ the carrier of it;
end;

canceled;

theorem :: TSP_1:4
 for Y being TopStruct, Y0 being SubSpace of Y
  for F being Subset of Y st F is closed holds
    ex F0 being Subset of Y0
    st F0 is closed & F0 = F /\ the carrier of Y0;


begin
:: 2. Kolmogorov Spaces.

definition let T be TopStruct;
 redefine attr T is discerning means
:: TSP_1:def 3
 T is empty or
   for x, y being Point of T st x <> y holds
   (ex V being Subset of T st V is open & x in V & not y in V) or
   (ex W being Subset of T st W is open & not x in W & y in W);
 synonym T is T_0;
end;

definition let Y be TopStruct;
 redefine attr Y is T_0 means
:: TSP_1:def 4
 Y is empty or
  for x, y being Point of Y st x <> y holds
   (ex E being Subset of Y st E is closed & x in E & not y in E)
   or
   (ex F being Subset of Y st F is closed & not x in F & y in F);
end;

definition
 cluster trivial -> T_0 (non empty TopStruct);
 cluster non T_0 -> non trivial (non empty TopStruct);
end;

definition
 cluster strict T_0 non empty TopSpace;
 cluster strict non T_0 non empty TopSpace;
end;

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

definition let X be non empty TopSpace;
 redefine attr X is T_0 means
:: TSP_1:def 5
 for x, y being Point of X st x <> y holds Cl {x} <> Cl {y};
end;

definition let X be non empty TopSpace;
 redefine attr X is T_0 means
:: TSP_1:def 6
 for x, y being Point of X st x <> y holds
            not x in Cl {y} or not y in Cl {x};
end;

definition let X be non empty TopSpace;
 redefine attr X is T_0 means
:: TSP_1:def 7
   for x, y being Point of X st x <> y & x in Cl {y} holds
                                   not Cl {y} c= Cl {x};
end;

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

definition
 mode Kolmogorov_space is T_0 non empty TopSpace;
 mode non-Kolmogorov_space is non T_0 non empty TopSpace;
end;

definition
 cluster non trivial strict Kolmogorov_space;
 cluster non trivial strict non-Kolmogorov_space;
end;


begin
:: 3. T_{0} Subsets.

definition let Y be TopStruct;
  let IT be Subset of Y;
 attr IT is T_0 means
:: TSP_1:def 8
 for x, y being Point of Y st x in IT & y in IT & x <> y holds
   (ex V being Subset of Y st V is open & x in V & not y in V) or
       (ex W being Subset of Y st W is open & not x in W & y in W);
end;

definition let Y be non empty TopStruct;
  let A be Subset of Y;
 redefine attr A is T_0 means
:: TSP_1:def 9
 for x, y being Point of Y st x in A & y in A & x <> y holds
   (ex E being Subset of Y st E is closed & x in E & not y in E)
   or
   (ex F being Subset of Y st F is closed & not x in F & y in F);
end;

theorem :: TSP_1:5
   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 T_0 implies D1 is T_0;

theorem :: TSP_1:6
 for Y being non empty TopStruct, A being Subset of Y
   st A = the carrier of Y
  holds A is T_0 iff Y is T_0;

reserve Y for non empty TopStruct;

theorem :: TSP_1:7
 for A, B being Subset of Y st B c= A
   holds A is T_0 implies B is T_0;

theorem :: TSP_1:8
 for A, B being Subset of Y
    holds A is T_0 or B is T_0 implies A /\ B is T_0;

theorem :: TSP_1:9
 for A, B being Subset of Y st A is open or B is open holds
                     A is T_0 & B is T_0 implies A \/ B is T_0;

theorem :: TSP_1:10
 for A, B being Subset of Y st A is closed or B is closed holds
                         A is T_0 & B is T_0 implies A \/ B is T_0;

theorem :: TSP_1:11
 for A being Subset of Y holds A is discrete implies A is T_0;

theorem :: TSP_1:12
   for A being non empty Subset of Y holds
  A is anti-discrete & A is not trivial implies A is not T_0;

definition let X be non empty TopSpace;
  let A be Subset of X;
 redefine attr A is T_0 means
:: TSP_1:def 10
 for x, y being Point of X st x in A & y in A & x <> y holds
                                            Cl {x} <> Cl {y};
end;

definition let X be non empty TopSpace;
  let A be Subset of X;
 redefine attr A is T_0 means
:: TSP_1:def 11
 for x, y being Point of X st x in A & y in A & x <> y holds
                                  not x in Cl {y} or not y in Cl {x};
end;

definition let X be non empty TopSpace;
  let A be Subset of X;
 redefine attr A is T_0 means
:: TSP_1:def 12
   for x, y being Point of X st x in A & y in A & x <> y holds
                      x in Cl {y} implies not Cl {y} c= Cl {x};
end;

reserve X for non empty TopSpace;

theorem :: TSP_1:13
 for A being empty Subset of X holds A is T_0;

theorem :: TSP_1:14
   for x being Point of X holds {x} is T_0;


begin
:: 4. Kolmogorov Subspaces.

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

definition let Y be TopStruct;
  let Y0 be SubSpace of Y;
 redefine attr Y0 is T_0 means
:: TSP_1:def 13
   Y0 is empty or
 for x, y being Point of Y st
      x is Point of Y0 & y is Point of Y0 & x <> y holds
   (ex V being Subset of Y st V is open & x in V & not y in V) or
       (ex W being Subset of Y
          st W is open & not x in W & y in W);
end;

definition let Y be TopStruct;
  let Y0 be SubSpace of Y;
 redefine attr Y0 is T_0 means
:: TSP_1:def 14
 Y0 is empty or
   for x, y being Point of Y st
      x is Point of Y0 & y is Point of Y0 & x <> y holds
   (ex E being Subset of Y
      st E is closed & x in E & not y in E) or
       (ex F being Subset of Y
       st F is closed & not x in F & y in F);
end;

reserve Y for non empty TopStruct;

theorem :: TSP_1:15
 for Y0 being non empty SubSpace of Y, A being Subset of Y st
                          A = the carrier of Y0 holds A is T_0 iff Y0 is T_0;

theorem :: TSP_1:16
   for Y0 being non empty SubSpace of Y,
     Y1 being T_0 non empty SubSpace of Y st
                       Y0 is SubSpace of Y1 holds Y0 is T_0;

reserve X for non empty TopSpace;

theorem :: TSP_1:17
   for X1 being T_0 non empty SubSpace of X, X2 being non empty SubSpace of X
 holds X1 meets X2 implies X1 meet X2 is T_0;

theorem :: TSP_1:18
   for X1, X2 being T_0 non empty SubSpace of X holds
  X1 is open or X2 is open implies X1 union X2 is T_0;

theorem :: TSP_1:19
   for X1, X2 being T_0 non empty SubSpace of X holds
   X1 is closed or X2 is closed implies X1 union X2 is T_0;

definition let X be non empty TopSpace;
 mode Kolmogorov_subspace of X is T_0 non empty SubSpace of X;
end;

theorem :: TSP_1:20
   for X being non empty TopSpace,
    A0 being non empty Subset of X st A0 is T_0
  ex X0 being strict Kolmogorov_subspace of X st A0 = the carrier of X0;

definition let X be non trivial (non empty TopSpace);
 cluster proper strict Kolmogorov_subspace of X;
end;

definition let X be Kolmogorov_space;
 cluster -> T_0 (non empty SubSpace of X);
end;

definition let X be non-Kolmogorov_space;
 cluster non proper -> non T_0 (non empty SubSpace of X);
 cluster T_0 -> proper (non empty SubSpace of X);
end;

definition let X be non-Kolmogorov_space;
 cluster strict non T_0 SubSpace of X;
end;

definition let X be non-Kolmogorov_space;
 mode non-Kolmogorov_subspace of X is non T_0 SubSpace of X;
end;

theorem :: TSP_1:21
   for X being non empty non-Kolmogorov_space,
    A0 being Subset of X st A0 is not T_0
  ex X0 being strict non-Kolmogorov_subspace of X st A0 = the carrier of X0;