Formalized Mathematics    (ISSN 1426-2630)
Volume 6, Number 4 (1997): pdf, ps, dvi.
  1. Adam Grabowski. Introduction to the Homotopy Theory, Formalized Mathematics 6(4), pages 449-454, 1997. MML Identifier: BORSUK_2
    Summary: The paper introduces some preliminary notions concerning the homotopy theory according to \cite{Greenberg}: paths and arcwise connected to topological spaces. The basic operations on paths (addition and reversing) are defined. In the last section the predicate: $P, Q$ {\em are homotopic} is defined. We also showed some properties of the product of two topological spaces needed to prove reflexivity and symmetry of the above predicate.
  2. Adam Grabowski, Yatsuka Nakamura. Some Properties of Real Maps, Formalized Mathematics 6(4), pages 455-459, 1997. MML Identifier: JORDAN5A
    Summary: The main goal of the paper is to show logical equivalence of the two definitions of the {\em open subset}: one from \cite{PCOMPS_1.ABS} and the other from \cite{RCOMP_1.ABS}. This has been used to show that the other two definitions are equivalent: the continuity of the map as in \cite{PRE_TOPC.ABS} and in \cite{FCONT_1.ABS}. We used this to show that continuous and one-to-one maps are monotone (see theorems 16 and 17 for details).
  3. Adam Grabowski, Yatsuka Nakamura. The Ordering of Points on a Curve. Part I, Formalized Mathematics 6(4), pages 461-465, 1997. MML Identifier: JORDAN5B
    Summary: Some auxiliary theorems needed to formalize the proof of the Jordan Curve Theorem according to \cite{TAKE-NAKA} are proved.
  4. Adam Grabowski, Yatsuka Nakamura. The Ordering of Points on a Curve. Part II, Formalized Mathematics 6(4), pages 467-473, 1997. MML Identifier: JORDAN5C
    Summary: The proof of the Jordan Curve Theorem according to \cite{TAKE-NAKA} is continued. The notions of the first and last point of a oriented arc are introduced as well as ordering of points on a curve in $\calE^2_T$.
  5. Artur Kornilowicz. On the Categories Without Uniqueness of \bf cod and \bf dom . Some Properties of the Morphisms and the Functors, Formalized Mathematics 6(4), pages 475-481, 1997. MML Identifier: ALTCAT_4
    Summary:
  6. Noriko Asamoto. The loop and Times Macroinstruction for \SCMFSA, Formalized Mathematics 6(4), pages 483-497, 1997. MML Identifier: SCMFSA8C
    Summary: We implement two macroinstructions {\tt loop} and {\tt Times} which iterate macroinstructions of {\SCMFSA}. In a {\tt loop} macroinstruction it jumps to the head when the original macroinstruction stops, in a {\tt Times} macroinstruction it behaves as if the original macroinstruction repeats $n$ times.
  7. Robert Milewski. Algebraic and Arithmetic Lattices. Part II, Formalized Mathematics 6(4), pages 499-503, 1997. MML Identifier: WAYBEL15
    Summary: The article is a translation of \cite[pp. 89--92]{CCL}.
  8. Roman Matuszewski, Yatsuka Nakamura. Projections in n-Dimensional Euclidean Space to Each Coordinates, Formalized Mathematics 6(4), pages 505-509, 1997. MML Identifier: JORDAN2B
    Summary: In the $n$-dimensional Euclidean space ${\cal E}^n_{\rm T}$, a projection operator to each coordinate is defined. It is proven that such an operator is linear. Moreover, it is continuous as a mapping from ${\cal E}^n_{\rm T}$ to ${R}^{1}$, the carrier of which is a set of all reals. If $n$ is 1, the projection becomes a homeomorphism, which means that ${\cal E}^1_{\rm T}$ is homeomorphic to ${R}^{1}$.
  9. Yatsuka Nakamura, Andrzej Trybulec. Intermediate Value Theorem and Thickness of Simple Closed Curves, Formalized Mathematics 6(4), pages 511-514, 1997. MML Identifier: TOPREAL5
    Summary: Various types of the intermediate value theorem (\cite {shilov}) are proved. For their special cases, the Bolzano theorem is also proved. Using such a theorem, it is shown that if a curve is a simple closed curve, then it is not horizontally degenerated, neither is it vertically degenerated.
  10. Jaroslaw Gryko. The J\'onson's Theorem, Formalized Mathematics 6(4), pages 515-524, 1997. MML Identifier: LATTICE5
    Summary:
  11. Yatsuka Nakamura, Andrzej Trybulec. Lebesgue's Covering Lemma, Uniform Continuity and Segmentation of Arcs, Formalized Mathematics 6(4), pages 525-529, 1997. MML Identifier: UNIFORM1
    Summary: For mappings from a metric space to a metric space, a notion of uniform continuity is defined. If we introduce natural topologies to the metric spaces, a uniformly continuous function becomes continuous. On the other hand, if the domain is compact, a continuous function is uniformly continuous. For this proof, Lebesgue's covering lemma is also proved. An arc, which is homeomorphic to [0,1], can be divided into small segments, as small as one wishes.
  12. Andrzej Trybulec, Yatsuka Nakamura. On the Rectangular Finite Sequences of the Points of the Plane, Formalized Mathematics 6(4), pages 531-539, 1997. MML Identifier: SPRECT_1
    Summary: The article deals with a rather technical concept -- rectangular sequences of the points of the plane. We mean by that a finite sequence consisting of five elements, that is circular, i.e. the first element and the fifth one of it are equal, and such that the polygon determined by it is a non degenerated rectangle, with sides parallel to axes. The main result is that for the rectangle determined by such a sequence the left and the right component of the complement of it are different and disjoint.
  13. Andrzej Trybulec, Yatsuka Nakamura. On the Order on a Special Polygon, Formalized Mathematics 6(4), pages 541-548, 1997. MML Identifier: SPRECT_2
    Summary: The goal of the article is to determine the order of the special points defined in \cite{PSCOMP_1.ABS} on a special polygon. We restrict ourselves to the clockwise oriented finite sequences (the concept defined in this article) that start in N-min C (C being a compact non empty subset of the plane).
  14. Yoshinori Fujisawa, Yasushi Fuwa. The Euler's Function, Formalized Mathematics 6(4), pages 549-551, 1997. MML Identifier: EULER_1
    Summary: This article is concerned with the Euler's function \cite{takagi} that plays an important role in cryptograms. In the first section, we present some selected theorems on integers. Next, we define the Euler's function. Finally, three theorems relating to the Euler's function are proved. The third theorem concerns two relatively prime integers which make up the Euler's function parameter. In the public key cryptography these two integer values are used as public and secret keys.
  15. Jing-Chao Chen. While Macro Instructions of \SCMFSA, Formalized Mathematics 6(4), pages 553-561, 1997. MML Identifier: SCMFSA_9
    Summary: The article defines {\em while macro instructions} based on \SCMFSA. Some theorems about the generalized halting problems of {\em while macro instructions} are proved.
  16. Yatsuka Nakamura, Andrzej Trybulec. A Decomposition of a Simple Closed Curves and the Order of Their Points, Formalized Mathematics 6(4), pages 563-572, 1997. MML Identifier: JORDAN6
    Summary: The goal of the article is to introduce an order on a simple closed curve. To do this, we fix two points on the curve and devide it into two arcs. We prove that such a decomposition is unique. Other auxiliary theorems about arcs are proven for preparation of the proof of the above.
  17. Andrzej Kondracki. The Chinese Remainder Theorem, Formalized Mathematics 6(4), pages 573-577, 1997. MML Identifier: WSIERP_1
    Summary: The article is a translation of the first chapters of a book {\em Wst{\Ple}p do teorii liczb} (Eng. {\em Introduction to Number Theory}) by W. Sierpi\'nski, WSiP, Biblioteczka Matematyczna, Warszawa, 1987. The first few pages of this book have already been formalized in MML. We prove the Chinese Remainder Theorem and Thue's Theorem as well as several useful number theory propositions.