Volume 5, 1993

University of Bialystok

Copyright (c) 1993 Association of Mizar Users

**Zbigniew Karno**- Warsaw University, Bialystok

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

- Properties of Subsets of a Topological Space with Modified Topology
- Trivial Topological Spaces
- Examples of Discrete and Anti-discrete Topological Spaces
- An Example of a Topological Space
- Discrete and Almost Discrete Spaces

- [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]
Zbigniew Karno.
Continuity of mappings over the union of subspaces.
*Journal of Formalized Mathematics*, 4, 1992. - [4]
Zbigniew Karno.
The lattice of domains of an extremally disconnected space.
*Journal of Formalized Mathematics*, 4, 1992. - [5]
Zbigniew Karno.
Remarks on special subsets of topological spaces.
*Journal of Formalized Mathematics*, 5, 1993. - [6] Kazimierz Kuratowski. \em Topology, volume I. PWN - Polish Scientific Publishers, Academic Press, Warsaw, New York and London, 1966.
- [7] Kazimierz Kuratowski. \em Topology, volume II. PWN - Polish Scientific Publishers, Academic Press, Warsaw, New York and London, 1968.
- [8]
Beata Padlewska.
Families of sets.
*Journal of Formalized Mathematics*, 1, 1989. - [9]
Beata Padlewska and Agata Darmochwal.
Topological spaces and continuous functions.
*Journal of Formalized Mathematics*, 1, 1989. - [10]
Andrzej Trybulec.
Tarski Grothendieck set theory.
*Journal of Formalized Mathematics*, Axiomatics, 1989. - [11]
Zinaida Trybulec.
Properties of subsets.
*Journal of Formalized Mathematics*, 1, 1989. - [12]
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]