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]
-
Properties of Topological Intervals
-
Continuous Mappings Between Topological Intervals
-
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.
Received August 17, 1992
[
Download a postscript version,
MML identifier index,
Mizar home page]