Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992 Association of Mizar Users

Separated and Weakly Separated Subspaces of Topological Spaces

Zbigniew Karno
Warsaw University, Bialystok


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

The terminology and notation used in this paper have been introduced in the following articles [4] [6] [3] [2] [5]

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


I would like to express my gratitude to Professors A. Trybulec and C. Byli\'nski for their valuable advice. I am also extremely grateful to W.A. Trybulec and to all participants of the Mizar Summer School (1991) for acquainting me with the Mizar system.


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

Received January 8, 1992

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