Formalized Mathematics    (ISSN 1898-9934 (Online), ISSN 1426-2630 (Print))
Volume 13, Number 2 (2005): pdf, ps, dvi.
  1. Yatsuka Nakamura, Andrzej Trybulec. The Fashoda Meet Theorem for Rectangles, Formalized Mathematics 13(2), pages 199-219, 2005. MML Identifier: JGRAPH_7
    Summary: Here, so called Fashoda Meet Theorem is proven in the case of rectangles. All cases of proper location of arcs are listed up, and it is shown that the theorem consists in each case. Such a list of cases will be useful when one wants to apply the theorem.
  2. Yuzhong Ding, Xiquan Liang. Preliminaries to Mathematical Morphology and Its Properties, Formalized Mathematics 13(2), pages 221-225, 2005. MML Identifier: MATHMORP
    Summary: In this paper we have discussed the basic mathematical morphological operators and their properties.
  3. Robert Milewski. Subsequences of Almost, Weakly and Poorly One-to-one Finite Sequences, Formalized Mathematics 13(2), pages 227-233, 2005. MML Identifier: JORDAN23
    Summary: {}
  4. Gilbert Lee, Piotr Rudnicki. Alternative Graph Structures, Formalized Mathematics 13(2), pages 235-252, 2005. MML Identifier: GLIB_000
    Summary: We define the notion of a graph anew without using the available Mizar structures. In our approach, we model graph structure as a finite function whose domain is a subset of natural numbers. The elements of the domain of the function play the role of selectors for accessing the components of the structure. As these selectors are first class objects, many future extensions of the new graph structure turned out to be easier to formalize in Mizar than with the traditional Mizar structures. \par After introducing graph structure, we define its selectors and then conditions that the structure needs to satisfy to form a directed graph (in the spirit of \cite{GRAPH_1.ABS}). For these graphs we define a collection of basic graph notions; the presentation of these notions is continued in articles \cite{GLIB_001.ABS,GLIB_002.ABS,GLIB_003.ABS}. \par We have tried to follow a number of graph theory books in choosing graph terminology but since the terminology is not commonly agreed upon, we had to make a number of compromises, see \cite{gl04}.
  5. Gilbert Lee. Walks in Graphs, Formalized Mathematics 13(2), pages 253-269, 2005. MML Identifier: GLIB_001
    Summary: We define walks for graphs introduced in \cite{GLIB_000.ABS}, introduce walk attributes and functors for walk creation and modification of walks. Subwalks of a walk are also defined.
  6. Gilbert Lee. Trees and Graph Components, Formalized Mathematics 13(2), pages 271-277, 2005. MML Identifier: GLIB_002
    Summary: In the graph framework of \cite{GLIB_000.ABS} we define connected and acyclic graphs, components of a graph, and define the notion of cut-vertex (articulation point).
  7. Gilbert Lee. Weighted and Labeled Graphs, Formalized Mathematics 13(2), pages 279-293, 2005. MML Identifier: GLIB_003
    Summary: In the graph framework of \cite{GLIB_000.ABS} we introduce new selectors: weights for edges and lables for both edges and vertices. We introduce also a number of tools for accessing and modifying these new fields.
  8. Gilbert Lee, Piotr Rudnicki. Correctness of Dijkstra's Shortest Path and Prim's Minimum Spanning Tree Algorithms, Formalized Mathematics 13(2), pages 295-304, 2005. MML Identifier: GLIB_004
    Summary: We prove correctness for Dijkstra's shortest path algorithm, and Prim's minimum weight spanning tree algorithm at the level of graph manipulations.
  9. Gilbert Lee. Correctnesss of Ford-Fulkerson's Maximum Flow Algorithm, Formalized Mathematics 13(2), pages 305-314, 2005. MML Identifier: GLIB_005
    Summary: We define and prove correctness of Ford/Fulkerson's Maximum Network-Flow algorithm at the level of graph manipulations.
  10. Artur Kornilowicz. Properties of Connected Subsets of the Real Line, Formalized Mathematics 13(2), pages 315-323, 2005. MML Identifier: RCOMP_3
    Summary: {}
  11. Artur Kornilowicz. The Fundamental Group of the Circle, Formalized Mathematics 13(2), pages 325-331, 2005. MML Identifier: TOPALG_5
    Summary: {}
  12. Artur Kornilowicz, Yasunari Shidama. Brouwer Fixed Point Theorem for Disks on the Plane, Formalized Mathematics 13(2), pages 333-336, 2005. MML Identifier: BROUWER
    Summary: {}
  13. Karol Pcak. Stirling Numbers of the Second Kind, Formalized Mathematics 13(2), pages 337-345, 2005. MML Identifier: STIRL2_1
    Summary: In this paper we define Stirling numbers of the second kind by cardinality of certain functional classes such that $$S(n,k) = \{f {\rm ~where~} f {\rm~is~function~of~}n,k : f {\rm ~is~onto~"increasing} \}$$ After that we show basic properties of this number in order to prove recursive dependence of Stirling number of the second kind. Next theorems are introduced to prove formula $$S(n,k) = \frac{1}{k!} \mathop\Sigma_{i=0}^{k-1}(-1)^i {{k}\choose{i}}(k-i)^n$$ where $k\leq n.$
  14. Bo Zhang, Hiroshi Yamazaki, Yatsuka Nakamura. Limit of Sequence of Subsets, Formalized Mathematics 13(2), pages 347-352, 2005. MML Identifier: SETLIM_1
    Summary: A concept of "limit of sequence of subsets" is defined here. This article contains the following items: 1. definition of the superior sequence and the inferior sequence of sets. 2. definition of the superior limit and the inferior limit of sets, and additional properties for the sigma-field of sets. and 3, definition of the limit value of a convergent sequence of sets, and additional properties for the sigma-field of sets.
  15. Magdalena Jastrzcebska, Adam Grabowski. The Properties of Supercondensed Sets, Subcondensed Sets and Condensed Sets, Formalized Mathematics 13(2), pages 353-359, 2005. MML Identifier: ISOMICHI
    Summary: We formalized article ``New concepts in the theory of topological space -- supercondensed set, subcondensed set, and condensed set'' by Yoshinori Isomichi. First we defined supercondensed, subcondensed, and condensed sets and then gradually, defining other attributes such as regular open set or regular closed set, we formalized all the theorems and remarks that one can find in Isomichi's article.