Formalized Mathematics    (ISSN 0777-4028)
Volume 2, Number 4 (1991): pdf, ps, dvi.
  1. Konrad Raczkowski, Andrzej Ndzusiak. Series, Formalized Mathematics 2(4), pages 449-452, 1991. MML Identifier: SERIES_1
    Summary: The article contains definitions and properties of convergent serieses.
  2. Marek Chmur. The Lattice of Natural Numbers and The Sublattice of it. The Set of Prime Numbers, Formalized Mathematics 2(4), pages 453-459, 1991. MML Identifier: NAT_LAT
    Summary: Basic properties of the least common multiple and the greatest common divisor. The lattice of natural numbers (${\rm L}_{\Bbb N}$) and the lattice of natural numbers greater than zero (${\rm L}_{\Bbb N^+}$) are constructed. The notion of the sublattice of the lattice of natural numbers is given. Some facts about it are proved. The last part of the article deals with some properties of prime numbers and with the notions of the set of prime numbers and the $n$-th prime number. It is proved that the set of prime numbers is infinite.
  3. Wojciech A. Trybulec. Commutator and Center of a Group, Formalized Mathematics 2(4), pages 461-466, 1991. MML Identifier: GROUP_5
    Summary: We introduce the notions of commutators of element, subgroups of a group, commutator of a group and center of a group. We prove P.Hall identity. The article is based on \cite{KARGAP:1}.
  4. Andrzej Trybulec. Natural Transformations. Discrete Categories, Formalized Mathematics 2(4), pages 467-474, 1991. MML Identifier: NATTRA_1
    Summary: We present well known concepts of category theory: natural transformations and functor categories, and prove propositions related to. Because of the formalization it proved to be convenient to introduce some auxiliary notions, for instance: transformations. We mean by a transformation of a functor $F$ to a functor $G$, both covariant functors from $A$ to $B$, a function mapping the objects of $A$ to the morphisms of $B$ and assigning to an object $a$ of $A$ an element of $\mathop{\rm Hom}(F(a),G(a))$. The material included roughly corresponds to that presented on pages 18,129--130,137--138 of the monography (\cite{SEMAD}). We also introduce discrete categories and prove some propositions to illustrate the concepts introduced.
  5. Katarzyna Jankowska. Matrices. Abelian Group of Matrices, Formalized Mathematics 2(4), pages 475-480, 1991. MML Identifier: MATRIX_1
    Summary: The basic conceptions of matrix algebra are introduced. The matrix is introduced as the finite sequence of sequences with the same length, i.e. as a sequence of lines. There are considered matrices over a field, and the fact that these matrices with addition form an Abelian group is proved.
  6. Leszek Borys. Paracompact and Metrizable Spaces, Formalized Mathematics 2(4), pages 481-485, 1991. MML Identifier: PCOMPS_1
    Summary: We give an example of a compact space. Next we define a locally finite subset family of a topological space and a paracompact topological space. An open sets family of a metric space we define next and it has been shown that the metric space with any open sets family is a topological space. Next we define metrizable space.
  7. Michal Muzalewski. Atlas of Midpoint Algebra, Formalized Mathematics 2(4), pages 487-491, 1991. MML Identifier: MIDSP_2
    Summary: This article is a continuation of \cite{MIDSP_1.ABS}. We have established a one-to-one correspondence between midpoint algebras and groups with the operator 1/2. In general we shall say that a given midpoint algebra $M$ and a group $V$ are $w$-assotiated iff $w$ is an atlas from $M$ to $V$. At the beginning of the paper a few facts which rather belong to \cite{VECTSP_1.ABS}, \cite{MOD_1.MIZ} are proved.
  8. Jozef Bialas. Several Properties of the $\sigma$-additive Measure, Formalized Mathematics 2(4), pages 493-497, 1991. MML Identifier: MEASURE2
    Summary: A continuation of \cite{MEASURE1.ABS}. The paper contains the definition and basic properties of a $\sigma$-additive, nonnegative measure, with values in $\overline{\Bbb R}$, the enlarged set of real numbers, where $\overline{\Bbb R}$ denotes set $\overline{\Bbb R} = {\Bbb R} \cup \{-\infty,+\infty\}$ --- by R.~Sikorski \cite{SIKORSKI:1}. Some simple theorems concerning basic properties of a $\sigma$-additive measure, measurable sets, measure zero sets are proved. The work is the fourth part of the series of articles concerning the Lebesgue measure theory.
  9. Stanislawa Kanas, Adam Lecko. Metrics in the Cartesian Product -- Part II, Formalized Mathematics 2(4), pages 499-504, 1991. MML Identifier: METRIC_4
    Summary: A continuation of \cite{METRIC_3.ABS}. It deals with the method of creation of the distance in the Cartesian product of metric spaces. The distance between two points belonging to Cartesian product of metric spaces has been defined as square root of the sum of squares of distances of appropriate coordinates (or projections) of these points. It is shown that product of metric spaces with such a distance is a metric space. Examples of metric spaces defined in this way are given.
  10. Alicia de la Cruz. Fix Point Theorem for Compact Spaces, Formalized Mathematics 2(4), pages 505-506, 1991. MML Identifier: ALI2
    Summary: The Banach theorem in compact metric spaces is proved.
  11. Jan Popiolek. Quadratic Inequalities, Formalized Mathematics 2(4), pages 507-509, 1991. MML Identifier: QUIN_1
    Summary: Consider a quadratic trinomial of the form $P(x)=ax^2+bx+c$, where $a\ne 0$. The determinant of the equation $P(x)=0$ is of the form $\Delta(a,b,c)=b^2-4ac$. We prove several quadratic inequalities when $\Delta(a,b,c)<0$, $\Delta(a,b,c)=0$ and $\Delta(a,b,c)>0$.
  12. Jan Popiolek. Introduction to Banach and Hilbert Spaces -- Part I, Formalized Mathematics 2(4), pages 511-516, 1991. MML Identifier: BHSP_1
    Summary: Basing on the notion of real linear space (see \cite{RLVECT_1.ABS}) we introduce real unitary space. At first, we define the scalar product of two vectors and examine some of its properties. On the base of this notion we introduce the norm and the distance in real unitary space and study properties of these concepts. Next, proceeding from the definition of the sequence in real unitary space and basic operations on sequences we prove several theorems which will be used in our further considerations.
  13. Jan Popiolek. Introduction to Banach and Hilbert Spaces -- Part II, Formalized Mathematics 2(4), pages 517-521, 1991. MML Identifier: BHSP_2
    Summary: A continuation of \cite{BHSP_1.ABS}. It contains the definitions of the convergent sequence and limit of the sequence. The convergence with respect to the norm and the distance is also introduced. Last part of this article is devoted to the following concepts: ball, closed ball and sphere.
  14. Jan Popiolek. Introduction to Banach and Hilbert Spaces -- Part III, Formalized Mathematics 2(4), pages 523-526, 1991. MML Identifier: BHSP_3
    Summary: The article is a continuation of \cite{BHSP_1.ABS} and of \cite{BHSP_2.ABS}. First we define the following concepts: the Cauchy sequence, the bounded sequence and the subsequence. The last part of this article contains definitions of the complete space and the Hilbert space.
  15. Czeslaw Bylinski. Category Ens, Formalized Mathematics 2(4), pages 527-533, 1991. MML Identifier: ENS_1
    Summary: If $V$ is any non-empty set of sets, we define $\hbox{\bf Ens}_V$ to be the category with the objects of all sets $X \in V$, morphisms of all mappings from $X$ into $Y$, with the usual composition of mappings. By a mapping we mean a triple $\langle X,Y,f \rangle$ where $f$ is a function from $X$ into $Y$. The notations and concepts included corresponds to that presented in \cite{SEMAD}, \cite{MacLane:1}. We also introduce representable functors to illustrate properties of the category {\bf Ens}.
  16. Andrzej Trybulec. A Borsuk Theorem on Homotopy Types, Formalized Mathematics 2(4), pages 535-545, 1991. MML Identifier: BORSUK_1
    Summary: We present a Borsuk's theorem published first in \cite{BORSUK:3} (compare also \cite[pages 119--120]{BORSUK:2}). It is slightly generalized, the assumption of the metrizability is omitted. We introduce concepts needed for the formulation and the proofs of the theorems on upper semi-continuous decompositions, retracts, strong deformation retract. However, only those facts that are necessary in the proof have been proved.
  17. Grzegorz Bancerek. Cartesian Product of Functions, Formalized Mathematics 2(4), pages 547-552, 1991. MML Identifier: FUNCT_6
    Summary: A supplement of \cite{CARD_3.ABS} and \cite{FUNCT_5.ABS}, i.e. some useful and explanatory properties of the product and also the curried and uncurried functions are shown. Besides, the functions yielding functions are considered: two different products and other operation of such functions are introduced. Finally, two facts are presented: quasi-distributivity of the power of the set to other one w.r.t. the union ($X^{\biguplus_{x}f(x)} \approx \prod_{x}X^{f(x)}$) and quasi-distributivity of the product w.r.t. the raising to the power ($\prod_{x}{f(x)^X} \approx (\prod_{x}f(x))^X$).
  18. Alicia de la Cruz. Introduction to Modal Propositional Logic, Formalized Mathematics 2(4), pages 553-558, 1991. MML Identifier: MODAL_1
    Summary:
  19. Alicia de la Cruz. Totally Bounded Metric Spaces, Formalized Mathematics 2(4), pages 559-562, 1991. MML Identifier: TBSP_1
    Summary:
  20. Michal Muzalewski. Categories of Groups, Formalized Mathematics 2(4), pages 563-571, 1991. MML Identifier: GRCAT_1
    Summary: We define the category of groups and its subcategories: category of Abelian groups and category of groups with the operator of $1/2$. The carriers of the groups are included in a universum. The universum is a parameter of the categories.
  21. Wojciech A. Trybulec, Michal J. Trybulec. Homomorphisms and Isomorphisms of Groups. Quotient Group, Formalized Mathematics 2(4), pages 573-578, 1991. MML Identifier: GROUP_6
    Summary: Quotient group, homomorphisms and isomorphisms of groups are introduced. The so called isomorphism theorems are proved following \cite{KARGAP:1}.
  22. Michal Muzalewski. Rings and Modules -- Part II, Formalized Mathematics 2(4), pages 579-585, 1991. MML Identifier: MOD_2
    Summary: We define the trivial left module, morphism of left modules and the field $Z_3$. We prove some elementary facts.
  23. Michal Muzalewski. Free Modules, Formalized Mathematics 2(4), pages 587-589, 1991. MML Identifier: MOD_3
    Summary: We define free modules and prove that every left module over Skew-Field is free.
  24. Jaroslaw Zajkowski. Oriented Metric-Affine Plane -- Part I, Formalized Mathematics 2(4), pages 591-597, 1991. MML Identifier: ANALORT
    Summary: We present (in Euclidean and Minkowskian geometry) definitions and some properties of oriented orthogonality relation. Next we consider consistence Euclidean space and consistence Minkowskian space.
  25. Agata Darmochwal. The Euclidean Space, Formalized Mathematics 2(4), pages 599-603, 1991. MML Identifier: EUCLID
    Summary: The general definition of Euclidean Space.
  26. Agata Darmochwal, Yatsuka Nakamura. Metric Spaces as Topological Spaces -- Fundamental Concepts, Formalized Mathematics 2(4), pages 605-608, 1991. MML Identifier: TOPMETR
    Summary: Some notions connected with metric spaces and the relationship between metric spaces and topological spaces. Compactness of topological spaces is transferred for the case of metric spaces \cite{KELL55}. Some basic theorems about translations of topological notions for metric spaces are proved. One-dimensional topological space ${\Bbb R^1}$ is introduced, too.
  27. Agata Darmochwal, Yatsuka Nakamura. Heine--Borel's Covering Theorem, Formalized Mathematics 2(4), pages 609-610, 1991. MML Identifier: HEINE
    Summary: Heine--Borel's covering theorem, also known as Borel--Lebesgue theorem (\cite{BOURBAKI}), is proved. Some useful theorems about real inequalities, intervals, sequences and notion of power sequence which are necessary for the theorem are also proved.
  28. Yatsuka Nakamura, Agata Darmochwal. Some Facts about Union of Two Functions and Continuity of Union of Functions, Formalized Mathematics 2(4), pages 611-613, 1991. MML Identifier: TOPMETR2
    Summary: Proofs of two theorems connected with union of any two functions and the proofs of two theorems about continuity of the union of two continuous functions between topogical spaces. The theorem stating that union of two subsets of $R^2$, which are homeomorphic to unit interval and have only one terminal joined point is also homeomorphic to unit interval is proved, too.