Formalized Mathematics    (ISSN 0777-4028)
Volume 2, Number 5 (1991): pdf, ps, dvi.
  1. Agata Darmochwal, Yatsuka Nakamura. The Topological Space $\calE^2_\rmT$. Arcs, Line Segments and Special Polygonal Arcs, Formalized Mathematics 2(5), pages 617-621, 1991. MML Identifier: TOPREAL1
    Summary: The notions of arc and line segment are introduced in two-dimensional topological real space ${\cal E}^2_{\rm T}$. Some basic theorems for these notions are proved. Using line segments, the notion of special polygonal arc is defined. It has been shown that any special polygonal arc is homeomorphic to unit interval ${\Bbb I}$. The notion of unit square $\square_{\cal E^{2}_{\rm T}}$ has been also introduced and some facts about it have been proved.
  2. Dariusz Surowik. Cyclic Groups and Some of Their Properties -- Part I, Formalized Mathematics 2(5), pages 623-627, 1991. MML Identifier: GR_CY_1
    Summary: Some properties of finite groups are proved. The notion of cyclic group is defined next, some cyclic groups are given, for example the group of integers with addition operations. Chosen properties of cyclic groups are proved next.
  3. Andrzej Trybulec. Isomorphisms of Categories, Formalized Mathematics 2(5), pages 629-634, 1991. MML Identifier: ISOCAT_1
    Summary: We continue the development of the category theory basically following \cite{SEMAD} (compare also \cite{MacLane:1}). We define the concept of isomorphic categories and prove basic facts related, e.g. that the Cartesian product of categories is associative up to the isomorphism. We introduce the composition of a functor and a transformation, and of transformation and a functor, and afterwards we define again those concepts for natural transformations. Let us observe, that we have to duplicate those concepts because of the permissiveness: if a functor $F$ is not naturally transformable to $G$, then natural transformation from $F$ to $G$ has no fixed meaning, hence we cannot claim that the composition of it with a functor as a transformation results in a natural transformation. We define also the so called horizontal composition of transformations (\cite{SEMAD}, p.~140, exercise {\bf 4}.{\bf 2},{\bf 5}(C)) and prove {\em interchange law} (\cite{MacLane:1}, p.44). We conclude with the definition of equivalent categories.
  4. Agata Darmochwal, Andrzej Trybulec. Similarity of Formulae, Formalized Mathematics 2(5), pages 635-642, 1991. MML Identifier: CQC_SIM1
    Summary: The main objective of the paper is to define the concept of the similarity of formulas. We mean by similar formulas the two formulas that differs only in the names of bound variables. Some authors (compare \cite{RASIOWA-SIKOR}) call such formulas {\em congruent}. We use the word {\em similar} following \cite{POGO:1}, \cite{POGO:2}, \cite{POGORZELSKI.1975}. The concept is unjustfully neglected in many logical handbooks. It is intuitively quite clear, however the exact definition is not simple. As far as we know, only W.A.~Pogorzelski and T.~Prucnal \cite{POGORZELSKI.1975} define it in the precise way. We follow basically the Pogorzelski's definition (compare \cite{POGO:1}). We define renumeration of bound variables and we say that two formulas are similar if after renumeration are equal. Therefore we need a rule of chosing bound variables independent of the original choice. Quite obvious solution is to use consecutively variables $x_{k+1},x_{k+2},\dots$, where $k$ is the maximal index of free variable occurring in the formula. Therefore after the renumeration we get the new formula in which different quantifiers bind different variables. It is the reason that the result of renumeration applied to a formula $\varphi$ we call {\em $\varphi$ with variables separated}.
  5. Michal Muzalewski. Category of Rings, Formalized Mathematics 2(5), pages 643-648, 1991. MML Identifier: RINGCAT1
    Summary: We define the category of non-associative rings. The carriers of the rings are included in a universum. The universum is a parameter of the category.
  6. Michal Muzalewski. Category of Left Modules, Formalized Mathematics 2(5), pages 649-652, 1991. MML Identifier: MODCAT_1
    Summary: We define the category of left modules over an associative ring. The carriers of the modules are included in a universum. The universum is a parameter of the category.
  7. Ewa Burakowska, Beata Madras. Real Function One-Side Differentiability, Formalized Mathematics 2(5), pages 653-656, 1991. MML Identifier: FDIFF_3
    Summary: We define real function one-side differentiability and one-side continuity. Main properties of one-side differentiability function are proved. Connections between one-side differential and differential real function at the point are demonstrated.
  8. Stanislawa Kanas, Adam Lecko. Sequences in Metric Spaces, Formalized Mathematics 2(5), pages 657-661, 1991. MML Identifier: METRIC_6
    Summary: Sequences in metric spaces are defined. The article contains definitions of bounded, convergent, Cauchy sequences. The subsequences are introduced too. Some theorems concerning sequences are proved.
  9. Agata Darmochwal, Yatsuka Nakamura. The Topological Space $\calE^2_\rmT$. Simple Closed Curves, Formalized Mathematics 2(5), pages 663-664, 1991. MML Identifier: TOPREAL2
    Summary: Continuation of \cite{TOPREAL1.ABS}. The fact that the unit square is compact is shown in the beginning of the article. Next the notion of simple closed curve is introduced. It is proved that any simple closed curve can be divided into two independent parts which are homeomorphic to unit interval ${\Bbb I}$.
  10. Zbigniew Karno. Separated and Weakly Separated Subspaces of Topological Spaces, Formalized Mathematics 2(5), pages 665-674, 1991. MML Identifier: TSEP_1
    Summary: A new concept of weakly separated subsets and subspaces of topological spaces is described in Mizar formalizm. Based on \cite{KURAT:2}, in comparison with the notion of separated subsets (subspaces), some properties of such subsets (subspaces) are discussed. Some necessary facts concerning closed subspaces, open subspaces and the union and the meet of two subspaces are also introduced. To present the main theorems we first formulate basic definitions. Let $X$ be a topological space. Two subsets $A_1$ and $A_2$ of $X$ are called {\em weakly separated} if $A_1 \setminus A_2$ and $A_2 \setminus A_1$ are separated. Two subspaces $X_{1}$ and $X_{2}$ of $X$ are called {\em weakly separated} if their carriers are weakly separated. The following theorem contains a useful characterization of weakly separated subsets in the special case when $A_{1} \cup A_{2}$ is equal to the carrier of $X$. {\em $A_{1}$ and $A_{2}$ are weakly separated iff there are such subsets of $X$, $C_{1}$ and $C_{2}$ closed (open) and $C$ open (closed, respectively), that $A_{1} \cup A_{2} = C_{1} \cup C_{2} \cup C$, $C_{1} \subset A_{1}$, $C_{2} \subset A_{2}$ and $C \subset A_{1} \cap A_{2}$}. Next theorem divided into two parts contains similar characterization of weakly separated subspaces in the special case when the union of $X_1$ and $X_2$ is equal to $X$. {\em If $X_{1}$ meets $X_{2}$, then $X_1$ and $X_2$ are weakly separated iff either $X_{1}$ is a subspace of $X_2$ or $X_2$ is a subspace of $X_{1}$ or there are such open (closed) subspaces $Y_1$ and $Y_2$ of $X$ that $Y_1$ is a subspace of $X_1$ and $Y_2$ is a subspace of $X_2$ and either $X$ is equal to the union of $Y_1$ and $Y_2$ or there is a(n) closed (open, respectively) subspace $Y$ of $X$ being a subspace of the meet of $X_1$ and $X_2$ and with the property that $X$ is the union of all $Y_1$, $Y_2$ and $Y$}. {\em If $X_1$ misses $X_{2}$, then $X_1$ and $X_2$ are weakly separated iff $X_1$ and $X_2$ are open (closed) subspaces of $X$}. Moreover, the following simple characterization of separated subspaces by means of weakly separated ones is obtained. {\em $X_1$ and $X_2$ are separated iff there are weakly separated subspaces $Y_1$ and $Y_2$ of $X$ such that $X_1$ is a subspace of $Y_1$, $X_2$ is a subspace of $Y_2$ and either $Y_1$ misses $Y_2$ or the meet of $Y_1$ and $Y_2$ misses the union of $X_1$ and $X_2$}.
  11. Malgorzata Korolkiewicz. The de l'Hospital Theorem, Formalized Mathematics 2(5), pages 675-678, 1991. MML Identifier: L'HOSPIT
    Summary:
  12. Grzegorz Bancerek, Agata Darmochwal. Comma Category, Formalized Mathematics 2(5), pages 679-681, 1991. MML Identifier: COMMACAT
    Summary: Comma category of two functors is introduced.
  13. Patricia L. Carlson, Grzegorz Bancerek. Context-Free Grammar -- Part 1, Formalized Mathematics 2(5), pages 683-687, 1991. MML Identifier: LANG1
    Summary: The concept of context-free grammar and of derivability in grammar are introduced. Moreover, the language (set of finite sequences of symbols) generated by grammar and some grammars are defined. The notion convenient to prove facts on language generated by grammar with exchange of symbols on grammar of union and concatenation of languages is included.
  14. Jozef Bialas. Completeness of the $\sigma$-Additive Measure. Measure Theory, Formalized Mathematics 2(5), pages 689-693, 1991. MML Identifier: MEASURE3
    Summary: Definitions and basic properties of a $\sigma$-additive, non-negative 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 \cite{SIKORSKI:1}. The article includes the text being a continuation of the paper \cite{MEASURE2.ABS}. Some theorems concerning basic properties of a $\sigma$-additive measure and completeness of the measure are proved.
  15. Elzbieta Kraszewska, Jan Popiolek. Series in Banach and Hilbert Spaces, Formalized Mathematics 2(5), pages 695-699, 1991. MML Identifier: BHSP_4
    Summary: In \cite{SERIES_1.ABS} the series of real numbers were investigated. The introduction to Banach and Hilbert spaces (\cite{BHSP_1.ABS}, \cite{BHSP_2.ABS},\cite{BHSP_3.ABS}), enables us to arrive at the concept of series in Hilbert space. We start with the notions: partial sums of series, sum and $n$-th sum of series, convergent series (summable series), absolutely convergent series. We prove some basic theorems: the necessary condition for a series to converge, Weierstrass' test, d'Alembert's test, Cauchy's test.
  16. Czeslaw Bylinski. Products and Coproducts in Categories, Formalized Mathematics 2(5), pages 701-709, 1991. MML Identifier: CAT_3
    Summary: A product and coproduct in categories are introduced. The concepts included correspond to that presented in \cite{SEMAD}.
  17. Katarzyna Jankowska. Transpose Matrices and Groups of Permutations, Formalized Mathematics 2(5), pages 711-717, 1991. MML Identifier: MATRIX_2
    Summary: Some facts concerning matrices with dimension $2\times 2$ are shown. Upper and lower triangular matrices, and operation of deleting rows and columns in a matrix are introduced. Besides, we deal with sets of permutations and the fact that all permutations of finite set constitute a finite group is proved. Some proofs are based on \cite{HUNGERFORD} and \cite{LANG}.
  18. Grzegorz Bancerek. Complete Lattices, Formalized Mathematics 2(5), pages 719-725, 1991. MML Identifier: LATTICE3
    Summary: In the first section the lattice of subsets of distinct set is introduced. The join and meet operations are, respectively, union and intersection of sets, and the ordering relation is inclusion. It is shown that this lattice is Boolean, i.e. distributive and complementary. The second section introduces the poset generated in a distinct lattice by its ordering relation. Besides, it is proved that posets which have l.u.b.'s and g.l.b.'s for every two elements generate lattices with the same ordering relations. In the last section the concept of complete lattice is introduced and discussed. Finally, the fact that the function $f$ from subsets of distinct set yielding elements of this set is a infinite union of some complete lattice, if $f$ yields an element $a$ for singleton $\{a\}$ and $f(f^\circ X) = f(\bigsqcup X)$ for every subset $X$, is proved. Some concepts and proofs are based on \cite{RASIOWA-SIKOR} and \cite{TRACZYK}.