Separated and Weakly Separated Subspaces of Topological Spaces

Zbigniew Karno

Warsaw University, Bialystok

Summary.

A new concept of weakly separated subsets and subspaces of topological spaces is described in Mizar formalizm. Based on [1], in comparison with the notion of separated subsets (subspaces), some properties of such subsets (subspaces) are discussed. Some necessary facts concerning closed subspaces, open subspaces and the union and the meet of two subspaces are also introduced. To present the main theorems we first formulate basic definitions. Let $X$ be a topological space. Two subsets $A_1$ and $A_2$ of $X$ are called {\em weakly separated} if $A_1 \setminus A_2$ and $A_2 \setminus A_1$ are separated. Two subspaces $X_{1}$ and $X_{2}$ of $X$ are called {\em weakly separated} if their carriers are weakly separated. The following theorem contains a useful characterization of weakly separated subsets in the special case when $A_{1} \cup A_{2}$ is equal to the carrier of $X$. {\em $A_{1}$ and $A_{2}$ are weakly separated iff there are such subsets of $X$, $C_{1}$ and $C_{2}$ closed (open) and $C$ open (closed, respectively), that $A_{1} \cup A_{2} = C_{1} \cup C_{2} \cup C$, $C_{1} \subset A_{1}$, $C_{2} \subset A_{2}$ and $C \subset A_{1} \cap A_{2}$}. Next theorem divided into two parts contains similar characterization of weakly separated subspaces in the special case when the union of $X_1$ and $X_2$ is equal to $X$. {\em If $X_{1}$ meets $X_{2}$, then $X_1$ and $X_2$ are weakly separated iff either $X_{1}$ is a subspace of $X_2$ or $X_2$ is a subspace of $X_{1}$ or there are such open (closed) subspaces $Y_1$ and $Y_2$ of $X$ that $Y_1$ is a subspace of $X_1$ and $Y_2$ is a subspace of $X_2$ and either $X$ is equal to the union of $Y_1$ and $Y_2$ or there is a(n) closed (open, respectively) subspace $Y$ of $X$ being a subspace of the meet of $X_1$ and $X_2$ and with the property that $X$ is the union of all $Y_1$, $Y_2$ and $Y$}. {\em If $X_1$ misses $X_{2}$, then $X_1$ and $X_2$ are weakly separated iff $X_1$ and $X_2$ are open (closed) subspaces of $X$}. Moreover, the following simple characterization of separated subspaces by means of weakly separated ones is obtained. {\em $X_1$ and $X_2$ are separated iff there are weakly separated subspaces $Y_1$ and $Y_2$ of $X$ such that $X_1$ is a subspace of $Y_1$, $X_2$ is a subspace of $Y_2$ and either $Y_1$ misses $Y_2$ or the meet of $Y_1$ and $Y_2$ misses the union of $X_1$ and $X_2$}.

MML Identifier: TSEP_1

Contents (PDF format)

1. Some properties of subspaces of topological spaces
2. Operations on subspaces of topological spaces
3. Separated and weakly separated subsets of topological spaces
4. Separated and weakly separated subspaces of topological spaces

Acknowledgments

Bibliography

[1] Kazimierz Kuratowski. \em Topology, volume I. PWN - Polish Scientific Publishers, Academic Press, Warsaw, New York and London, 1966.

[2] Beata Padlewska. Connected spaces. Journal of Formalized Mathematics, 1, 1989.

[3] Beata Padlewska and Agata Darmochwal. Topological spaces and continuous functions. Journal of Formalized Mathematics, 1, 1989.

[4] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.

[5] Andrzej Trybulec. A Borsuk theorem on homotopy types. Journal of Formalized Mathematics, 3, 1991.

[6] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.