Formalized Mathematics    (ISSN 0777-4028)
Volume 1, Number 4 (1990): pdf, ps, dvi.
  1. Henryk Oryszczyszyn, Krzysztof Prazmowski. Classical Configurations in Affine Planes, Formalized Mathematics 1(4), pages 625-633, 1990. MML Identifier: AFF_2
    Summary: The classical sequence of implications which hold between Desargues and Pappus Axioms is proved. Formally Minor and Major Desargues Axiom (as suitable properties -- predicates -- of an affine plane) together with all its indirect forms are introduced; the same procedure is applied to Pappus Axioms. The so called Trapezium Desargues Axiom is also considered.
  2. Eugeniusz Kusak, Henryk Oryszczyszyn, Krzysztof Prazmowski. Affine Localizations of Desargues Axiom, Formalized Mathematics 1(4), pages 635-642, 1990. MML Identifier: AFF_3
    Summary: Several affine localizations of Major Desargues Axiom together with its indirect forms are introduced. Logical relationships between these formulas and between them and the classical Desargues Axiom are demonstrated.
  3. Czeslaw Bylinski. Binary Operations Applied to Finite Sequences, Formalized Mathematics 1(4), pages 643-649, 1990. MML Identifier: FINSEQOP
    Summary: The article contains some propositions and theorems related to \cite{FUNCOP_1.ABS} and \cite{FINSEQ_2.ABS}. The notions introduced in \cite{FUNCOP_1.ABS} are extended to finite sequences. A number of additional propositions related to this notions are proved. There are also proved some properties of distributive operations and unary operations. The notation and propositions for inverses are introduced.
  4. Czeslaw Bylinski. Semigroup operations on finite subsets, Formalized Mathematics 1(4), pages 651-656, 1990. MML Identifier: SETWOP_2
    Summary: A continuation of \cite{SETWISEO.ABS}. The propositions and theorems proved in \cite{SETWISEO.ABS} are extended to finite sequences. Several additional theorems related to semigroup operations of functions not included in \cite{SETWISEO.ABS} are proved. The special notation for operations on finite sequences is introduced.
  5. Wojciech Skaba. The Collinearity Structure, Formalized Mathematics 1(4), pages 657-659, 1990. MML Identifier: COLLSP
    Summary: The text includes basic axioms and theorems concerning the collinearity structure based on Wanda Szmielew \cite{SZMIELEW:1}, pp. 18--20. Collinearity is defined as a relation on Cartesian product $\mizleftcart S, S, S \mizrightcart$ of set $S$. The basic text is preceeded with a few auxiliary theorems (e.g: ternary relation). Then come the two basic axioms of the collinearity structure: A1.1.1 and A1.1.2 and a few theorems. Another axiom: Aks dim, which states that there exist at least 3 non-collinear points, excludes the trivial structures (i.e. pairs $\llangle S, \mizleftcart S, S, S \mizrightcart\rrangle$). Following it the notion of a line is included and several additional theorems are appended.
  6. Czeslaw Bylinski. The Sum and Product of Finite Sequences of Real Numbers, Formalized Mathematics 1(4), pages 661-668, 1990. MML Identifier: RVSUM_1
    Summary: Some operations on the set of $n$-tuples of real numbers are introduced. Addition, difference of such $n$-tuples, complement of a $n$-tuple and multiplication of these by real numbers are defined. In these definitions more general properties of binary operations applied to finite sequences from \cite{FINSEQOP.ABS} are used. Then the fact that certain properties are satisfied by those operations is demonstrated directly from \cite{FINSEQOP.ABS}. Moreover some properties can be recognized as being those of real vector space. Multiplication of $n$-tuples of real numbers and square power of $n$-tuple of real numbers using for notation of some properties of finite sums and products of real numbers are defined, followed by definitions of the finite sum and product of $n$-tuples of real numbers using notions and properties introduced in \cite{SETWOP_2.ABS}. A number of propositions and theorems on sum and product of finite sequences of real numbers are proved. As additional properties there are proved some properties of real numbers and set representations of binary operations on real numbers.
  7. Czeslaw Bylinski. A Classical First Order Language, Formalized Mathematics 1(4), pages 669-676, 1990. MML Identifier: CQC_LANG
    Summary: The aim is to construct a language for the classical predicate calculus. The language is defined as a subset of the language constructed in \cite{QC_LANG1.ABS}. Well-formed formulas of this language are defined and some usual connectives and quantifiers of \cite{QC_LANG1.ABS}, \cite{QC_LANG2.ABS} are accordingly. We prove inductive and definitional schemes for formulas of our language. Substitution for individual variables in formulas of the introduced language is defined. This definition is borrowed from \cite{POGORZELSKI.1975}. For such purpose some auxiliary notation and propositions are introduced.
  8. Henryk Oryszczyszyn, Krzysztof Prazmowski, Malgorzata Prazmowska. Classical and Non--classical Pasch Configurations in Ordered Affine Planes, Formalized Mathematics 1(4), pages 677-680, 1990. MML Identifier: PASCH
    Summary: Several configuration axioms, which are commonly called in the literature ``Pasch Axioms" are introduced; three of them were investigated by Szmielew and concern invariantability of the betweenness relation under parallel projections, and two other were introduced by Tarski. It is demonstrated that they all are consequences of the trapezium axiom, adopted to characterize ordered affine spaces.
  9. Marek Chmur. The Lattice of Real Numbers. The Lattice of Real Functions, Formalized Mathematics 1(4), pages 681-684, 1990. MML Identifier: REAL_LAT
    Summary: A proof of the fact, that $\llangle {\Bbb R}, {\rm max}, {\rm min} \rrangle$ is a lattice (real lattice). Some basic properties (real lattice is distributive and modular) of it are proved. The same is done for the set ${\Bbb R}^A$ with operations: max($f(A)$) and min($f(A)$), where ${\Bbb R}^A$ means the set of all functions from $A$ (being non-empty set) to $\Bbb R$, $f$ is just such a function.
  10. Grzegorz Lewandowski, Krzysztof Prazmowski. A Construction of an Abstract Space of Congruence of Vectors, Formalized Mathematics 1(4), pages 685-688, 1990. MML Identifier: TDGROUP
    Summary: In the class of abelian groups a subclass of two-divisible-groups is singled out, and in the latter, a subclass of uniquely-two-divisible-groups. With every such a group a special geometrical structure, more precisely the structure of ``congruence of vectors'' is correlated. The notion of ``affine vector space'' (denoted by AffVect) is introduced. This term is defined by means of suitable axiom system. It is proved that every structure of the congruence of vectors determined by a non trivial uniquely two divisible group is a affine vector space.
  11. Agata Darmochwal. A First--Order Predicate Calculus, Formalized Mathematics 1(4), pages 689-695, 1990. MML Identifier: CQC_THE1
    Summary: A continuation of \cite{CQC_LANG.ABS}, with an axiom system of first-order predicate theory. The consequence Cn of a set of formulas $X$ is defined as the intersection of all theories containing $X$ and some basic properties of it has been proved (monotonicity, idempotency, completeness etc.). The notion of a proof of given formula is also introduced and it is shown that ${\rm Cn} X = \{~p: p $ has a proof w.r.t. $ X\}$. First 14 theorems are rather simple facts. I just wanted them to be included in the data base.
  12. Jaroslaw Kotowicz. Partial Functions from a Domain to a Domain, Formalized Mathematics 1(4), pages 697-702, 1990. MML Identifier: PARTFUN2
    Summary: The value of a partial function from a domain to a domain and a inverse partial function are introduced. The value and inverse function were defined in the article \cite{FUNCT_1.ABS}, but new definitions are introduced. The basic properties of the value, the inverse partial function, the identity partial function, the composition of partial functions, the $1{-}1$ partial function, the restriction of a partial function, the image, the inverse image and the graph are proved. Constant partial functions are introduced, too.
  13. Jaroslaw Kotowicz. Partial Functions from a Domain to the Set of Real Numbers, Formalized Mathematics 1(4), pages 703-709, 1990. MML Identifier: RFUNCT_1
    Summary: Basic operations in the set of partial functions which map a domain to the set of all real numbers are introduced. They include adition, subtraction, multiplication, division, multipication by a real number and also module. Main properties of these operations are proved. A definition of the partial function bounded on a set (bounded below and bounded above) is presented. There are theorems showing the laws of conservation of totality and boundedness for operations of partial functions. The characteristic function of a subset of a domain as a partial function is redefined and a few properties are proved.
  14. Grzegorz Bancerek. Increasing and Continuous Ordinal Sequences, Formalized Mathematics 1(4), pages 711-714, 1990. MML Identifier: ORDINAL4
    Summary: Concatenation of two ordinal sequences, the mode of all ordinals belonging to a universe and the mode of sequences of them with length equal to the rank of the universe are introduced. Besides, the increasing and continuous transfinite sequences, the limes of ordinal sequences and the power of ordinals, and the fact that every increasing and continuous transfinite sequence has critical numbers (fixed points) are discussed.
  15. Henryk Oryszczyszyn, Krzysztof Prazmowski. Transformations in Affine Spaces, Formalized Mathematics 1(4), pages 715-723, 1990. MML Identifier: TRANSGEO
    Summary: Two classes of bijections of its point universe are correlated with every affine structure. The first class consists of the transformations, called formal isometries, which map every segment onto congruent segment, the second class consists of the automorphisms of such a structure. Each of these two classes of bijections forms a group for a given affine structure, if it satisfies a very weak axiom system (models of these axioms are called congruence spaces); formal isometries form a normal subgroup in the group of automorphism. In particular ordered affine spaces and affine spaces are congruence spaces; therefore formal isometries of these structures can be considered. They are called positive dilatations and dilatations, resp. For convenience the class of negative dilatations, transformations which map every ``vector" onto parallel ``vector", but with opposite sense, is singled out. The class of translations is distinguished as well. Basic facts concerning all these types of transformations are established, like rigidity, decomposition principle, introductory group-theoretical properties. At the end collineations of affine spaces and their properties are investigated; for affine planes it is proved that the class of collineations coincides with the class of bijections preserving lines.
  16. Czeslaw Bylinski. Subcategories and Products of Categories, Formalized Mathematics 1(4), pages 725-732, 1990. MML Identifier: CAT_2
    Summary: The {\it subcategory} of a category and product of categories is defined. The {\it inclusion functor} is the injection (inclusion) map $E \atop \hookrightarrow$ which sends each object and each arrow of a Subcategory $E$ of a category $C$ to itself (in $C$). The inclusion functor is faithful. {\it Full subcategories} of $C$, that is, those subcategories $E$ of $C$ such that $\hbox{Hom}_E(a,b) = \hbox{Hom}_C(b,b)$ for any objects $a,b$ of $E$, are defined. A subcategory $E$ of $C$ is full when the inclusion functor $E \atop \hookrightarrow$ is full. The proposition that a full subcategory is determined by giving the set of objects of a category is proved. The product of two categories $B$ and $C$ is constructed in the usual way. Moreover, some simple facts on $bifunctors$ (functors from a product category) are proved. The final notions in this article are that of projection functors and product of two functors ({\it complex} functors and {\it product} functors).
  17. Edmund Woronowicz. Many--Argument Relations, Formalized Mathematics 1(4), pages 733-737, 1990. MML Identifier: MARGREL1
    Summary: Definitions of relations based on finite sequences. The arity of relation, the set of logical values {\it Boolean} consisting of {\it false} and {\it true} and the operations of negation and conjunction on them are defined.
  18. Edmund Woronowicz. Interpretation and Satisfiability in the First Order Logic, Formalized Mathematics 1(4), pages 739-743, 1990. MML Identifier: VALUAT_1
    Summary: The main notion discussed is satisfiability. Interpretation and some auxiliary concepts are also introduced.
  19. Andrzej Ndzusiak. Probability, Formalized Mathematics 1(4), pages 745-749, 1990. MML Identifier: PROB_2
    Summary: Some further theorems concerning probability, among them the equivalent definition of probability are discussed, followed by notions of independence of events and conditional probability and basic theorems on them.
  20. Henryk Oryszczyszyn, Krzysztof Prazmowski. Translations in Affine Planes, Formalized Mathematics 1(4), pages 751-753, 1990. MML Identifier: TRANSLAC
    Summary: Connections between Minor Desargues Axiom and the transitivity of translation groups are investigated. A formal proof of the theorem which establishes the equivalence of these two properties of affine planes is given. We also prove that, under additional requirement, the plane in question satisfies Fano Axiom; its translation group is uniquely two-divisible.
  21. Jan Popiolek. Introduction to Probability, Formalized Mathematics 1(4), pages 755-760, 1990. MML Identifier: RPR_1
    Summary: Definitions of Elementary Event and Event in any sample space $E$ are given. Next, the probability of an Event when $E$ is finite is introduced and some properties of this function are investigated. Last part of the paper is devoted to the conditional probability and essential properties of this function (Bayes Theorem).
  22. Wojciech Leonczuk, Krzysztof Prazmowski. A Construction of Analytical Projective Space, Formalized Mathematics 1(4), pages 761-766, 1990. MML Identifier: ANPROJ_1
    Summary: The collinearity structure denoted by Projec\-ti\-ve\-Spa\-ce(V) is correlated with a given vector space $V$ (over the field of Reals). It is a formalization of the standard construction of a projective space, where points are interpreted as equivalence classes of the relation of proportionality considered in the set of all non-zero vectors. Then the relation of collinearity corresponds to the relation of linear dependence of vectors. Several facts concerning vectors are proved, which correspond in this language to some classical axioms of projective geometry.
  23. Wojciech Leonczuk, Krzysztof Prazmowski. Projective Spaces -- Part I, Formalized Mathematics 1(4), pages 767-776, 1990. MML Identifier: ANPROJ_2
    Summary: In the class of all collinearity structures a subclass of (dimension free) projective spaces, defined by means of a suitable axiom system, is singled out. Whenever a real vector space V is at least 3-dimensional, the structure ProjectiveSpace(V) is a projective space in the above meaning. Some narrower classes of projective spaces are defined: Fano projective spaces, projective planes, and Fano projective planes. For any of the above classes an explicit axiom system is given, as well as an analytical example. There is also a construction a of 3-dimensional and a 4-dimensional real vector space; these are needed to show appropriate examples of projective spaces.
  24. Konrad Raczkowski, Pawel Sadowski. Topological Properties of Subsets in Real Numbers, Formalized Mathematics 1(4), pages 777-780, 1990. MML Identifier: RCOMP_1
    Summary: The following notions for real subsets are defined: open set, closed set, compact set, intervals and neighbourhoods. In the sequel some theorems involving above mentioned notions are proved.
  25. Jaroslaw Kotowicz. Properties of Real Functions, Formalized Mathematics 1(4), pages 781-786, 1990. MML Identifier: RFUNCT_2
    Summary: The list of theorems concerning properties of real sequences and functions is enlarged. (See e.g. \cite{SEQ_1.ABS}, \cite{SEQ_4.ABS}, \cite{RFUNCT_1.ABS}). The monotone real functions are introduced and their properties are discussed.
  26. Konrad Raczkowski, Pawel Sadowski. Real Function Continuity, Formalized Mathematics 1(4), pages 787-791, 1990. MML Identifier: FCONT_1
    Summary: The continuity of real functions is discussed. There is a function defined on some domain in real numbers which is continuous in a single point and on a subset of domain of the function. Main properties of real continuous functions are proved. Among them there is the Weierstra{\ss} Theorem. Algebraic features for real continuous functions are shown. Lipschitzian functions are introduced. The Lipschitz condition entails continuity.
  27. Jaroslaw Kotowicz, Konrad Raczkowski. Real Function Uniform Continuity, Formalized Mathematics 1(4), pages 793-795, 1990. MML Identifier: FCONT_2
    Summary: The uniform continuity for real functions is introduced. More theorems concerning continuous functions are given. (See \cite{FCONT_1.ABS}) The Darboux Theorem is exposed. Algebraic features for uniformly continuous functions are presented. Various facts, e.g., a continuous function on a compact set is uniformly continuous are proved.
  28. Konrad Raczkowski, Pawel Sadowski. Real Function Differentiability, Formalized Mathematics 1(4), pages 797-801, 1990. MML Identifier: FDIFF_1
    Summary: For a real valued function defined on its domain in real numbers the differentiability in a single point and on a subset of the domain is presented. The main elements of differential calculus are developed. The algebraic properties of differential real functions are shown.
  29. Jaroslaw Kotowicz, Konrad Raczkowski, Pawel Sadowski. Average Value Theorems for Real Functions of One Variable, Formalized Mathematics 1(4), pages 803-805, 1990. MML Identifier: ROLLE
    Summary: Three basic theorems in differential calculus of one variable functions are presented: Rolle Theorem, Lagrange Theorem and Cauchy Theorem. There are also direct conclusions.