Formalized Mathematics    (ISSN 0777-4028)
Volume 2, Number 2 (1991): pdf, ps, dvi.
  1. Stanislawa Kanas, Jan Stankiewicz. Metrics in Cartesian Product, Formalized Mathematics 2(2), pages 193-197, 1991. MML Identifier: METRIC_3
    Summary: A continuation of paper \cite{METRIC_1.ABS}. It deals with the method of creation of the distance in the Cartesian product of metric spaces. The distance of two points belonging to Cartesian product of metric spaces has been defined as sum 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.
  2. Adam Lecko, Mariusz Startek. Submetric Spaces -- Part I, Formalized Mathematics 2(2), pages 199-203, 1991. MML Identifier: SUB_METR
    Summary:
  3. Adam Lecko, Mariusz Startek. On Pseudometric Spaces, Formalized Mathematics 2(2), pages 205-211, 1991. MML Identifier: METRIC_2
    Summary:
  4. Konrad Raczkowski, Andrzej Ndzusiak. Real Exponents and Logarithms, Formalized Mathematics 2(2), pages 213-216, 1991. MML Identifier: POWER
    Summary: Definitions and properties of the following concepts: root, real exponent and logarithm. Also the number $e$ is defined.
  5. Eugeniusz Kusak, Wojciech Leonczuk. Hessenberg Theorem, Formalized Mathematics 2(2), pages 217-219, 1991. MML Identifier: HESSENBE
    Summary: We prove the Hessenberg theorem which states that every Pappian projective space is Desarguesian.
  6. Michal Muzalewski, Wojciech Skaba. Three-Argument Operations and Four-Argument Operations, Formalized Mathematics 2(2), pages 221-224, 1991. MML Identifier: MULTOP_1
    Summary: The article contains the definition of three- and four- argument operations. The article introduces also a few operation related schemes: {\it FuncEx3D}, {\it TriOpEx}, {\it Lambda3D}, {\it TriOpLambda}, {\it FuncEx4D}, {\it QuaOpEx}, {\it Lambda4D}, {\it QuaOpLambda}.
  7. Wojciech Leonczuk, Krzysztof Prazmowski. Incidence Projective Spaces, Formalized Mathematics 2(2), pages 225-232, 1991. MML Identifier: INCPROJ
    Summary: A basis for investigations on incidence projective spaces. With every projective space defined in terms of collinearity relation we associate the incidence structure consisting of points and of lines of the given space. We introduce general notion of projective space defined in terms of incidence and define several properties of such structures (like satisfability of the Desargues Axiom or conditions on the dimension).
  8. Barbara Konstanta, Urszula Kowieska, Grzegorz Lewandowski, Krzysztof Prazmowski. One-Dimensional Congruence of Segments, Basic Facts and Midpoint Relation, Formalized Mathematics 2(2), pages 233-235, 1991. MML Identifier: AFVECT01
    Summary: We study a theory of one-dimensional congruence of segments. The theory is characterized by a suitable formal axiom system; as a model of this system one can take the structure obtained from any weak directed geometrical bundle, with the congruence interpreted as in the case of ``classical" vectors. Preliminary consequences of our axiom system are proved, basic relations of maximal distance and of midpoint are defined, and several fundamental properties of them are established.
  9. Andrzej Trybulec. Algebra of Normal Forms, Formalized Mathematics 2(2), pages 237-242, 1991. MML Identifier: NORMFORM
    Summary: We mean by a normal form a finite set of ordered pairs of subsets of a fixed set that fulfils two conditions: elements of it consist of disjoint sets and element of it are incomparable w.r.t. inclusion. The underlying set corresponds to a set of propositional variables but it is arbitrary. The correspondents to a normal form of a formula, e.g. a disjunctive normal form is as follows. The normal form is the set of disjuncts and a disjunct is an ordered pair consisting of the sets of propositional variables that occur in the disjunct non-negated and negated. The requirement that the element of a normal form consists of disjoint sets means that contradictory disjuncts have been removed and the second condition means that the absorption law has been used to shorten the normal form. We construct a lattice $\langle {\Bbb N},\sqcup,\sqcap \rangle$, where $ a \sqcup b = \mu (a \cup b)$ and $a \sqcap b = \mu c$, $c$ being set of all pairs $\langle X_1 \cup Y_1, X_2 \cup Y_2 \rangle$, $\langle X_1, X_2 \rangle \in a$ and $\langle Y_1,Y_2 \rangle \in b$, which consist of disjoiny sets. $\mu a$ denotes here the set of all minimal, w.r.t. inclusion, elements of $a$. We prove that the lattice of normal forms over a set defined in this way is distributive and that $\emptyset$ is the minimal element of it.
  10. Michal Muzalewski, Leslaw W. Szczerba. Ordered Rings -- Part I, Formalized Mathematics 2(2), pages 243-245, 1991. MML Identifier: O_RING_1
    Summary: This series of papers is devoted to the notion of the ordered ring, and one of its most important cases: the notion of ordered field. It follows the results of \cite{SZMIELEW:1}. The idea of the notion of order in the ring is based on that of positive cone i.e. the set of positive elements. Positive cone has to contain at least squares of all elements, and be closed under sum and product. Therefore the key notions of this theory are that of square, sum of squares, product of squares, etc. and finally elements generated from squares by means of sums and products. Part I contains definitions of all those key notions and inclusions between them.
  11. Michal Muzalewski, Leslaw W. Szczerba. Ordered Rings -- Part II, Formalized Mathematics 2(2), pages 247-249, 1991. MML Identifier: O_RING_2
    Summary: This series of papers is devoted to the notion of the ordered ring, and one of its most important cases: the notion of ordered field. It follows the results of \cite{SZMIELEW:1}. The idea of the notion of order in the ring is based on that of positive cone i.e. the set of positive elements. Positive cone has to contain at least squares of all elements, and has to be closed under sum and product. Therefore the key notions of this theory are that of square, sum of squares, product of squares, etc. and finally elements generated from squares by means of sums and products. Part II contains classification of sums of such elements.
  12. Michal Muzalewski, Leslaw W. Szczerba. Ordered Rings -- Part III, Formalized Mathematics 2(2), pages 251-253, 1991. MML Identifier: O_RING_3
    Summary: This series of papers is devoted to the notion of the ordered ring, and one of its most important cases: the notion of ordered field. It follows the results of \cite{SZMIELEW:1}. The idea of the notion of order in the ring is based on that of positive cone i.e. the set of positive elements. Positive cone has to contain at least squares of all elements, and be closed under sum and product. Therefore the key notions of this theory are that of square, sum of squares, product of squares, etc. and finally elements generated from squares by means of sums and products. Part III contains classification of products of such elements.
  13. Michal Muzalewski, Wojciech Skaba. N-Tuples and Cartesian Products for n$=$5, Formalized Mathematics 2(2), pages 255-258, 1991. MML Identifier: MCART_2
    Summary: This article defines ordered $n$-tuples, projections and Cartesian products for $n=5$. We prove many theorems concerning the basic properties of the $n$-tuples and Cartesian products that may be utilized in several further, more challenging applications. A few of these theorems are a strightforward consequence of the regularity axiom. The article originated as an upgrade of the article \cite{MCART_1.ABS}.
  14. Michal Muzalewski, Wojciech Skaba. Ternary Fields, Formalized Mathematics 2(2), pages 259-261, 1991. MML Identifier: ALGSTR_3
    Summary: This article contains part 3 of the set of papers concerning the theory of algebraic structures, based on the book \cite[pp. 13--15]{SZMIELEW:1} (pages 6--8 for English edition).\par First the basic structure $\langle F, 0, 1, T\rangle$ is defined, where $T$ is a ternary operation on $F$ (three argument operations have been introduced in the article \cite{MULTOP_1.ABS}. Following it, the basic axioms of a ternary field are displayed, the mode is defined and its existence proved. The basic properties of a ternary field are also contemplated there.}
  15. Jozef Bialas. The $\sigma$-additive Measure Theory, Formalized Mathematics 2(2), pages 263-270, 1991. MML Identifier: MEASURE1
    Summary: The article contains definition and basic properties of $\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 \cite{SIKORSKI:1}. We present definitions of $\sigma$-field of sets, $\sigma$-additive measure, measurable sets, measure zero sets and the basic theorems describing relationships between the notion mentioned above. The work is the third part of the series of articles concerning the Lebesgue measure theory.
  16. Eugeniusz Kusak, Wojciech Leonczuk. Incidence Projective Space (a reduction theorem in a plane), Formalized Mathematics 2(2), pages 271-274, 1991. MML Identifier: PROJRED1
    Summary: The article begins with basic facts concerning arbitrary projective spaces. Further we are concerned with Fano projective spaces (we prove it has rank at least four). Finally we restrict ourselves to Desarguesian planes; we define the notion of perspectivity and we prove the reduction theorem for projectivities with concurrent axes.
  17. Michal Muzalewski, Wojciech Skaba. Groups, Rings, Left- and Right-Modules, Formalized Mathematics 2(2), pages 275-278, 1991. MML Identifier: MOD_1
    Summary: The notion of group was defined as a group structure introduced in the article \cite{VECTSP_1.ABS}. The article contains the basic properties of groups, rings, left- and right-modules of an associative ring.
  18. Michal Muzalewski, Wojciech Skaba. Finite Sums of Vectors in Left Module over Associative Ring, Formalized Mathematics 2(2), pages 279-282, 1991. MML Identifier: LMOD_1
    Summary:
  19. Michal Muzalewski, Wojciech Skaba. Submodules and Cosets of Submodules in Left Module over Associative Ring, Formalized Mathematics 2(2), pages 283-287, 1991. MML Identifier: LMOD_2
    Summary:
  20. Michal Muzalewski, Wojciech Skaba. Operations on Submodules in Left Module over Associative Ring, Formalized Mathematics 2(2), pages 289-293, 1991. MML Identifier: LMOD_3
    Summary:
  21. Michal Muzalewski, Wojciech Skaba. Linear Combinations in Left Module over Associative Ring, Formalized Mathematics 2(2), pages 295-300, 1991. MML Identifier: LMOD_4
    Summary:
  22. Michal Muzalewski, Wojciech Skaba. Linear Independence in Left Module over Domain, Formalized Mathematics 2(2), pages 301-303, 1991. MML Identifier: LMOD_5
    Summary: Notion of a submodule generated by a set of vectors and linear independence of a set of vectors. A few theorems originated as a generalization of the theorems from the article \cite{VECTSP_7.ABS}.
  23. Jan Popiolek, Andrzej Trybulec. Calculus of Propositions, Formalized Mathematics 2(2), pages 305-307, 1991. MML Identifier: PROCAL_1
    Summary: Continues the analysis of classical language of first order (see \cite{QC_LANG1.ABS}, \cite{QC_LANG2.ABS}, \cite{CQC_LANG.ABS}, \cite{CQC_THE1.ABS}, \cite{LUKASI_1.ABS}). Three connectives: truth, negation and conjuction are primary (see \cite{QC_LANG1.ABS}). The others (alternative, implication and equivalence) are defined with respect to them (see \cite{QC_LANG2.ABS}). We prove some important tautologies of the calculus of propositions. Most of them are given as the axioms of classical logical calculus (see \cite{GRZEG1}). In the last part of our article we give some basic rules of inference.
  24. Agata Darmochwal. Calculus of Quantifiers. Deduction Theorem, Formalized Mathematics 2(2), pages 309-312, 1991. MML Identifier: CQC_THE2
    Summary: Some tautologies of the Classical Quantifier Calculus. The deduction theorem is also proved.