Rotating and Reversing

Andrzej Trybulec

University of Bialystok

Summary.

Quite a number of lemmas for the Jordan curve theorem, as yet in the case of the special polygonal curves, have been proved. By ``special" we mean, that it is a polygonal curve with edges parallel to axes and actually the lemmas have been proved, mostly, for the triangulations i.e. for finite sequences that define the curve. Moreover some of the results deal only with a special case: \begin{itemize} \item[-] finite sequences are clockwise oriented, \item[-] the first member of the sequence is the member with the lowest ordinate among those with the highest abscissa (N-min $f,$ where $f$ is a finite sequence, in the Mizar jargon). \end{itemize} In the change of the orientation one has to reverse the sequence (the operation introduced in [6]) and to change the second restriction one has to rotate the sequence (the operation introduced in [19]). The goal of the paper is to prove, mostly simple, facts about the relationship between properties and attributes of the finite sequence and its rotation (similar results about reversing had been proved in [6]). Some of them deal with recounting parameters, others with properties that are invariant under the rotation. We prove also that the finite sequence is either clockwise oriented or it is such after reversing. Everything is proved for the so called standard finite sequences, which means that if a point belongs to it then every point with the same abscissa or with the same ordinate, that belongs to the polygon, belongs also to the finite sequence. It does not seem that this requirement causes serious technical obstacles.

MML Identifier: REVROT_1

Contents (PDF format)

1. Preliminaries
2. About the Rotation
3. Rotating Circular Ones
4. Finite Sequence on the Plane
5. Rotating Finite Sequence on the Plane
6. Rotating Circular Ones (on the Plane)
7. The Orientation

Bibliography

[1] Grzegorz Bancerek. Cardinal numbers. Journal of Formalized Mathematics, 1, 1989.

[2] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.

[3] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Journal of Formalized Mathematics, 1, 1989.

[4] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[5] Czeslaw Bylinski. Finite sequences and tuples of elements of a non-empty sets. Journal of Formalized Mathematics, 2, 1990.

[6] Czeslaw Bylinski. Some properties of restrictions of finite sequences. Journal of Formalized Mathematics, 7, 1995.

[7] Agata Darmochwal. The Euclidean space. Journal of Formalized Mathematics, 3, 1991.

[8] Agata Darmochwal and Yatsuka Nakamura. The topological space $\calE^2_\rmT$. Arcs, line segments and special polygonal arcs. Journal of Formalized Mathematics, 3, 1991.

[9] Katarzyna Jankowska. Matrices. Abelian group of matrices. Journal of Formalized Mathematics, 3, 1991.

[10] Jaroslaw Kotowicz. Functions and finite sequences of real numbers. Journal of Formalized Mathematics, 5, 1993.

[11] Jaroslaw Kotowicz and Yatsuka Nakamura. Introduction to Go-Board --- part I. Journal of Formalized Mathematics, 4, 1992.

[12] Jaroslaw Kotowicz and Yatsuka Nakamura. Introduction to Go-Board --- part II. Journal of Formalized Mathematics, 4, 1992.

[13] Yatsuka Nakamura and Andrzej Trybulec. Decomposing a Go-Board into cells. Journal of Formalized Mathematics, 7, 1995.

[14] Yatsuka Nakamura, Andrzej Trybulec, and Czeslaw Bylinski. Bounded domains and unbounded domains. Journal of Formalized Mathematics, 11, 1999.

[15] Takaya Nishiyama and Yasuho Mizuhara. Binary arithmetics. Journal of Formalized Mathematics, 5, 1993.

[16] Beata Padlewska and Agata Darmochwal. Topological spaces and continuous functions. Journal of Formalized Mathematics, 1, 1989.

[17] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.

[18] Andrzej Trybulec. Left and right component of the complement of a special closed curve. Journal of Formalized Mathematics, 7, 1995.

[19] Andrzej Trybulec. On the decomposition of finite sequences. Journal of Formalized Mathematics, 7, 1995.

[20] Andrzej Trybulec and Yatsuka Nakamura. On the order on a special polygon. Journal of Formalized Mathematics, 9, 1997.

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