Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992
Association of Mizar Users
On a Duality Between Weakly Separated
Subspaces of Topological Spaces
-
Zbigniew Karno
-
Warsaw University, Bialystok
Summary.
-
Let $X$ be a topological space and let $X_{1}$ and
$X_{2}$ be subspaces of $X$ with the carriers $A_{1}$ and
$A_{2}$, respectively. Recall that $X_{1}$ and $X_{2}$
are {\em weakly separated}\/ if $A_{1} \setminus A_{2}$ and
$A_{2} \setminus A_{1}$ are separated (see [2]
and also [1] for applications).
Our purpose is to list a number of properties of such subspaces,
supplementary to those given in [2].
Note that in the Mizar formalism the carrier of any topological
space (hence the carrier of any its subspace) is always non-empty,
therefore for convenience we list beforehand analogous properties
of weakly separated subsets without any additional conditions.\par
To present the main results we first formulate a useful definition.
We say that $X_{1}$ and $X_{2}$ {\em constitute a decomposition}\/
of $X$ if $A_{1}$ and $A_{2}$ are disjoint and the union of $A_{1}$
and $A_{2}$ covers the carrier of $X$ (comp. [3]).
We are ready now to present the following duality property between pairs
of weakly separated subspaces~: {\em If each pair of subspaces
$X_{1}$, $Y_{1}$ and $X_{2}$, $Y_{2}$ of $X$ constitutes a decomposition
of $X$, then $X_{1}$ and $X_{2}$ are weakly separated iff $Y_{1}$ and
$Y_{2}$ are weakly separated}. From this theorem we get
immediately that under
the same hypothesis, {\em $X_{1}$ and $X_{2}$ are separated iff
$X_{1}$ misses $X_{2}$ and $Y_{1}$ and $Y_{2}$ are weakly separated}.
Moreover, we show the following enlargement theorem~: {\em If
$X_{i}$ and $Y_{i}$ are subspaces of $X$ such that $Y_{i}$ is a subspace
of $X_{i}$ and $Y_{1} \cup Y_{2} = X_{1} \cup X_{2}$
and if $Y_{1}$ and $Y_{2}$ are weakly separated, then $X_{1}$
and $X_{2}$ are weakly separated}.
We show also the following dual extenuation theorem~: {\em If
$X_{i}$ and $Y_{i}$ are subspaces of $X$ such that $Y_{i}$ is a subspace
of $X_{i}$ and $Y_{1} \cap Y_{2} = X_{1} \cap X_{2}$
and if $X_{1}$ and $X_{2}$ are weakly separated, then $Y_{1}$
and $Y_{2}$ are weakly separated}.
At the end we give a few properties of weakly separated
subspaces in subspaces.
MML Identifier:
TSEP_2
The terminology and notation used in this paper have been
introduced in the following articles
[5]
[7]
[4]
[8]
[6]
[2]
-
Certain Set--Decompositions of a Topological Space
-
Duality between Pairs of Weakly Separated Subsets
-
Certain Subspace--Decompositions of a Topological Space
-
Duality between Pairs of Weakly Separated Subspaces
Bibliography
- [1]
Zbigniew Karno.
Continuity of mappings over the union of subspaces.
Journal of Formalized Mathematics,
4, 1992.
- [2]
Zbigniew Karno.
Separated and weakly separated subspaces of topological spaces.
Journal of Formalized Mathematics,
4, 1992.
- [3]
Kazimierz Kuratowski.
\em Topology, volume I.
PWN - Polish Scientific Publishers, Academic Press, Warsaw, New York
and London, 1966.
- [4]
Beata Padlewska and Agata Darmochwal.
Topological spaces and continuous functions.
Journal of Formalized Mathematics,
1, 1989.
- [5]
Andrzej Trybulec.
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Axiomatics, 1989.
- [6]
Andrzej Trybulec.
A Borsuk theorem on homotopy types.
Journal of Formalized Mathematics,
3, 1991.
- [7]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
- [8]
Miroslaw Wysocki and Agata Darmochwal.
Subsets of topological spaces.
Journal of Formalized Mathematics,
1, 1989.
Received November 9, 1992
[
Download a postscript version,
MML identifier index,
Mizar home page]