Formalized Mathematics    (ISSN 1426-2630)
Volume 10, Number 3 (2002): pdf, ps, dvi.
  1. Grzegorz Bancerek, Adam Naumowicz. Preliminaries to Automatic Generation of Mizar Documentation for Circuits, Formalized Mathematics 10(3), pages 117-133, 2002. MML Identifier: CIRCCMB3
    Summary: In this paper we introduce technical notions used by a system which automatically generates Mizar documentation for specified circuits. They provide a ready for use elements needed to justify correctness of circuits' construction. We concentrate on the concept of stabilization and analyze one-gate circuits and their combinations.
  2. Robert Milewski. Properties of the Upper and Lower Sequence on the Cage, Formalized Mathematics 10(3), pages 135-143, 2002. MML Identifier: JORDAN15
    Summary:
  3. Adam Grabowski. On the Decompositions of Intervals and Simple Closed Curves, Formalized Mathematics 10(3), pages 145-151, 2002. MML Identifier: BORSUK_4
    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.
  4. Andrzej Trybulec. On the Minimal Distance Between Sets in Euclidean Space, Formalized Mathematics 10(3), pages 153-158, 2002. MML Identifier: JORDAN1K
    Summary: The concept of the minimal distance between two sets in a Euclidean space is introduced and some useful lemmas are proved.
  5. Yatsuka Nakamura, Andrzej Trybulec. Sequences of Metric Spaces and an Abstract Intermediate Value Theorem, Formalized Mathematics 10(3), pages 159-161, 2002. MML Identifier: TOPMETR3
    Summary: Relations of convergence of real sequences and convergence of metric spaces are investigated. An abstract intermediate value theorem for two closed sets in the range is presented. At the end, it is proven that an arc connecting the west minimal point and the east maximal point in a simple closed curve must be identical to the upper arc or lower arc of the closed curve.
  6. Andrzej Trybulec, Yatsuka Nakamura. On the Decomposition of a Simple Closed Curve into Two Arcs, Formalized Mathematics 10(3), pages 163-167, 2002. MML Identifier: JORDAN16
    Summary: The purpose of the paper is to prove lemmas needed for the Jordan curve theorem. The main result is that the decomposition of a simple closed curve into two arcs with the ends $p_1, p_2$ is unique in the sense that every arc on the curve with the same ends must be equal to one of them.
  7. Artur Kornilowicz. The Ordering of Points on a Curve. Part III, Formalized Mathematics 10(3), pages 169-171, 2002. MML Identifier: JORDAN17
    Summary:
  8. Artur Kornilowicz. The Ordering of Points on a Curve. Part IV, Formalized Mathematics 10(3), pages 173-177, 2002. MML Identifier: JORDAN18
    Summary:
  9. Josef Urban. Order Sorted Algebras, Formalized Mathematics 10(3), pages 179-188, 2002. MML Identifier: OSALG_1
    Summary: Initial notions for order sorted algebras.
  10. Josef Urban. Subalgebras of an Order Sorted Algebra. Lattice of Subalgebras, Formalized Mathematics 10(3), pages 189-196, 2002. MML Identifier: OSALG_2
    Summary:
  11. Josef Urban. Homomorphisms of Order Sorted Algebras, Formalized Mathematics 10(3), pages 197-200, 2002. MML Identifier: OSALG_3
    Summary:
  12. Josef Urban. Order Sorted Quotient Algebra, Formalized Mathematics 10(3), pages 201-210, 2002. MML Identifier: OSALG_4
    Summary:
  13. Josef Urban. Free Order Sorted Universal Algebra, Formalized Mathematics 10(3), pages 211-225, 2002. MML Identifier: OSAFREE
    Summary: Free Order Sorted Universal Algebra --- the general construction for any locally directed signatures.