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

MML Identifier: TEX_2

The terminology and notation used in this paper have been introduced in the following articles              

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

 Jozef Bialas. Group and field definitions. Journal of Formalized Mathematics, 1, 1989.
 Leszek Borys. Paracompact and metrizable spaces. Journal of Formalized Mathematics, 3, 1991.
 Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
 Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
 Czeslaw Bylinski. Partial functions. Journal of Formalized Mathematics, 1, 1989.
 Zbigniew Karno. The lattice of domains of an extremally disconnected space. Journal of Formalized Mathematics, 4, 1992.
 Zbigniew Karno. On discrete and almost discrete topological spaces. Journal of Formalized Mathematics, 5, 1993.
 Zbigniew Karno. Remarks on special subsets of topological spaces. Journal of Formalized Mathematics, 5, 1993.
 Kazimierz Kuratowski. \em Topology, volume I. PWN - Polish Scientific Publishers, Academic Press, Warsaw, New York and London, 1966.
 Beata Padlewska and Agata Darmochwal. Topological spaces and continuous functions. Journal of Formalized Mathematics, 1, 1989.
 M. H. Stone. Application of Boolean algebras to topology. \em Math. Sb., 1:765--771, 1936.
 Andrzej Trybulec. Domains and their Cartesian products. Journal of Formalized Mathematics, 1, 1989.
 Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
 Andrzej Trybulec. A Borsuk theorem on homotopy types. Journal of Formalized Mathematics, 3, 1991.
 Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
 Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.
 Miroslaw Wysocki and Agata Darmochwal. Subsets of topological spaces. Journal of Formalized Mathematics, 1, 1989.

Received November 5, 1993