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]

Contents (PDF format)

  1. Certain Set--Decompositions of a Topological Space
  2. Duality between Pairs of Weakly Separated Subsets
  3. Certain Subspace--Decompositions of a Topological Space
  4. 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]