Separated and Weakly Separated Subspaces of Topological Spaces
Zbigniew Karno · 1991
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 A1 and A2 of X are called weakly separated if A1 \A2 and A2 \A1 are separated. Two subspaces X1 and X2 of X are called weakly separated if their carriers are weakly separated. The following theorem contains a useful characterization of weakly separated subsets in the special case when A1 ∪ A2 is equal to the carrier of X. A1 and A2 are weakly separated iff there are such subsets of X, C1 and C2 closed (open) and C open (closed, respectively), that A1 ∪ A2 = C1 ∪ C2 ∪ C, C1 ⊂ A1, C2 ⊂ A2 and C ⊂ A1 ∩ A2. Next theorem divided into two parts contains similar characterization of weakly separated subspaces in the special case when the union of X1 and X2 is equal to X. If X1 meets X2, then X1 and X2 are weakly separated iff either X1 is a subspace of X2 or X2 is a subspace of X1 or there are such open (closed) subspaces Y1 and Y2 of X that Y1 is a subspace of X1 and Y2 is a subspace of X2 and either X is equal to the union of Y1 and Y2 or there is a(n) closed (open, respectively) subspace Y of X being a subspace of the meet of X1 and X2 and with the property that X is the union of all Y1, Y2 and Y . If X1 misses X2, then X1 and X2 are weakly separated iff X1 and X2 are open (closed) subspaces of X. Moreover, the following simple characterization of separated subspaces by means of weakly separated ones is obtained. X1 and X2 are separated iff there are weakly separated subspaces Y1 and Y2 of X such that X1 is a subspace of Y1, X2 is a subspace of Y2 and either Y1 misses Y2 or the meet of Y1 and Y2 misses the union of X1 and X2.