Maximal Discrete Subspaces of Almost Discrete Topological Spaces

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)

Proper Subsets of 1-sorted Structures
Proper Subspaces of Topological Spaces
Maximal Discrete Subsets and Subspaces
Maximal Discrete Subspaces of Almost Discrete Spaces
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}.