Volume 4, 1992

University of Bialystok

Copyright (c) 1992 Association of Mizar Users

**Zbigniew Karno**- Warsaw University, Bialystok

- Let $X$ and $Y$ be topological spaces and let $X_{1}$ and $X_{2}$ be subspaces of $X$. Let $f : X_{1} \cup X_{2} \rightarrow Y$ be a mapping defined on the union of $X_{1}$ and $X_{2}$ such that the restriction mappings $f_{\mid X_{1}}$ and $f_{\mid X_{2}}$ are continuous. It is well known that if $X_{1}$ and $X_{2}$ are both open (closed) subspaces of $X$, then $f$ is continuous (see e.g. [7, p.106]). \par The aim is to show, using Mizar System, the following theorem (see Section 5): {\em If $X_{1}$ and $X_{2}$ are weakly separated, then $f$ is continuous} (compare also [14, p.358] for related results). This theorem generalizes the preceding one because if $X_{1}$ and $X_{2}$ are both open (closed), then these subspaces are weakly separated (see [6]). However, the following problem remains open. \begin{itemize} \item[ ] {\bf Problem 1.} Characterize the class of pairs of subspaces $X_{1}$ and $X_{2}$ of a topological space $X$ such that ($\ast$) for any topological space $Y$ and for any mapping $f : X_{1} \cup X_{2} \rightarrow Y$, $f$ is continuous if the restrictions $f_{\mid X_{1}}$ and $f_{\mid X_{2}}$ are continuous. \end{itemize} In some special case we have the following characterization: {\em $X_{1}$ and $X_{2}$ are separated iff $X_{1}$ misses $X_{2}$ and the condition} ($\ast$) {\em is fulfilled.} In connection with this fact we hope that the following specification of the preceding problem has an affirmative answer. \begin{itemize} \item[ ] {\bf Problem 2.} Suppose the condition ($\ast$) is fulfilled. Must $X_{1}$ and $X_{2}$ be weakly separated ? \end{itemize} Note that in the last section the concept of the union of two mappings is introduced and studied. In particular, all results presented above are reformulated using this notion. In the remaining sections we introduce concepts needed for the formulation and the proof of theorems on properties of continuous mappings, restriction mappings and modifications of the topology.

- Set-Theoretic Preliminaries
- Selected Properties of Subspaces of Topological Spaces
- Continuity of Mappings
- A Modification of the Topology of Topological Spaces
- Continuity of Mappings over the Union of Subspaces
- The Union of Continuous Mappings

- [1]
Czeslaw Bylinski.
Functions and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989. - [2]
Czeslaw Bylinski.
Functions from a set to a set.
*Journal of Formalized Mathematics*, 1, 1989. - [3]
Czeslaw Bylinski.
Partial functions.
*Journal of Formalized Mathematics*, 1, 1989. - [4]
Czeslaw Bylinski.
Some basic properties of sets.
*Journal of Formalized Mathematics*, 1, 1989. - [5]
Czeslaw Bylinski.
The modification of a function by a function and the iteration of the composition of a function.
*Journal of Formalized Mathematics*, 2, 1990. - [6]
Zbigniew Karno.
Separated and weakly separated subspaces of topological spaces.
*Journal of Formalized Mathematics*, 4, 1992. - [7] Kazimierz Kuratowski. \em Topology, volume I. PWN - Polish Scientific Publishers, Academic Press, Warsaw, New York and London, 1966.
- [8]
Michal Muzalewski.
Categories of groups.
*Journal of Formalized Mathematics*, 3, 1991. - [9]
Beata Padlewska.
Locally connected spaces.
*Journal of Formalized Mathematics*, 2, 1990. - [10]
Beata Padlewska and Agata Darmochwal.
Topological spaces and continuous functions.
*Journal of Formalized Mathematics*, 1, 1989. - [11]
Andrzej Trybulec.
Tarski Grothendieck set theory.
*Journal of Formalized Mathematics*, Axiomatics, 1989. - [12]
Andrzej Trybulec.
A Borsuk theorem on homotopy types.
*Journal of Formalized Mathematics*, 3, 1991. - [13]
Zinaida Trybulec.
Properties of subsets.
*Journal of Formalized Mathematics*, 1, 1989. - [14] Eduard \vCech. \em Topological Spaces. Academia, Publishing House of the Czechoslovak Academy of Sciences, Prague, 1966.
- [15]
Edmund Woronowicz.
Relations and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989.

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