Journal of Formalized Mathematics
Volume 10, 1998
University of Bialystok
Copyright (c) 1998 Association of Mizar Users

On the Dividing Function of the Simple Closed Curve into Segments


Yatsuka Nakamura
Shinshu University, Nagano

Summary.

At the beginning, the concept of the segment of the simple closed curve in 2-dimensional Euclidean space is defined. Some properties of segments are shown in the succeeding theorems. At the end, the existence of the function which can divide the simple closed curve into segments is shown. We can make the diameter of segments as small as we want.

MML Identifier: JORDAN7

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

Contents (PDF format)

  1. Definition of the Segment and Its Property
  2. A Function to Divide the Simple Closed Curve

Bibliography

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.
[2] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. 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 and Piotr Rudnicki. Bounding boxes for compact sets in $\calE^2$. Journal of Formalized Mathematics, 9, 1997.
[6] Agata Darmochwal. Compact spaces. 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. The Euclidean space. Journal of Formalized Mathematics, 3, 1991.
[9] Agata Darmochwal and Yatsuka Nakamura. Metric spaces as topological spaces --- fundamental concepts. Journal of Formalized Mathematics, 3, 1991.
[10] Agata Darmochwal and Yatsuka Nakamura. The topological space $\calE^2_\rmT$. Arcs, line segments and special polygonal arcs. Journal of Formalized Mathematics, 3, 1991.
[11] Agata Darmochwal and Yatsuka Nakamura. The topological space $\calE^2_\rmT$. Simple closed curves. Journal of Formalized Mathematics, 3, 1991.
[12] Alicia de la Cruz. Totally bounded metric spaces. Journal of Formalized Mathematics, 3, 1991.
[13] Adam Grabowski and Yatsuka Nakamura. The ordering of points on a curve. Part II. Journal of Formalized Mathematics, 9, 1997.
[14] Jaroslaw Kotowicz and Yatsuka Nakamura. Introduction to Go-Board --- part I. Journal of Formalized Mathematics, 4, 1992.
[15] Yatsuka Nakamura and Andrzej Trybulec. Adjacency concept for pairs of natural numbers. Journal of Formalized Mathematics, 8, 1996.
[16] Yatsuka Nakamura and Andrzej Trybulec. A decomposition of simple closed curves and the order of their points. Journal of Formalized Mathematics, 9, 1997.
[17] Takaya Nishiyama and Yasuho Mizuhara. Binary arithmetics. Journal of Formalized Mathematics, 5, 1993.
[18] Beata Padlewska and Agata Darmochwal. Topological spaces and continuous functions. Journal of Formalized Mathematics, 1, 1989.
[19] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[20] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.
[21] Wojciech A. Trybulec. Pigeon hole principle. Journal of Formalized Mathematics, 2, 1990.
[22] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[23] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.

Received June 16, 1998


[ Download a postscript version, MML identifier index, Mizar home page]