On Discrete and Almost Discrete Topological Spaces

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

On Discrete and Almost Discrete Topological Spaces

Zbigniew Karno: Warsaw University, Bialystok

Summary.

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 (comp. [6],[7]). Almost discrete spaces were investigated in Mizar formalism in [4]. We present here a few properties of such spaces supplementary to those given in [4].\par Most interesting is the following characterization~: {\em A topological space $X$ is almost discrete iff every nonempty subset of $X$ is not nowhere dense}. Hence, {\em $X$ is non almost discrete iff there is an everywhere dense subset of $X$ different from the carrier of $X$}. We have an analogous characterization of discrete spaces~: {\em A topological space $X$ is discrete iff every nonempty subset of $X$ is not boundary}. Hence, {\em $X$ is non discrete iff there is a dense subset of $X$ different from the carrier of $X$}. It is well known that the class of all almost discrete spaces contains both the class of discrete spaces and the class of anti-discrete spaces (see e.g., [4]). Observations presented here show that the class of all almost discrete non discrete spaces is not contained in the class of anti-discrete spaces and the class of all almost discrete non anti-discrete spaces is not contained in the class of discrete spaces. Moreover, the class of almost discrete non discrete non anti-discrete spaces is nonempty. To analyse these interdependencies we use various examples of topological spaces constructed here in Mizar formalism.