Journal of Formalized Mathematics
Volume 14, 2002
University of Bialystok
Copyright (c) 2002
Association of Mizar Users
On the Decompositions of Intervals
and Simple Closed Curves
-
Adam Grabowski
-
University of Bialystok
Summary.
-
The aim of the paper is to show that the only subcontinua
of the Jordan curve are arcs, the whole curve,
and singletons of its points. Additionally, it has been shown
that the only subcontinua of the unit interval $\Bbb I$
are closed intervals.
This work has been partially supported by the European Community
TYPES grant IST-1999-29001 and CALCULEMUS grant HPRN-CT-2000-00102.
The terminology and notation used in this paper have been
introduced in the following articles
[23]
[26]
[1]
[25]
[27]
[3]
[5]
[2]
[4]
[21]
[8]
[6]
[22]
[10]
[12]
[13]
[17]
[28]
[20]
[24]
[15]
[16]
[18]
[19]
[11]
[7]
[14]
[9]
-
Preliminaries
-
Decompositions of Intervals
-
Decompositions of Simple Closed Curves
Bibliography
- [1]
Grzegorz Bancerek.
The ordinal numbers.
Journal of Formalized Mathematics,
1, 1989.
- [2]
Jozef Bialas.
Group and field definitions.
Journal of Formalized Mathematics,
1, 1989.
- [3]
Czeslaw Bylinski.
Functions and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
- [4]
Czeslaw Bylinski.
Functions from a set to a set.
Journal of Formalized Mathematics,
1, 1989.
- [5]
Czeslaw Bylinski.
Partial functions.
Journal of Formalized Mathematics,
1, 1989.
- [6]
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.
- [7]
Czeslaw Bylinski and Piotr Rudnicki.
Bounding boxes for compact sets in $\calE^2$.
Journal of Formalized Mathematics,
9, 1997.
- [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]
Agata Darmochwal and Yatsuka Nakamura.
The topological space $\calE^2_\rmT$. Simple closed curves.
Journal of Formalized Mathematics,
3, 1991.
- [14]
Noboru Endou and Artur Kornilowicz.
The definition of the Riemann definite integral and some related lemmas.
Journal of Formalized Mathematics,
11, 1999.
- [15]
Adam Grabowski.
Properties of the product of compact topological spaces.
Journal of Formalized Mathematics,
11, 1999.
- [16]
Zbigniew Karno.
Separated and weakly separated subspaces of topological spaces.
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]
Yatsuka Nakamura.
Half open intervals in real numbers.
Journal of Formalized Mathematics,
14, 2002.
- [19]
Yatsuka Nakamura and Jaroslaw Kotowicz.
The Jordan's property for certain subsets of the plane.
Journal of Formalized Mathematics,
4, 1992.
- [20]
Beata Padlewska.
Connected spaces.
Journal of Formalized Mathematics,
1, 1989.
- [21]
Beata Padlewska and Agata Darmochwal.
Topological spaces and continuous functions.
Journal of Formalized Mathematics,
1, 1989.
- [22]
Konrad Raczkowski and Pawel Sadowski.
Topological properties of subsets in real numbers.
Journal of Formalized Mathematics,
2, 1990.
- [23]
Andrzej Trybulec.
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Axiomatics, 1989.
- [24]
Andrzej Trybulec.
A Borsuk theorem on homotopy types.
Journal of Formalized Mathematics,
3, 1991.
- [25]
Andrzej Trybulec.
Subsets of real numbers.
Journal of Formalized Mathematics,
Addenda, 2003.
- [26]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
- [27]
Edmund Woronowicz.
Relations and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
- [28]
Mariusz Zynel and Adam Guzowski.
\Tzero\ topological spaces.
Journal of Formalized Mathematics,
6, 1994.
Received August 7, 2002
[
Download a postscript version,
MML identifier index,
Mizar home page]