Formalized Mathematics    (ISSN 1898-9934 (Online), ISSN 1426-2630 (Print))
Volume 11, Number 1 (2003): pdf, ps, dvi.
  1. Noboru Endou, Takashi Mitsuishi, Yasunari Shidama. Subspaces and Cosets of Subspace of Real Unitary Space, Formalized Mathematics 11(1), pages 1-7, 2003. MML Identifier: RUSUB_1
    Summary: In this article, subspace and the coset of subspace of real unitary space are defined. And we discuss some of their fundamental properties.
  2. Noboru Endou, Takashi Mitsuishi, Yasunari Shidama. Operations on Subspaces in Real Unitary Space, Formalized Mathematics 11(1), pages 9-16, 2003. MML Identifier: RUSUB_2
    Summary: In this article, we extend an operation of real linear space to real unitary space. We show theorems proved in \cite{RLSUB_2.ABS} on real unitary space.
  3. Noboru Endou, Takashi Mitsuishi, Yasunari Shidama. Linear Combinations in Real Unitary Space, Formalized Mathematics 11(1), pages 17-22, 2003. MML Identifier: RUSUB_3
    Summary: In this article, we mainly discuss linear combination of vectors in Real Unitary Space and dimension of the space. As the result, we obtain some theorems that are similar to those in Real Linear Space.
  4. Noboru Endou, Takashi Mitsuishi, Yasunari Shidama. Dimension of Real Unitary Space, Formalized Mathematics 11(1), pages 23-28, 2003. MML Identifier: RUSUB_4
    Summary: In this article we describe the dimension of real unitary space. Most of theorems are restricted from real linear space. In the last section, we introduce affine subset of real unitary space.
  5. Takashi Mitsuishi, Noboru Endou, Keiji Ohkubo. Trigonometric Functions on Complex Space, Formalized Mathematics 11(1), pages 29-32, 2003. MML Identifier: SIN_COS3
    Summary: This article describes definitions of sine, cosine, hyperbolic sine and hyperbolic cosine. Some of their basic properties are discussed.
  6. Noboru Endou, Takashi Mitsuishi, Yasunari Shidama. Topology of Real Unitary Space, Formalized Mathematics 11(1), pages 33-38, 2003. MML Identifier: RUSUB_5
    Summary: In this article we introduce three subjects in real unitary space: parallelism of subsets, orthogonality of subsets and topology of the space. In particular, to introduce the topology of real unitary space, we discuss the metric topology which is induced by the inner product in the space. As the result, we are able to discuss some topological subjects on real unitary space.
  7. William W. Armstrong, Yatsuka Nakamura, Piotr Rudnicki. Armstrong's Axioms, Formalized Mathematics 11(1), pages 39-51, 2003. MML Identifier: ARMSTRNG
    Summary: We present a formalization of the seminal paper by W.~W.~Armstrong~\cite{arm74} on functional dependencies in relational data bases. The paper is formalized in its entirety including examples and applications. The formalization was done with a routine effort albeit some new notions were defined which simplified formulation of some theorems and proofs.\par The definitive reference to the theory of relational databases is~\cite{Maier}, where saturated sets are called closed sets. Armstrong's ``axioms'' for functional dependencies are still widely taught at all levels of database design, see for instance~\cite{Elmasri}.
  8. Noboru Endou, Takashi Mitsuishi, Yasunari Shidama. Convex Sets and Convex Combinations, Formalized Mathematics 11(1), pages 53-58, 2003. MML Identifier: CONVEX1
    Summary: Convexity is one of the most important concepts in a study of analysis. Especially, it has been applied around the optimization problem widely. Our purpose is to define the concept of convexity of a set on Mizar, and to develop the generalities of convex analysis. The construction of this article is as follows: Convexity of the set is defined in the section 1. The section 2 gives the definition of convex combination which is a kind of the linear combination and related theorems are proved there. In section 3, we define the convex hull which is an intersection of all convex sets including a given set. The last section is some theorems which are necessary to compose this article.
  9. Jaroslaw Kotowicz. Quotient Vector Spaces and Functionals, Formalized Mathematics 11(1), pages 59-68, 2003. MML Identifier: VECTSP10
    Summary: The article presents well known facts about quotient vector spaces and functionals (see \cite{SLang}). There are repeated theorems and constructions with either weaker assumptions or in more general situations (see \cite{HAHNBAN.ABS}, \cite{VECTSP_1.ABS}, \cite{LMOD_7.ABS}). The construction of coefficient functionals and non degenerated functional in quotient vector space generated by functional in the given vector space are the only new things which are done.
  10. Jaroslaw Kotowicz. Bilinear Functionals in Vector Spaces, Formalized Mathematics 11(1), pages 69-86, 2003. MML Identifier: BILINEAR
    Summary: The main goal of the article is the presentation of the theory of bilinear functionals in vector spaces. It introduces standard operations on bilinear functionals and proves their classical properties. It is shown that quotient functionals are non degenerated on the left and the right. In the case of symmetric and alternating bilinear functionals it is shown that the left and right kernels are equal.
  11. Jaroslaw Kotowicz. Hermitan Functionals. Canonical Construction of Scalar Product in Quotient Vector Space, Formalized Mathematics 11(1), pages 87-98, 2003. MML Identifier: HERMITAN
    Summary: In the article we present antilinear functionals, sesquilinear and hermitan forms. We prove Schwarz and Minkowski inequalities, and Parallelogram Law for non negative hermitan form. The proof of Schwarz inequality is based on \cite{RUDIN:2}. The incorrect proof of this fact can be found in \cite{Maurin}. The construction of scalar product in quotient vector space from non negative hermitan functions is the main result of the article.
  12. Krzysztof Retel. The Class of Series -- Parallel Graphs. Part I, Formalized Mathematics 11(1), pages 99-103, 2003. MML Identifier: NECKLACE
    Summary: The paper introduces some preliminary notions concerning the graph theory according to \cite{Thomasse}. We define Necklace $n$ as a graph with vertex $\{1,2,3,\dots,n\}$ and edge set $\{(1,2),(2,3),\dots,(n-1,n)\}.$ The goal of the article is to prove that Necklace $n$ and Complement of Necklace $n$ are isomorphic for $n = 0, 1, 4.$
  13. Christoph Schwarzweller. Term Orders, Formalized Mathematics 11(1), pages 105-111, 2003. MML Identifier: TERMORD
    Summary: We continue the formalization of \cite{Becker93} towards Gr\"obner Bases. Here we deal with term orders, that is with orders on bags. We introduce the notions of head term, head coefficient, and head monomial necessary to define reduction for polynomials.
  14. Christoph Schwarzweller. Polynomial Reduction, Formalized Mathematics 11(1), pages 113-123, 2003. MML Identifier: POLYRED
    Summary: We continue the formalization of \cite{Becker93} towards Gr\"obner Bases. In this article we introduce reduction of polynomials and prove its termination, its adequateness for ideal congruence as well as the translation lemma used later to show confluence of reduction.
  15. Grzegorz Bancerek, Mitsuru Aoki, Akio Matsumoto, Yasunari Shidama. Processes in Petri nets, Formalized Mathematics 11(1), pages 125-132, 2003. MML Identifier: PNPROC_1
    Summary: Sequential and concurrent compositions of processes in Petri nets are introduced. A process is formalized as a set of (possible), so called, firing sequences. In the definition of the sequential composition the standard concatenation is used $$ R_1 \mathop{\rm before} R_2 = \{p_1\mathop{^\frown}p_2: p_1\in R_1\ \land\ p_2\in R_2\} $$ The definition of the concurrent composition is more complicated $$ R_1 \mathop{\rm concur} R_2 = \{ q_1\cup q_2: q_1\ {\rm misses}\ q_2\ \land\ \mathop{\rm Seq} q_1\in R_1\ \land\ \mathop{\rm Seq} q_2\in R_2\} $$ For example, $$ \{\langle t_0\rangle\} \mathop{\rm concur} \{\langle t_1,t_2\rangle\} = \{\langle t_0,t_1,t_2\rangle , \langle t_1,t_0,t_2\rangle , \langle t_1,t_2,t_0\rangle\} $$ The basic properties of the compositions are shown.