Formalized Mathematics    (ISSN 1426-2630)
Volume 9, Number 3 (2001): pdf, ps, dvi.
  1. Andrzej Trybulec. The Canonical Formulae, Formalized Mathematics 9(3), pages 441-447, 2001. MML Identifier: HILBERT3
    Summary:
  2. Adam Grabowski. The Incompleteness of the Lattice of Substitutions, Formalized Mathematics 9(3), pages 449-454, 2001. MML Identifier: HEYTING3
    Summary: In \cite{HEYTING3.ABS} we proved that the lattice of substitutions, as defined in \cite{SUBSTLAT.ABS}, is a Heyting lattice (i.e. it is pseudo-complemented and it has the zero element). We show that the lattice needs not to be complete. Obviously, the example has to be infinite, namely we can take the set of natural numbers as variables and a singleton as a set of constants. The incompleteness has been shown for lattices of substitutions defined in terms of \cite{LATTICES.ABS} and relational structures \cite{ORDERS_1.ABS}.
  3. Robert Milewski. Trigonometric Form of Complex Numbers, Formalized Mathematics 9(3), pages 455-460, 2001. MML Identifier: COMPTRIG
    Summary:
  4. Robert Milewski. Fundamental Theorem of Algebra, Formalized Mathematics 9(3), pages 461-470, 2001. MML Identifier: POLYNOM5
    Summary:
  5. Hiroshi Yamazaki, Yoshinori Fujisawa, Yatsuka Nakamura. On Replace Function and Swap Function for Finite Sequences, Formalized Mathematics 9(3), pages 471-474, 2001. MML Identifier: FINSEQ_7
    Summary: In this article, we show the property of the Replace Function and the Swap Function of finite sequences. In the first section, we prepared some useful theorems for finite sequences. In the second section, we defined the Replace function and proved some theorems about the function. This function replaces an element of a sequence by another value. In the third section, we defined the Swap function and proved some theorems about the function. This function swaps two elements of a sequence. In the last section, we show the property of composed functions of the Replace Function and the Swap Function.
  6. Hiroshi Yamazaki, Katsumi Wasaki. The Correctness of the High Speed Array Multiplier Circuits, Formalized Mathematics 9(3), pages 475-479, 2001. MML Identifier: GATE_5
    Summary: This article introduces the verification of the correctness for the operations and the specification of the high speed array multiplier. We formalize the concepts of 2-by-2 and 3-by-3 bit Plain array multiplier, 3-by-3 Wallace tree multiplier circuit, and show that outputs of the array multiplier are equivalent to outputs of normal (sequencial) multiplier.
  7. Andrzej Trybulec. Some Lemmas for the Jordan Curve Theorem, Formalized Mathematics 9(3), pages 481-484, 2001. MML Identifier: JCT_MISC
    Summary: I present some miscellaneous simple facts that are still missing in the library. The only common feature is that, most of them, were needed as lemmas in the proof of the Jordan curve theorem.
  8. Josef Urban. Mahlo and Inaccessible Cardinals, Formalized Mathematics 9(3), pages 485-489, 2001. MML Identifier: CARD_LAR
    Summary: This article contains basic ordinal topology: closed unbounded and stationary sets and necessary theorems about them, completness of the centered system of Clubs of $M$, Mahlo and strongly Mahlo cardinals, the proof that (strongly) Mahlo is (strongly) inaccessible, and the proof that Rank of strongly inaccessible is a model of ZF.
  9. Noboru Endou, Katsumi Wasaki, Yasunari Shidama. Basic Properties of Extended Real Numbers, Formalized Mathematics 9(3), pages 491-494, 2001. MML Identifier: EXTREAL1
    Summary: We introduce product, quotient and absolute value, and we prove some basic properties of extended real numbers.
  10. Noboru Endou, Katsumi Wasaki, Yasunari Shidama. Definitions and Basic Properties of Measurable Functions, Formalized Mathematics 9(3), pages 495-500, 2001. MML Identifier: MESFUNC1
    Summary: In this article we introduce some definitions concerning measurable functions and prove related properties.
  11. Artur Kornilowicz, Robert Milewski, Adam Naumowicz, Andrzej Trybulec. Gauges and Cages. Part I, Formalized Mathematics 9(3), pages 501-509, 2001. MML Identifier: JORDAN1A
    Summary:
  12. Noboru Endou, Katsumi Wasaki, Yasunari Shidama. Some Properties of Extended Real Numbers Operations: abs, min and max, Formalized Mathematics 9(3), pages 511-516, 2001. MML Identifier: EXTREAL2
    Summary: In this article, we extend some properties concerning real numbers to extended real numbers. Almost all properties included in this article are extended properties of other articles: \cite{AXIOMS.ABS}, \cite{REAL_1.ABS}, \cite{ABSVALUE.ABS}, \cite{SQUARE_1.ABS} and \cite{REAL_2.ABS}.
  13. Takashi Mitsuishi, Katsumi Wasaki, Yasunari Shidama. The Concept of Fuzzy Relation and Basic Properties of its Operation, Formalized Mathematics 9(3), pages 517-524, 2001. MML Identifier: FUZZY_3
    Summary: This article introduces the fuzzy relation. This is the expansion of usual relation, and the value is given at the fuzzy value. At first, the definition of the fuzzy relation characterized by membership function is described. Next, the definitions of the zero relation and universe relation and basic operations of these relations are shown.
  14. Noboru Endou, Katsumi Wasaki, Yasunari Shidama. The Measurability of Extended Real Valued Functions, Formalized Mathematics 9(3), pages 525-529, 2001. MML Identifier: MESFUNC2
    Summary: In this article we prove the measurablility of some extended real valued functions which are $f$+$g$, $f$\,--\,$g$ and so on. Moreover, we will define the simple function which are defined on the sigma field. It will play an important role for the Lebesgue integral theory.
  15. Robert Milewski, Andrzej Trybulec, Artur Kornilowicz, Adam Naumowicz. Some Properties of Cells and Arcs, Formalized Mathematics 9(3), pages 531-535, 2001. MML Identifier: JORDAN1B
    Summary:
  16. Gang Liu, Yasushi Fuwa, Masayoshi Eguchi. Formal Topological Spaces, Formalized Mathematics 9(3), pages 537-543, 2001. MML Identifier: FINTOPO2
    Summary: This article is divided into two parts. In the first part, we prove some useful theorems on finite topological spaces. In the second part, in order to consider a family of neighborhoods to a point in a space, we extend the notion of finite topological space and define a new topological space, which we call formal topological space. We show the relation between formal topological space struct ({\tt FMT\_Space\_Str}) and the {\tt TopStruct} by giving a function ({\tt NeighSp}). And the following notions are introduced in formal topological spaces: boundary, closure, interior, isolated point, connected point, open set and close set, then some basic facts concerning them are proved. We will discuss the relation between the formal topological space and the finite topological space in future work.
  17. Adam Grabowski, Artur Kornilowicz, Andrzej Trybulec. Some Properties of Cells and Gauges, Formalized Mathematics 9(3), pages 545-548, 2001. MML Identifier: JORDAN1C
    Summary:
  18. Andrzej Trybulec, Yatsuka Nakamura. Again on the Order on a Special Polygon, Formalized Mathematics 9(3), pages 549-553, 2001. MML Identifier: SPRECT_5
    Summary:
  19. Artur Kornilowicz, Robert Milewski. Gauges and Cages. Part II, Formalized Mathematics 9(3), pages 555-558, 2001. MML Identifier: JORDAN1D
    Summary:
  20. Christoph Schwarzweller. The Binomial Theorem for Algebraic Structures, Formalized Mathematics 9(3), pages 559-564, 2001. MML Identifier: BINOM
    Summary: In this paper we prove the well-known binomial theorem for algebraic structures. In doing so we tried to be as modest as possible concerning the algebraic properties of the underlying structure. Consequently, we proved the binomial theorem for ``commutative rings'' in which the existence of an inverse with respect to addition is replaced by a weaker property of cancellation.
  21. Jonathan Backer, Piotr Rudnicki, Christoph Schwarzweller. Ring Ideals, Formalized Mathematics 9(3), pages 565-582, 2001. MML Identifier: IDEAL_1
    Summary: We introduce the basic notions of ideal theory in rings. This includes left and right ideals, (finitely) generated ideals and some operations on ideals such as the addition of ideals and the radical of an ideal. In addition we introduce linear combinations to formalize the well-known characterization of generated ideals. Principal ideal domains and Noetherian rings are defined. The latter development follows \cite{Becker93}, pages 144--145.
  22. Jonathan Backer, Piotr Rudnicki. Hilbert Basis Theorem, Formalized Mathematics 9(3), pages 583-589, 2001. MML Identifier: HILBASIS
    Summary: We prove the Hilbert basis theorem following \cite{Becker93}, page 145. First we prove the theorem for the univariate case and then for the multivariate case. Our proof for the latter is slightly different than in \cite{Becker93}. As a base case we take the ring of polynomilas with no variables. We also prove that a polynomial ring with infinite number of variables is not Noetherian.
  23. Franz Merkl. Dynkin's Lemma in Measure Theory, Formalized Mathematics 9(3), pages 591-595, 2001. MML Identifier: DYNKIN
    Summary: This article formalizes the proof of Dynkin's lemma in measure theory. Dynkin's lemma is a useful tool in measure theory and probability theory: it helps frequently to generalize a statement about all elements of a intersection-stable set system to all elements of the sigma-field generated by that system.
  24. Mariusz Giero, Roman Matuszewski. Lower Tolerance. Preliminaries to Wroclaw Taxonomy, Formalized Mathematics 9(3), pages 597-603, 2001. MML Identifier: TAXONOM1
    Summary: The paper introduces some preliminary notions concerning the Wroclaw taxonomy according to \cite{MatTry77}. The classifications and tolerances are defined and considered w.r.t. sets and metric spaces. We prove theorems showing various classifications based on tolerances.
  25. Grzegorz Bancerek. Concrete Categories, Formalized Mathematics 9(3), pages 605-621, 2001. MML Identifier: YELLOW18
    Summary: In the paper, we develop the notation of duality and equivalence of categories and concrete categories based on \cite{ALTCAT_1.ABS}. The development was motivated by the duality theory for continuous lattices (see \cite[p. 189]{CCL}), where we need to cope with concrete categories of lattices and maps preserving their properties. For example, the category {\it UPS} of complete lattices and directed suprema preserving maps; or the category {\it INF} of complete lattices and infima preserving maps. As the main result of this paper it is shown that every category is isomorphic to its concretization (the concrete category with the same objects). Some useful schemes to construct categories and functors are also presented.
  26. Andrzej Trybulec. Classes of Independent Partitions, Formalized Mathematics 9(3), pages 623-625, 2001. MML Identifier: PARTIT_2
    Summary: The paper includes proofs of few theorems proved earlier by Shunichi Kobayashi in many different settings.
  27. Jozef Bialas, Yatsuka Nakamura. Some Properties of Dyadic Numbers and Intervals, Formalized Mathematics 9(3), pages 627-630, 2001. MML Identifier: URYSOHN2
    Summary: The article is the second part of a paper proving the fundamental Urysohn Theorem concerning the existence of a real valued continuous function on a normal topological space. The paper is divided into two parts. In the first part, we introduce some definitions and theorems concerning properties of intervals; in the second we prove some of properties of dyadic numbers used in proving Urysohn Lemma.
  28. Jozef Bialas, Yatsuka Nakamura. The Urysohn Lemma, Formalized Mathematics 9(3), pages 631-636, 2001. MML Identifier: URYSOHN3
    Summary: This article is the third part of a paper proving the fundamental Urysohn Theorem concerning the existence of a real valued continuous function on a normal topological space. The paper is divided into two parts. In the first part, we describe the construction of the function solving thesis of the Urysohn Lemma. The second part contains the proof of the Urysohn Lemma in normal space and the proof of the same theorem for compact space.
  29. Ewa Grdzka. The Algebra of Polynomials, Formalized Mathematics 9(3), pages 637-643, 2001. MML Identifier: POLYALG1
    Summary: In this paper we define the algebra of formal power series and the algebra of polynomials over an arbitrary field and prove some properties of these structures. We also formulate and prove theorems showing some general properties of sequences. These preliminaries will be used for defining and considering linear functionals on the algebra of polynomials.
  30. Grzegorz Bancerek. Circuit Generated by Terms and Circuit Calculating Terms, Formalized Mathematics 9(3), pages 645-657, 2001. MML Identifier: CIRCTRM1
    Summary: In the paper we investigate the dependence between the structure of circuits and sets of terms. Circuits in our terminology (see \cite{CIRCUIT1.ABS}) are treated as locally-finite many sorted algebras over special signatures. Such approach enables to formalize every real circuit. The goal of this investigation is to specify circuits by terms and, enentualy, to have methods of formal verification of real circuits. The following notation is introduced in this paper: \begin{itemize} \item structural equivalence of circuits, i.e. equivalence of many sorted signatures, \item embedding of a circuit into another one, \item similarity of circuits (a concept narrower than isomorphism of many sorted algebras over equivalent signatures), \item calculation of terms by a circuit according to an algebra, \item specification of circuits by terms and an algebra. \end{itemize}