Volume 4, 1992

University of Bialystok

Copyright (c) 1992 Association of Mizar Users

**Zbigniew Karno**- Warsaw University, Bialystok

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

- 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

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

[ Download a postscript version, MML identifier index, Mizar home page]