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

- Maximal $T_{0}$-Subsets
- Maximal Kolmogorov Subspaces
- Stone Retraction Mapping Theorems

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

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