Journal of Formalized Mathematics
Volume 9, 1997
University of Bialystok
Copyright (c) 1997
Association of Mizar Users
Some Properties of Real Maps
-
Adam Grabowski
-
University of Bialystok
-
This paper was written while the author visited the Shinshu
University in the winter of 1997.
-
Yatsuka Nakamura
-
Shinshu University, Nagano
Summary.
-
The main goal of the paper is to show logical equivalence
of the two definitions of the {\em open subset}: one from
[3] and the other from [21].
This has been used to show that the other two definitions
are equivalent: the continuity of the map as in
[19] and in [20]. We used
this to show that continuous and one-to-one maps are
monotone (see theorems 16 and 17 for details).
The terminology and notation used in this paper have been
introduced in the following articles
[22]
[24]
[1]
[23]
[14]
[25]
[26]
[5]
[6]
[20]
[11]
[4]
[21]
[7]
[17]
[15]
[18]
[12]
[19]
[9]
[8]
[10]
[16]
[3]
[2]
[13]
-
Preliminaries
-
Equivalence of analytical and topological definitions of continuity
-
On the monotonicity of continuous maps
Bibliography
- [1]
Grzegorz Bancerek.
The ordinal numbers.
Journal of Formalized Mathematics,
1, 1989.
- [2]
Jozef Bialas and Yatsuka Nakamura.
The theorem of Weierstrass.
Journal of Formalized Mathematics,
7, 1995.
- [3]
Leszek Borys.
Paracompact and metrizable spaces.
Journal of Formalized Mathematics,
3, 1991.
- [4]
Czeslaw Bylinski.
Binary operations.
Journal of Formalized Mathematics,
1, 1989.
- [5]
Czeslaw Bylinski.
Functions and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
- [6]
Czeslaw Bylinski.
Functions from a set to a set.
Journal of Formalized Mathematics,
1, 1989.
- [7]
Czeslaw Bylinski.
Partial functions.
Journal of Formalized Mathematics,
1, 1989.
- [8]
Agata Darmochwal.
Compact spaces.
Journal of Formalized Mathematics,
1, 1989.
- [9]
Agata Darmochwal.
Families of subsets, subspaces and mappings in topological spaces.
Journal of Formalized Mathematics,
1, 1989.
- [10]
Agata Darmochwal.
The Euclidean space.
Journal of Formalized Mathematics,
3, 1991.
- [11]
Agata Darmochwal and Yatsuka Nakamura.
Metric spaces as topological spaces --- fundamental concepts.
Journal of Formalized Mathematics,
3, 1991.
- [12]
Agata Darmochwal and Yatsuka Nakamura.
The topological space $\calE^2_\rmT$. Arcs, line segments and special polygonal arcs.
Journal of Formalized Mathematics,
3, 1991.
- [13]
Adam Grabowski.
Introduction to the homotopy theory.
Journal of Formalized Mathematics,
9, 1997.
- [14]
Krzysztof Hryniewiecki.
Basic properties of real numbers.
Journal of Formalized Mathematics,
1, 1989.
- [15]
Stanislawa Kanas, Adam Lecko, and Mariusz Startek.
Metric spaces.
Journal of Formalized Mathematics,
2, 1990.
- [16]
Zbigniew Karno.
Continuity of mappings over the union of subspaces.
Journal of Formalized Mathematics,
4, 1992.
- [17]
Jaroslaw Kotowicz.
Convergent real sequences. Upper and lower bound of sets of real numbers.
Journal of Formalized Mathematics,
1, 1989.
- [18]
Beata Padlewska.
Locally connected spaces.
Journal of Formalized Mathematics,
2, 1990.
- [19]
Beata Padlewska and Agata Darmochwal.
Topological spaces and continuous functions.
Journal of Formalized Mathematics,
1, 1989.
- [20]
Konrad Raczkowski and Pawel Sadowski.
Real function continuity.
Journal of Formalized Mathematics,
2, 1990.
- [21]
Konrad Raczkowski and Pawel Sadowski.
Topological properties of subsets in real numbers.
Journal of Formalized Mathematics,
2, 1990.
- [22]
Andrzej Trybulec.
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Axiomatics, 1989.
- [23]
Andrzej Trybulec.
Subsets of real numbers.
Journal of Formalized Mathematics,
Addenda, 2003.
- [24]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
- [25]
Edmund Woronowicz.
Relations and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
- [26]
Edmund Woronowicz.
Relations defined on sets.
Journal of Formalized Mathematics,
1, 1989.
Received September 10, 1997
[
Download a postscript version,
MML identifier index,
Mizar home page]