Journal of Formalized Mathematics
Volume 9, 1997
University of Bialystok
Copyright (c) 1997 Association of Mizar Users

## Some Properties of Real Maps

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

#### MML Identifier: JORDAN5A

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]

#### Contents (PDF format)

1. Preliminaries
2. Equivalence of analytical and topological definitions of continuity
3. 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.