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

## On Kolmogorov Topological Spaces

Zbigniew Karno
Warsaw University, Bialystok

### Summary.

Let $X$ be a topological space. $X$ is said to be {\em $T_{0}$-space}\/ (or {\em Kolmogorov space}) provided for every pair of distinct points $x,\,y \in X$ there exists an open subset of $X$ containing exactly one of these points; equivalently, for every pair of distinct points $x,\,y \in X$ there exists a closed subset of $X$ containing exactly one of these points (see [1], [6], [2]).\par The purpose is to list some of the standard facts on Kolmogorov spaces, using Mizar formalism. As a sample we formulate the following characteristics of such spaces: {\em $X$ is a Kolmogorov space iff for every pair of distinct points $x,\,y \in X$ the closures $\overline{\{x\}}$ and $\overline{\{y\}}$ are distinct}.\par There is also reviewed analogous facts on Kolmogorov subspaces of topological spaces. In the presented approach $T_{0}$-subsets are introduced and some of their properties developed.

Presented at Mizar Conference: Mathematics in Mizar (Bia{\l}ystok, September 12--14, 1994).

#### MML Identifier: TSP_1

The terminology and notation used in this paper have been introduced in the following articles [8] [10] [7] [9] [3] [4] [11] [5]

#### Contents (PDF format)

1. Subspaces
2. Kolmogorov Spaces
3. $T_{0}$-Subsets
4. Kolmogorov Subspaces

#### Bibliography

[1] P. Alexandroff and H. H. Hopf. \em Topologie I. Springer-Verlag, Berlin, 1935.
[2] Ryszard Engelking. \em General Topology, volume 60 of \em Monografie Matematyczne. PWN - Polish Scientific Publishers, Warsaw, 1977.
[3] Zbigniew Karno. Separated and weakly separated subspaces of topological spaces. Journal of Formalized Mathematics, 4, 1992.
[4] Zbigniew Karno. Maximal discrete subspaces of almost discrete topological spaces. Journal of Formalized Mathematics, 5, 1993.
[5] Zbigniew Karno. Maximal anti-discrete subspaces of topological spaces. Journal of Formalized Mathematics, 6, 1994.
[6] Kazimierz Kuratowski. \em Topology, volume I. PWN - Polish Scientific Publishers, Academic Press, Warsaw, New York and London, 1966.
[7] Beata Padlewska and Agata Darmochwal. Topological spaces and continuous functions. Journal of Formalized Mathematics, 1, 1989.
[8] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[9] Andrzej Trybulec. A Borsuk theorem on homotopy types. Journal of Formalized Mathematics, 3, 1991.
[10] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[11] Mariusz Zynel and Adam Guzowski. \Tzero\ topological spaces. Journal of Formalized Mathematics, 6, 1994.