Volume 6, 1994

University of Bialystok

Copyright (c) 1994 Association of Mizar Users

**Zbigniew Karno**- Warsaw University, Bialystok

- 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).

- Subspaces
- Kolmogorov Spaces
- $T_{0}$-Subsets
- Kolmogorov Subspaces

- [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.

[ Download a postscript version, MML identifier index, Mizar home page]