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

## Maximal Kolmogorov Subspaces of a Topological Space as Stone Retracts of the Ambient Space

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 (see [1], [9], [5]). Such spaces and subspaces were investigated in Mizar formalism in [8]. A Kolmogorov subspace $X_{0}$ of a topological space $X$ is said to be {\em maximal}\/ provided for every Kolmogorov subspace $Y$ of $X$ if $X_{0}$ is subspace of $Y$ then the topological structures of $Y$ and $X_{0}$ are the same.\par M.H.~Stone proved in [11] that every topological space can be made into a Kolmogorov space by identifying points with the same closure (see also [12]). The purpose is to generalize the Stone result, using Mizar System. It is shown here that: (1) {\em in every topological space $X$ there exists a maximal Kolmogorov subspace $X_{0}$ of $X$}, and (2) {\em every maximal Kolmogorov subspace $X_{0}$ of $X$ is a continuous retract of $X$}. Moreover, {\em if $r : X \rightarrow X_{0}$ is a continuous retraction of $X$ onto a maximal Kolmogorov subspace $X_{0}$ of $X$, then $r^{-1}(x) = {\rm MaxADSet}(x)$ for any point $x$ of $X$ belonging to $X_{0}$, where ${\rm MaxADSet}(x)$ is a unique maximal anti-discrete subset of $X$ containing $x$} (see [7] for the precise definition of the set ${\rm MaxADSet}(x)$). The retraction $r$ from the last theorem is defined uniquely, and it is denoted in the text by Stone-retraction". It has the following two remarkable properties: $r$ is open, i.e., sends open sets in $X$ to open sets in $X_{0}$, and $r$ is closed, i.e., sends closed sets in $X$ to closed sets in $X_{0}$.\par These results may be obtained by the methods described by R.H. Warren in [16].

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

#### MML Identifier: TSP_2

The terminology and notation used in this paper have been introduced in the following articles [13] [4] [15] [17] [2] [3] [10] [18] [14] [6] [7] [8]

#### Contents (PDF format)

1. Maximal $T_{0}$-Subsets
2. Maximal Kolmogorov Subspaces
3. Stone Retraction Mapping Theorems

#### Bibliography

[1] P. Alexandroff and H. H. Hopf. \em Topologie I. Springer-Verlag, Berlin, 1935.
[2] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[3] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
[4] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
[5] Ryszard Engelking. \em General Topology, volume 60 of \em Monografie Matematyczne. PWN - Polish Scientific Publishers, Warsaw, 1977.
[6] Zbigniew Karno. Maximal discrete subspaces of almost discrete topological spaces. Journal of Formalized Mathematics, 5, 1993.
[7] Zbigniew Karno. Maximal anti-discrete subspaces of topological spaces. Journal of Formalized Mathematics, 6, 1994.
[8] Zbigniew Karno. On Kolmogorov topological spaces. Journal of Formalized Mathematics, 6, 1994.
[9] Kazimierz Kuratowski. \em Topology, volume I. PWN - Polish Scientific Publishers, Academic Press, Warsaw, New York and London, 1966.
[10] Beata Padlewska and Agata Darmochwal. Topological spaces and continuous functions. Journal of Formalized Mathematics, 1, 1989.
[11] M. H. Stone. Application of Boolean algebras to topology. \em Math. Sb., 1:765--771, 1936.
[12] W.J. Thron. \em Topological Structures. Holt, Rinehart and Winston, New York, 1966.
[13] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[14] Andrzej Trybulec. A Borsuk theorem on homotopy types. Journal of Formalized Mathematics, 3, 1991.
[15] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[16] R.H. Warren. Identification spaces and unique uniformity. \em Pacific Journal of Mathematics, 95:483--492, 1981.
[17] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[18] Miroslaw Wysocki and Agata Darmochwal. Subsets of topological spaces. Journal of Formalized Mathematics, 1, 1989.