Formalized Mathematics    (ISSN 1898-9934 (Online), ISSN 1426-2630 (Print))
Volume 12, Number 2 (2004): pdf, ps, dvi.
  1. Yasumasa Suzuki. Banach Space of Bounded Real Sequences, Formalized Mathematics 12(2), pages 77-83, 2004. MML Identifier: RSSPACE4
    Summary: We introduce the arithmetic addition and multiplication in the set of bounded real sequences and also introduce the norm. This set has the structure of the Banach space.
  2. Yuzhong Ding, Xiquan Liang. Solving Roots of Polynomial Equation of Degree 2 and 3 with Complex Coefficients, Formalized Mathematics 12(2), pages 85-92, 2004. MML Identifier: POLYEQ_3
    Summary: In the article, solving complex roots of polynomial equation of degree 2 and 3 with real coefficients and complex roots of polynomial equation of degree 2 and 3 with complex coefficients is discussed.
  3. Noboru Endou. Complex Linear Space and Complex Normed Space, Formalized Mathematics 12(2), pages 93-102, 2004. MML Identifier: CLVECT_1
    Summary: In this article, we introduce the notion of complex linear space and complex normed space.
  4. Yasunari Shidama. The Banach Algebra of Bounded Linear Operators, Formalized Mathematics 12(2), pages 103-108, 2004. MML Identifier: LOPBAN_2
    Summary: In this article, the basic properties of Banach algebra are described. This algebra is defined as the set of all bounded linear operators from one normed space to another.
  5. Noboru Endou. Complex Linear Space of Complex Sequences, Formalized Mathematics 12(2), pages 109-117, 2004. MML Identifier: CSSPACE
    Summary: In this article, we introduce a notion of complex linear space of complex sequence and complex unitary space.
  6. Yatsuka Nakamura. Behaviour of an Arc Crossing a Line, Formalized Mathematics 12(2), pages 119-124, 2004. MML Identifier: JORDAN20
    Summary: In 2-dimensional Euclidean space, we examine behaviour of an arc when it crosses a vertical line. There are 3 types when an arc enters into a line, which are: ``Left-In'', ``Right-In'' and ``Oscilating-In''. Also, there are 3 types when an arc goes out from a line, which are: ``Left-Out'', ``Right-Out'' and ``Oscilating-Out''. If an arc is a special polygonal arc, there are only 2 types for each case, entering in and going out. They are ``Left-In'' and ``Right-In'' for entering in, and ``Left-Out'' and ``Right-Out'' for going out.
  7. Masami Tanaka, Yatsuka Nakamura. Some Set Series in Finite Topological Spaces. Fundamental Concepts for Image Processing, Formalized Mathematics 12(2), pages 125-129, 2004. MML Identifier: FINTOPO3
    Summary: First we give a definition of ``inflation'' of a set in finite topological spaces. Then a concept of ``deflation'' of a set is also defined. In the remaining part, we give a concept of the ``set series'' for a subset of a finite topological space. Using this, we can define a series of neighbourhoods for each point in the space. The work is done according to \cite{Nakamura:2}.
  8. Yasunari Shidama. The Series on Banach Algebra, Formalized Mathematics 12(2), pages 131-138, 2004. MML Identifier: LOPBAN_3
    Summary: In this article, the basic properties of the series on Banach algebra are described. The Neumann series is introduced in the last section.
  9. Pacharapokin Chanapat, Kanchun,, Hiroshi Yamazaki. Formulas and Identities of Trigonometric Functions, Formalized Mathematics 12(2), pages 139-141, 2004. MML Identifier: SIN_COS4
    Summary: In this article, we concentrated especially on addition formulas of fundamental trigonometric functions, and their identities.
  10. Krzysztof Retel. The Class of Series-Parallel Graphs. Part III, Formalized Mathematics 12(2), pages 143-149, 2004. MML Identifier: NECKLA_3
    Summary: This paper contains some facts and theorems relating to the following operations on graphs: union, sum, complement and ``embeds''. We also introduce connected graphs to prove that a finite irreflexive symmetric N-free graph is a finite series-parallel graph. This article continues the formalization of \cite{Thomasse}.
  11. Artur Kornilowicz, Yasunari Shidama. Relocability for SCM over Ring, Formalized Mathematics 12(2), pages 151-157, 2004. MML Identifier: SCMRING4
    Summary:
  12. Noboru Endou. Convergent Sequences in Complex Unitary Space, Formalized Mathematics 12(2), pages 159-165, 2004. MML Identifier: CLVECT_2
    Summary: In this article, we introduce the notion of convergence sequence in complex unitary space and complex Hilbert space.
  13. Artur Kornilowicz. Recursive Definitions. Part II, Formalized Mathematics 12(2), pages 167-172, 2004. MML Identifier: RECDEF_2
    Summary:
  14. Yasunari Shidama. The Exponential Function on Banach Algebra, Formalized Mathematics 12(2), pages 173-177, 2004. MML Identifier: LOPBAN_4
    Summary: In this article, the basic properties of the exponential function on Banach algebra are described.
  15. Artur Kornilowicz, Piotr Rudnicki. Fundamental Theorem of Arithmetic, Formalized Mathematics 12(2), pages 179-186, 2004. MML Identifier: NAT_3
    Summary: We formalize the notion of the prime-power factorization of a natural number and prove the Fundamental Theorem of Arithmetic. We prove also how prime-power factorization can be used to compute: products, quotients, powers, greatest common divisors and least common multiples.
  16. Noboru Endou. Hilbert Space of Complex Sequences, Formalized Mathematics 12(2), pages 187-190, 2004. MML Identifier: CSSPACE2
    Summary: An extension of \cite{RSSPACE2.ABS}. As the example of complex norm spaces, we introduce the arithmetic addition and multiplication in the set of absolute summable complex sequences and also introduce the norm.
  17. Noboru Endou. Banach Space of Absolute Summable Complex Sequences, Formalized Mathematics 12(2), pages 191-194, 2004. MML Identifier: CSSPACE3
    Summary: An extension of \cite{RSSPACE3.ABS}. As the example of complex norm spaces, I introduced the arithmetic addition and multiplication in the set of absolute summable complex sequences and also introduced the norm.
  18. Yasunari Shidama. The Taylor Expansions, Formalized Mathematics 12(2), pages 195-200, 2004. MML Identifier: TAYLOR_1
    Summary: In this article, some classic theorems of calculus are described. The Taylor expansions and the logarithmic differentiation, etc. are included here.
  19. Noboru Endou. Complex Banach Space of Bounded Linear Operators, Formalized Mathematics 12(2), pages 201-209, 2004. MML Identifier: CLOPBAN1
    Summary: An extension of \cite{LOPBAN_1.ABS}. In this article, the basic properties of complex linear spaces which are defined by the set of all complex linear operators from one complex linear space to another are described. Finally, a complex Banach space is introduced. This is defined by the set of all bounded complex linear operators, like in \cite{LOPBAN_1.ABS}.
  20. Noboru Endou. Complex Banach Space of Bounded Complex Sequences, Formalized Mathematics 12(2), pages 211-218, 2004. MML Identifier: CSSPACE4
    Summary: An extension of \cite{RSSPACE4.ABS}. In this article, we introduce two complex Banach spaces. One of them is the space of bounded complex sequences. The other one is the space of complex bounded functions, which is defined by the set of all complex bounded functions.
  21. Hirofumi Fukura, Yatsuka Nakamura. Concatenation of Finite Sequences Reducing Overlapping Part and an Argument of Separators of Sequential Files, Formalized Mathematics 12(2), pages 219-224, 2004. MML Identifier: FINSEQ_8
    Summary: For two finite sequences, we present a notion of their concatenation, reducing overlapping part of the tail of the former and the head of the latter. At the same time, we also give a notion of common part of two finite sequences, which relates to the concatenation given here. A finite sequence is separated by another finite sequence (separator). We examined the condition that a separator separates uniquely any finite sequence. This will become a model of a separator of sequential files.
  22. Yasumasa Suzuki, Noboru Endou. Cauchy Sequence of Complex Unitary Space, Formalized Mathematics 12(2), pages 225-229, 2004. MML Identifier: CLVECT_3
    Summary: As an extension of \cite{BHSP_4.ABS}, we introduce the Cauchy sequence of complex unitary space and describe its properties.