Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992
Association of Mizar Users
Continuity of Mappings over the Union of Subspaces
-
Zbigniew Karno
-
Warsaw University, Bialystok
Summary.
-
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.
MML Identifier:
TMAP_1
The terminology and notation used in this paper have been
introduced in the following articles
[11]
[4]
[13]
[15]
[1]
[3]
[2]
[5]
[10]
[9]
[12]
[8]
[6]
-
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
Acknowledgments
I would like to express my thanks to Professors
A.~Trybulec and Cz.~Byli\'nski for their active interest in the publication
of this article and for elucidating to me new advanced Mizar constructions.
Bibliography
- [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.
Received May 22, 1992
[
Download a postscript version,
MML identifier index,
Mizar home page]