Journal of Formalized Mathematics
Volume 5, 1993
University of Bialystok
Copyright (c) 1993 Association of Mizar Users

## Maximal Discrete Subspaces of Almost Discrete Topological Spaces

Zbigniew Karno
Warsaw University, Bialystok

### Summary.

Let $X$ be a topological space and let $D$ be a subset of $X$. $D$ is said to be {\em discrete}\/ provided for every subset $A$ of $X$ such that $A \subseteq D$ there is an open subset $G$ of $X$ such that $A = D \cap G$\/ (comp. e.g., [9]). A discrete subset $M$ of $X$ is said to be {\em maximal discrete}\/ provided for every discrete subset $D$ of $X$ if $M \subseteq D$ then $M = D$. A subspace of $X$ is {\em discrete}\/ ({\em maximal discrete}) iff its carrier is discrete (maximal discrete) in $X$.\par Our purpose is to list a number of properties of discrete and maximal discrete sets in Mizar formalism. In particular, we show here that {\em if $D$ is dense and discrete then $D$ is maximal discrete}; moreover, {\em if $D$ is open and maximal discrete then $D$ is dense}. We discuss also the problem of the existence of maximal discrete subsets in a topological space.\par To present the main results we first recall a definition of a class of topological spaces considered herein. A topological space $X$ is called {\em almost discrete}\/ if every open subset of $X$ is closed; equivalently, if every closed subset of $X$ is open. Such spaces were investigated in Mizar formalism in [6] and [7]. We show here that {\em every almost discrete space contains a maximal discrete subspace and every such subspace is a retract of the enveloping space}. Moreover, {\em if $X_{0}$ is a maximal discrete subspace of an almost discrete space $X$ and $r : X \rightarrow X_{0}$ is a continuous retraction, then $r^{-1}(x) = \overline{\{x\}}$ for every point $x$ of $X$ belonging to $X_{0}$}. This fact is a specialization, in the case of almost discrete spaces, of the theorem of M.H. Stone that every topological space can be made into a $T_{0}$-space by suitable identification of points (see [11]).

#### MML Identifier: TEX_2

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

#### Contents (PDF format)

1. Proper Subsets of 1-sorted Structures
2. Proper Subspaces of Topological Spaces
3. Maximal Discrete Subsets and Subspaces
4. Maximal Discrete Subspaces of Almost Discrete Spaces
5. Continuous Mappings and Almost Discrete Spaces

#### Acknowledgments

The author wishes to thank Professor A. Trybulec for many helpful conversations during the preparation of this paper. The author is also grateful to G.~Bancerek for the definition of the clustered attribute {\em proper}.

#### Bibliography

[1] Jozef Bialas. Group and field definitions. Journal of Formalized Mathematics, 1, 1989.
[2] Leszek Borys. Paracompact and metrizable spaces. Journal of Formalized Mathematics, 3, 1991.
[3] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[4] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
[5] Czeslaw Bylinski. Partial functions. Journal of Formalized Mathematics, 1, 1989.
[6] Zbigniew Karno. The lattice of domains of an extremally disconnected space. Journal of Formalized Mathematics, 4, 1992.
[7] Zbigniew Karno. On discrete and almost discrete topological spaces. Journal of Formalized Mathematics, 5, 1993.
[8] Zbigniew Karno. Remarks on special subsets of topological spaces. Journal of Formalized Mathematics, 5, 1993.
[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] Andrzej Trybulec. Domains and their Cartesian products. Journal of Formalized Mathematics, 1, 1989.
[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] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[17] Miroslaw Wysocki and Agata Darmochwal. Subsets of topological spaces. Journal of Formalized Mathematics, 1, 1989.