Journal of Formalized Mathematics
Volume 6, 1994
University of Bialystok
Copyright (c) 1994 Association of Mizar Users

### On Kolmogorov Topological Spaces

by
Zbigniew Karno

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;
```