Journal of Formalized Mathematics
Volume 6, 1994
University of Bialystok
Copyright (c) 1994 Association of Mizar Users

Maximal Anti-Discrete Subspaces of Topological Spaces

Zbigniew Karno
Warsaw University, Bialystok

Summary.

Let $X$ be a topological space and let $A$ be a subset of $X$. $A$ is said to be {\em anti-discrete}\/ provided for every open subset $G$ of $X$ either $A \cap G = \emptyset$ or $A \subseteq G$; equivalently, for every closed subset $F$ of $X$ either $A \cap F = \emptyset$ or $A \subseteq F$. An anti-discrete subset $M$ of $X$ is said to be {\em maximal anti-discrete}\/ provided for every anti-discrete subset $A$ of $X$ if $M \subseteq A$ then $M = A$. A subspace of $X$ is {\em maximal anti-discrete}\/ iff its carrier is maximal anti-discrete in $X$. The purpose is to list a few properties of maximal anti-discrete sets and subspaces in Mizar formalism.\par It is shown that every $x \in X$ is contained in a unique maximal anti-discrete subset M$(x)$ of $X$, denoted in the text by MaxADSet($x$). Such subset can be defined by $${\rm M}(x) = \bigcap\ \{ S \subseteq X : x \in S,\ {\rm and}\ S \ {\rm is}\ {\rm open}\ {\rm or}\ {\rm closed}\ {\rm in}\ X\}.$$ It has the following remarkable properties: (1) $y \in {\rm M}(x)$ iff ${\rm M}(y) = {\rm M}(x)$, (2) either ${\rm M}(x) \cap {\rm M}(y) = \emptyset$ or ${\rm M}(x) = {\rm M}(y)$, (3) ${\rm M}(x) = {\rm M}(y)$ iff $\overline{\{x\}} = \overline{\{y\}}$, and (4) ${\rm M}(x) \cap {\rm M}(y) = \emptyset$ iff $\overline{\{x\}} \neq \overline{\{y\}}$. It follows from these properties that $\{{\rm M}(x) : x \in X\}$ is the $T_{0}$-partition of $X$ defined by M.H.~Stone in [8].\par Moreover, it is shown that the operation M defined on all subsets of $X$ by $${\rm M}(A) = \bigcup\ \{{\rm M}(x) : x \in A\},$$ denoted in the text by MaxADSet($A$), satisfies the Kuratowski closure axioms (see e.g., [5]), i.e., (1) ${\rm M}(A \cup B) = {\rm M}(A) \cup {\rm M}(B)$, (2) ${\rm M}(A) = {\rm M}({\rm M}(A))$, (3) $A \subseteq {\rm M}(A)$,and (4) ${\rm M}(\emptyset) = \emptyset$. Note that this operation commutes with the usual closure operation of $X$, and if $A$ is an open (or a closed) subset of $X$, then ${\rm M}(A) = A$.

MML Identifier: TEX_4

The terminology and notation used in this paper have been introduced in the following articles [9] [1] [11] [6] [7] [12] [10] [3] [2] [4]

Contents (PDF format)

1. Properties of the Closure and the Interior Operations
2. Anti-Discrete Subsets of Topological Structures
3. Maximal Anti-Discrete Subsets of Topological Structures
4. Anti-Discrete and Maximal Anti-discrete Subsets of Topological Spaces
5. Maximal Anti-Discrete Subspaces

Bibliography

[1] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
[2] Zbigniew Karno. The lattice of domains of an extremally disconnected space. Journal of Formalized Mathematics, 4, 1992.
[3] Zbigniew Karno. Separated and weakly separated subspaces of topological spaces. Journal of Formalized Mathematics, 4, 1992.
[4] Zbigniew Karno. Maximal discrete subspaces of almost discrete topological spaces. Journal of Formalized Mathematics, 5, 1993.
[5] Kazimierz Kuratowski. \em Topology, volume I. PWN - Polish Scientific Publishers, Academic Press, Warsaw, New York and London, 1966.
[6] Beata Padlewska. Families of sets. Journal of Formalized Mathematics, 1, 1989.
[7] Beata Padlewska and Agata Darmochwal. Topological spaces and continuous functions. Journal of Formalized Mathematics, 1, 1989.
[8] M. H. Stone. Application of Boolean algebras to topology. \em Math. Sb., 1:765--771, 1936.
[9] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[10] Andrzej Trybulec. A Borsuk theorem on homotopy types. Journal of Formalized Mathematics, 3, 1991.
[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.