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]
-
Properties of the Closure and the Interior Operations
-
Anti-Discrete Subsets of Topological Structures
-
Maximal Anti-Discrete Subsets of Topological Structures
-
Anti-Discrete and Maximal Anti-discrete Subsets of Topological Spaces
-
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.
Received July 26, 1994
[
Download a postscript version,
MML identifier index,
Mizar home page]