Formalized Mathematics    (ISSN 1898-9934 (Online), ISSN 1426-2630 (Print))
Volume 12, Number 3 (2004): pdf, ps, dvi.
  1. Noboru Endou. Complex Valued Functions Space, Formalized Mathematics 12(3), pages 231-235, 2004. MML Identifier: CFUNCDOM
    Summary: This article is an extension of \cite{FUNCSDOM.ABS} to complex valued functions.
  2. Noboru Endou. Banach Algebra of Bounded Complex Linear Operators, Formalized Mathematics 12(3), pages 237-242, 2004. MML Identifier: CLOPBAN2
    Summary: This article is an extension of \cite{LOPBAN_2.ABS}.
  3. Yuzhong Ding, Xiquan Liang. Formulas and Identities of Trigonometric Functions, Formalized Mathematics 12(3), pages 243-246, 2004. MML Identifier: SIN_COS5
    Summary:
  4. Yuzhong Ding, Xiquan Liang. Solving Roots of the Special Polynomial Equation with Real Coefficients, Formalized Mathematics 12(3), pages 247-250, 2004. MML Identifier: POLYEQ_4
    Summary:
  5. Adam Grabowski, Artur Kornilowicz. Algebraic Properties of Homotopies, Formalized Mathematics 12(3), pages 251-260, 2004. MML Identifier: BORSUK_6
    Summary:
  6. Artur Kornilowicz, Yasunari Shidama, Adam Grabowski. The Fundamental Group, Formalized Mathematics 12(3), pages 261-268, 2004. MML Identifier: TOPALG_1
    Summary: This is the next article in a series devoted to homotopy theory (following \cite{BORSUK_2.ABS} and \cite{BORSUK_6.ABS}). The concept of fundamental groups of pointed topological spaces has been introduced. Isomorphism of fundamental groups defined with respect to different points belonging to the same component has been stated. Triviality of fundamental group(s) of ${\Bbb R}^n$ has been shown.
  7. Takaya Nishiyama, Keiji Ohkubo, Yasunari Shidama. The Continuous Functions on Normed Linear Spaces, Formalized Mathematics 12(3), pages 269-275, 2004. MML Identifier: NFCONT_1
    Summary: In this article, the basic properties of the continuous function on normed linear spaces are described.
  8. Takaya Nishiyama, Artur Kornilowicz, Yasunari Shidama. The Uniform Continuity of Functions on Normed Linear Spaces, Formalized Mathematics 12(3), pages 277-279, 2004. MML Identifier: NFCONT_2
    Summary: In this article, the basic properties of uniform continuity of functions on normed linear spaces are described.
  9. Noboru Endou. Series on Complex Banach Algebra, Formalized Mathematics 12(3), pages 281-288, 2004. MML Identifier: CLOPBAN3
    Summary: This article is an extension of \cite{LOPBAN_3.ABS}.
  10. Noboru Endou. Exponential Function on Complex Banach Algebra, Formalized Mathematics 12(3), pages 289-293, 2004. MML Identifier: CLOPBAN4
    Summary: This article is an extension of \cite{LOPBAN_4.ABS}.
  11. Artur Kornilowicz. The Fundamental Group of Convex Subspaces of $\calE^n_\rmT$, Formalized Mathematics 12(3), pages 295-299, 2004. MML Identifier: TOPALG_2
    Summary: The triviality of the fundamental group of subspaces of ${\cal E}^n_{\rm T}$ and ${\Bbb R}^{\bf 1}$ have been shown.
  12. Artur Kornilowicz, Yasunari Shidama. Intersections of Intervals and Balls in $\calE^n_\rmT$, Formalized Mathematics 12(3), pages 301-306, 2004. MML Identifier: TOPREAL9
    Summary:
  13. Magdalena Jastrzcebska, Adam Grabowski. Some Properties of Fibonacci Numbers, Formalized Mathematics 12(3), pages 307-313, 2004. MML Identifier: FIB_NUM2
    Summary: We formalized some basic properties of the Fibonacci numbers using definitions and lemmas from \cite{PRE_FF.ABS} and \cite{FIB_NUM.ABS}, e.g. Cassini's and Catalan's identities. We also showed the connections between Fibonacci numbers and Pythagorean triples as defined in \cite{PYTHTRIP.ABS}. The main result of this article is a proof of Carmichael Theorem on prime divisors of prime-generated Fibonacci numbers. According to it if we look at the prime factors of a Fibonacci number generated by a prime number, none of them has appeared as a factor in any earlier Fibonacci number. We plan to develop the full proof of the Carmichael Theorem following \cite{Yabuta:01}.
  14. Ewa Romanowicz, Adam Grabowski. The Hall Marriage Theorem, Formalized Mathematics 12(3), pages 315-320, 2004. MML Identifier: HALLMAR1
    Summary: The Marriage Theorem, as credited to Philip Hall \cite{Hall:1935}, gives the necessary and sufficient condition allowing us to select a distinct element from each of a finite collection $\{A_i\}$ of $n$ finite subsets. This selection, called a set of different representatives (SDR), exists if and only if the marriage condition (or Hall condition) is satisfied: $$\forall_{J\subseteq\{1,\dots,n\}}|\bigcup_{i\in J} A_i|\geq |J|.$$ The proof which is given in this article (according to Richard Rado, 1967) is based on the lemma that for finite sequences with non-trivial elements which satisfy Hall property there exists a reduction (see Def. 5) such that Hall property again holds (see Th.~29 for details).
  15. Hiroshi Imura, Morishige Kimura, Yasunari Shidama. The Differentiable Functions on Normed Linear Spaces, Formalized Mathematics 12(3), pages 321-327, 2004. MML Identifier: NDIFF_1
    Summary: In this article, the basic properties of the differentiable functions on normed linear spaces are described.
  16. Piotr Wojtecki, Adam Grabowski. Lucas Numbers and Generalized Fibonacci Numbers, Formalized Mathematics 12(3), pages 329-333, 2004. MML Identifier: FIB_NUM3
    Summary: The recursive definition of Fibonacci sequences \cite{PRE_FF.ABS} is a good starting point for various variants and generalizations. We can point out here e.g. Lucas (with $2$ and $1$ as opening values) and the so-called generalized Fibonacci numbers (starting with arbitrary integers $a$ and $b$). \par In this paper, we introduce Lucas and G-numbers and we state their basic properties analogous to those proven in \cite{FIB_NUM.ABS} and \cite{FIB_NUM2.ABS}.
  17. Katarzyna Romanowicz, Adam Grabowski. The Operation of Addition of Relational Structures, Formalized Mathematics 12(3), pages 335-339, 2004. MML Identifier: LATSUM_1
    Summary: The article contains the formalization of the addition operator on relational structures as defined by A.~Wro{\'n}ski \cite{Wronski:1974} (as a generalization of Troelstra's sum or Ja{\'s}kowski star addition). The ordering relation of $A \otimes B$ is given by $$\le_{A\otimes B}\:=\:\le_A\cup \le_B\cup\: (\le_A \circ \le_B),$$ where the carrier is defined as the set-theoretical union of carriers of $A$ and $B$. Main part -- Section 3 -- is devoted to the Mizar translation of Theorem 1 (iv--xiii), p.~66 of \cite{Wronski:1974}.
  18. Karol Pcak. The Nagata-Smirnov Theorem. Part I, Formalized Mathematics 12(3), pages 341-346, 2004. MML Identifier: NAGATA_1
    Summary: In this paper we define a discrete subset family of a topological space and basis sigma locally finite and sigma discrete. We prove first an auxiliary fact for discrete family and sigma locally finite and sigma discrete basis. We show also the necessary condition for the Nagata Smirnov theorem: every metrizable space is $T_3$ and has a sigma locally finite basis. Also, we define a sufficient condition for a $T_3$ topological space to be $T_4$. We introduce the concept of pseudo metric.
  19. Gijs Geleijnse, Grzegorz Bancerek. Properties of Groups, Formalized Mathematics 12(3), pages 347-350, 2004. MML Identifier: GROUP_8
    Summary: In this article we formalize theorems from Chapter 1 of \cite{Hall:1959}. Our article covers Theorems 1.5.4, 1.5.5 (inequality on indices), 1.5.6 (equality of indices), Lemma 1.6.1 and several other supporting theorems needed to complete the formalization.
  20. Dorota Czcestochowska, Adam Grabowski. Catalan Numbers, Formalized Mathematics 12(3), pages 351-353, 2004. MML Identifier: CATALAN1
    Summary: In this paper, we define Catalan sequence (starting from $0$) and prove some of its basic properties. The Catalan numbers ($0,1,1,2,5,14,42,\dots$) arise in a number of problems in combinatorics. They can be computed e.g. using the formula $$C_n=\frac{{{2n}\choose {n}}}{n+1},$$ their recursive definition is also well known: $$C_1=1,\quad C_n=\Sigma_{i=1}^{n-1}C_i C_{n-i},\quad n\geq 2.$$ Among other things, the Catalan numbers describe the number of ways in which parentheses can be placed in a sequence of numbers to be multiplied, two at a time.
  21. Violetta Kozarkiewicz, Adam Grabowski. Axiomatization of Boolean Algebras Based on Sheffer Stroke, Formalized Mathematics 12(3), pages 355-361, 2004. MML Identifier: SHEFFER1
    Summary: We formalized another axiomatization of Boolean algebras. The classical one, as introduced in \cite{LATTICES.ABS}, ``the fourth set of postulates'' due to Huntington \cite{Huntington1} (\cite{ROBBINS1.ABS} in Mizar) and the single axiom in terms of disjunction and negation \cite{ROBBINS2.ABS}. In this article, we aimed at the description of Boolean algebras using Sheffer stroke according to \cite{Sheffer:1913}, namely by the following three axioms: $$(x
  22. Aneta Lukaszuk, Adam Grabowski. Short Sheffer Stroke-Based Single Axiom for Boolean Algebras, Formalized Mathematics 12(3), pages 363-370, 2004. MML Identifier: SHEFFER2
    Summary: We continue the description of Boolean algebras in terms of the Sheffer stroke as defined in \cite{SHEFFER1.ABS}. The single axiomatization for BAs in terms of disjunction and negation was shown in \cite{ROBBINS2.ABS}. As was checked automatically with the help of automated theorem prover Otter, single axiom of the form $$(x
  23. Hiroshi Imura, Yuji Sakai, Yasunari Shidama. Differentiable Functions on Normed Linear Spaces. Part II, Formalized Mathematics 12(3), pages 371-374, 2004. MML Identifier: NDIFF_2
    Summary: A continuation of \cite{NDIFF_1.ABS}, the basic properties of the differentiable functions on normed linear spaces are described.
  24. Takaya Nishiyama, Hirofumi Fukura, Yatsuka Nakamura. Logical Correctness of Vector Calculation Programs, Formalized Mathematics 12(3), pages 375-380, 2004. MML Identifier: PRGCOR_2
    Summary: In C-program, vectors of $n$-dimension are sometimes represented by arrays, where the dimension n is saved in the 0-th element of each array. If we write the program in non-overwriting type, we can gi Here, we give a program calculating inner product of 2 vectors, as an example of such a type, and its Logical-Model. If the Logical-Model is well defined, and theorems tying the model with previous definitions are given, we can say that the program is correct logically. In case the program is given as implicit function form (i.e., the result of calculation is given by a variable of one of arguments of a function), its Logical-Model is given by a definition of a ne Logical correctness of such a program is shown by theorems following the definition. As examples of such programs, we presented vector calculation of add, sub, minus and scalar product.
  25. Hiroshi Imura, Masami Tanaka, Yatsuka Nakamura. Continuous Mappings between Finite and One-Dimensional Finite Topological Spaces, Formalized Mathematics 12(3), pages 381-384, 2004. MML Identifier: FINTOPO4
    Summary: We showed relations between separateness and inflation operation. We also gave some relations between separateness and connectedness defined before. For two finite topological spaces, we defined a continuous function from one to another. Some topological concepts are preserved by such continuous functions. We gave one-dimensional concrete models of finite topological space.
  26. Karol Pcak. The Nagata-Smirnov Theorem. Part II, Formalized Mathematics 12(3), pages 385-389, 2004. MML Identifier: NAGATA_2
    Summary: In this paper we show some auxiliary facts for sequence function to be pseudo-metric. Next we prove the Nagata-Smirnov theorem that every topological space is metrizable if and only if it has $\sigma$-locally finite basis. We attach also the proof of the Bing's theorem that every topological space is metrizable if and only if its basis is $\sigma$-discrete.
  27. Artur Kornilowicz. On the Isomorphism of Fundamental Groups, Formalized Mathematics 12(3), pages 391-396, 2004. MML Identifier: TOPALG_3
    Summary:
  28. Noboru Endou. Algebra of Complex Vector Valued Functions, Formalized Mathematics 12(3), pages 397-401, 2004. MML Identifier: VFUNCT_2
    Summary: This article is an extension of \cite{VFUNCT_1.ABS}.
  29. Noboru Endou. Continuous Functions on Real and Complex Normed Linear Spaces, Formalized Mathematics 12(3), pages 403-419, 2004. MML Identifier: NCFCONT1
    Summary: This article is an extension of \cite{NFCONT_1.ABS}.
  30. Artur Kornilowicz. On the Fundamental Groups of Products of Topological Spaces, Formalized Mathematics 12(3), pages 421-425, 2004. MML Identifier: TOPALG_4
    Summary: In the paper we show that fundamental group of the product of two topological spaces is isomorphic to the product of fundamental groups of the spaces.