Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992 Association of Mizar Users

## The Brouwer Fixed Point Theorem for Intervals

Toshihiko Watanabe
Shinshu University, Nagano

### Summary.

The aim is to prove, using Mizar System, the following simplest version of the Brouwer Fixed Point Theorem [3]. {\em For every continuous mapping $f : {\Bbb I} \rightarrow {\Bbb I}$ of the topological unit interval $\Bbb I$ there exists a point $x$ such that $f(x) = x$} (see e.g. [9], [4]).

This paper was done under the supervision of Z. Karno while the author was visiting the Institute of Mathematics of Warsaw University in Bia{\l}ystok.

#### MML Identifier: TREAL_1

The terminology and notation used in this paper have been introduced in the following articles [17] [20] [1] [19] [21] [5] [6] [10] [16] [15] [7] [14] [11] [13] [2] [8] [12] [18]

#### Contents (PDF format)

1. Properties of Topological Intervals
2. Continuous Mappings Between Topological Intervals
3. Connectedness of Intervals and Brouwer Fixed Point Theorem for Intervals

#### Acknowledgments

The author wishes to express his thanks to Professors A.~Trybulec and Z.~Karno for their useful suggestions and many valuable comments.

#### Bibliography

[1] Grzegorz Bancerek. The ordinal numbers. Journal of Formalized Mathematics, 1, 1989.
[2] Leszek Borys. Paracompact and metrizable spaces. Journal of Formalized Mathematics, 3, 1991.
[3] L. Brouwer. \"Uber Abbildungen von Mannigfaltigkeiten. \em Mathematische Annalen, 38(71):97--115, 1912.
[4] Robert H. Brown. \em The Lefschetz Fixed Point Theorem. Scott--Foresman, New York, 1971.
[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] Agata Darmochwal. Families of subsets, subspaces and mappings in topological spaces. Journal of Formalized Mathematics, 1, 1989.
[8] Agata Darmochwal and Yatsuka Nakamura. Metric spaces as topological spaces --- fundamental concepts. Journal of Formalized Mathematics, 3, 1991.
[9] James Dugundji and Andrzej Granas. \em Fixed Point Theory, volume I. PWN - Polish Scientific Publishers, Warsaw, 1982.
[10] Krzysztof Hryniewiecki. Basic properties of real numbers. Journal of Formalized Mathematics, 1, 1989.
[11] Stanislawa Kanas, Adam Lecko, and Mariusz Startek. Metric spaces. Journal of Formalized Mathematics, 2, 1990.
[12] Zbigniew Karno. Separated and weakly separated subspaces of topological spaces. Journal of Formalized Mathematics, 4, 1992.
[13] Michal Muzalewski. Categories of groups. Journal of Formalized Mathematics, 3, 1991.
[14] Beata Padlewska. Connected spaces. Journal of Formalized Mathematics, 1, 1989.
[15] Beata Padlewska and Agata Darmochwal. Topological spaces and continuous functions. Journal of Formalized Mathematics, 1, 1989.
[16] Konrad Raczkowski and Pawel Sadowski. Topological properties of subsets in real numbers. Journal of Formalized Mathematics, 2, 1990.
[17] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[18] Andrzej Trybulec. A Borsuk theorem on homotopy types. Journal of Formalized Mathematics, 3, 1991.
[19] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.
[20] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[21] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.