Formalized Mathematics    (ISSN 1898-9934 (Online), ISSN 1426-2630 (Print))
Volume 13, Number 4 (2005): pdf, ps, dvi.
  1. Bo Zhang, Hiroshi Yamazaki, Yatsuka Nakamura. Set Sequences and Monotone Class, Formalized Mathematics 13(4), pages 435-441, 2005. MML Identifier: PROB_3
    Summary: In this paper, we first defined the partial-union sequence, the partial-intersection sequence, and the partial-difference-union sequence of given sequence of subsets, and then proved the additive theorem of infinite sequences and sub-additive theorem of finite sequences for probability. Further, we defined the monotone class of families of subsets, and discussed about the relations between the monotone class and the $\sigma$-field which are generated by field of subsets of a given set.
  2. Hirofumi Fukura, Yatsuka Nakamura. A Theory of Sequential Files, Formalized Mathematics 13(4), pages 443-446, 2005. MML Identifier: FILEREC1
    Summary: This article is a continuation of \cite{FINSEQ_8.ABS}. We present a notion of files and records. These are two finite sequences. One is a record and another is a separator for the carriage return and/or line feed. So, we define a record. The sequential text file contains records and separators. Generally, a record and a separator are paired in the file. And in a special situation, the separator does not exist in the file, for that the record is only one record or record is nothing. And the record does not exist in the file, for that some separator is in file. In this article, we present some theory for files and records.
  3. Fahui Zhai, Jianbing Cao, Xiquan Liang. Circled Sets, Circled Hull, and Circled Family, Formalized Mathematics 13(4), pages 447-451, 2005. MML Identifier: CIRCLED1
    Summary: In this article, we prove some basic properties of the circled sets. We also define the circled hull, and give the definition of circled family.
  4. Adam Grabowski. On the Borel Families of Subsets of Topological Spaces, Formalized Mathematics 13(4), pages 453-461, 2005. MML Identifier: TOPGEN_4
    Summary: This is the next Mizar article in a series aiming at complete formalization of ``General Topology'' \cite{ENGEL:1} by Engelking. We cover the second part of Section 1.3.
  5. Noboru Endou, Yasunari Shidama. Linearity of Lebesgue Integral of Simple Valued Function, Formalized Mathematics 13(4), pages 463-465, 2005. MML Identifier: MESFUNC4
    Summary: In this article, the authors prove linearity of Lebesgue integral of simple valued function.
  6. Yatsuka Nakamura, Andrzej Trybulec, Artur Kornilowicz. The Fashoda Meet Theorem for Continuous Mappings, Formalized Mathematics 13(4), pages 467-469, 2005. MML Identifier: JGRAPH_8
    Summary: {}
  7. Artur Kornilowicz, Grzegorz Bancerek, Adam Naumowicz. Tietze Extension Theorem, Formalized Mathematics 13(4), pages 471-475, 2005. MML Identifier: TIETZE
    Summary: In this paper we formalize the Tietze extension theorem using as a basis the proof presented at the PlanetMath web server (\url{http://planetmath.org/encyclopedia/ProofOfTietzeExtensionTheorem2.html}).
  8. Adam Naumowicz, Grzegorz Bancerek. Homeomorphisms of Jordan Curves, Formalized Mathematics 13(4), pages 477-480, 2005. MML Identifier: JORDAN24
    Summary: In this paper we prove that simple closed curves can be homeomorphically framed into a given rectangle. We also show that homeomorphisms preserve the Jordan property.
  9. Artur Kornilowicz. Jordan Curve Theorem, Formalized Mathematics 13(4), pages 481-491, 2005. MML Identifier: JORDAN
    Summary: This paper formalizes the Jordan Curve Theorem following \cite{BrouwerJordan}.
  10. Wenpai Chang, Hiroshi Yamazaki, Yatsuka Nakamura. The Inner Product and Conjugate of Matrix of Complex Numbers, Formalized Mathematics 13(4), pages 493-499, 2005. MML Identifier: MATRIXC1
    Summary: Concepts of the inner product and conjugate of matrix of complex numbers are defined here. Operations such as addition, subtraction, scalar multiplication and inner product are introduced using correspondent definitions of the conjugate of a matrix of a complex field. Many equations for such operations consist like a case of the conjugate of matrix of a field and some operations on the set of sum of complex numbers are introduced.
  11. Jianbing Cao, Fahui Zhai, Xiquan Liang. Partial Sum and Partial Product of Some Series, Formalized Mathematics 13(4), pages 501-503, 2005. MML Identifier: SERIES_4
    Summary: This article contains partial sum and partial product of some series which are often used.
  12. Jianbing Cao, Fahui Zhai, Xiquan Liang. Some Differentiable Formulas of Special Functions, Formalized Mathematics 13(4), pages 505-509, 2005. MML Identifier: FDIFF_5
    Summary: This article contains some differentiable formulas of special functions.
  13. Pacharapokin Chanapat, Hiroshi Yamazaki. Formulas and Identities of Hyperbolic Functions, Formalized Mathematics 13(4), pages 511-513, 2005. MML Identifier: SIN_COS8
    Summary: In this article, we proved formulas of hyperbolic sine, hyperbolic cosine and hyperbolic tangent, and their identities.
  14. Grzegorz Bancerek. Niemytzki Plane - an Example of Tychonoff Space Which Is Not $T_4$, Formalized Mathematics 13(4), pages 515-524, 2005. MML Identifier: TOPGEN_5
    Summary: We continue Mizar formalization of General Topology according to the book \cite{ENGEL:1} by Engelking. Niemytzki plane is defined as halfplane $y \geq 0$ with topology introduced by a neighborhood system. Niemytzki plane is not $T_4$. Next, the definition of Tychonoff space is given. The characterization of Tychonoff space by prebasis and the fact that Tychonoff spaces are between $T_3$ and $T_4$ is proved. The final result is that Niemytzki plane is also a Tychonoff space.
  15. Fuguo Ge, Xiquan Liang. On the Partial Product and Partial Sum of Series and Related Basic Inequalities, Formalized Mathematics 13(4), pages 525-528, 2005. MML Identifier: SERIES_5
    Summary: This article introduced some important inequalities on partial sum and partial product, as well as some basic inequalities.
  16. Yan Zhang, Bo Li, Xiquan Liang. Several Differentiable Formulas of Special Functions. Part II, Formalized Mathematics 13(4), pages 529-535, 2005. MML Identifier: FDIFF_6
    Summary: In this article, we give other several differentiable formulas of special functions.
  17. Shunichi Kobayashi. On the Calculus of Binary Arithmetics. Part II, Formalized Mathematics 13(4), pages 537-540, 2005. MML Identifier: BINARI_6
    Summary:
  18. Xiaopeng Yue, Xiquan Liang, Zhongpin Sun. Some Properties of Some Special Matrices, Formalized Mathematics 13(4), pages 541-547, 2005. MML Identifier: MATRIX_6
    Summary: This article describes definitions of reversible matrix, symmetrical matrix, antisymmetric matrix, orthogonal matrix and their main properties.
  19. Shin'nosuke Yamaguchi, Katsumi Wasaki, Nobuhiro Shimoi. Generalized Full Adder Circuits (GFAs). Part I, Formalized Mathematics 13(4), pages 549-571, 2005. MML Identifier: GFACIRC1
    Summary: We formalize the concept of the Generalized Full Addition and Subtraction circuits (GFAs), define the structures of calculation units for the redundant signed digit (RSD) operations, and prove the stability of the circuits. Generally, one-bit binary full adder assumes positive weights to all of its three binary inputs and two outputs. We obtain four type of 1-bit GFA to constract the RSD arithmetic logical units that we generalize full adder to have both positive and negative weights to inputs and outputs.
  20. Artur Kornilowicz. Quotient Rings, Formalized Mathematics 13(4), pages 573-576, 2005. MML Identifier: RING_1
    Summary: The notions of prime ideals and maximal ideals of a ring are introduced. Quotient rings are defined. Characterisation of of prime and maximal ideals using quotient rings are proved.
  21. Noboru Endou, Yasunari Shidama. Completeness of the Real Euclidean Space, Formalized Mathematics 13(4), pages 577-580, 2005. MML Identifier: REAL_NS1
    Summary: {}