Formalized Mathematics    (ISSN 0777-4028)
Volume 1, Number 3 (1990): pdf, ps, dvi.
  1. Bogdan Nowak, Slawomir Bialecki. Zermelo's Theorem, Formalized Mathematics 1(3), pages 431-432, 1990. MML Identifier: WELLSET1
    Summary: The article contains direct proof of Zermelo's theorem about the existence of a well ordering for any set and the lemma the proof depends on.
  2. Jozef Bialas. Group and Field Definitions, Formalized Mathematics 1(3), pages 433-439, 1990. MML Identifier: REALSET1
    Summary: The article contains exactly the same definitions of group and field as those in \cite{DIEUDONNE}. These definitions were prepared without the help of the definitions and properties of {\it Nat} and {\it Real} modes included in the MML. This is the first of a series of articles in which we are going to introduce the concept of the set of real numbers in a elementary axiomatic way.
  3. Konrad Raczkowski, Pawel Sadowski. Equivalence Relations and Classes of Abstraction, Formalized Mathematics 1(3), pages 441-444, 1990. MML Identifier: EQREL_1
    Summary: In this article we deal with the notion of equivalence relation. The main properties of equivalence relations are proved. Then we define the classes of abstraction determined by an equivalence relation. Finally, the connections between a partition of a set and an equivalence relation are presented. We introduce the following notation of modes: {\it Equivalence Relation, a partition}.
  4. Andrzej Trybulec, Czeslaw Bylinski. Some Properties of Real Numbers, Formalized Mathematics 1(3), pages 445-449, 1990. MML Identifier: SQUARE_1
    Summary: We define the following operations on real numbers: $max(x,y)$, $min(x,y)$, $x^2$, $\sqrt{x}$. We prove basic properties of introduced operations. A number of auxiliary theorems absent in \cite{REAL_1.ABS} and \cite{ABSVALUE.ABS} is proved.
  5. Grzegorz Bancerek. Connectives and Subformulae of the First Order Language, Formalized Mathematics 1(3), pages 451-458, 1990. MML Identifier: QC_LANG2
    Summary: In the article the development of the first order language defined in \cite{QC_LANG1.ABS} is continued. The following connectives are introduced: implication ($\Rightarrow$), disjunction ($\vee$), and equivalence ($\Leftrightarrow$). We introduce also the existential quantifier ($\exists$) and FALSUM. Some theorems on disjunctive, conditional, biconditional and existential formulae are proved and their selector functors are introduced. The second part of the article deals with notions of subformula, proper subformula and immediate constituent of a QC-formula.
  6. Czeslaw Bylinski, Grzegorz Bancerek. Variables in Formulae of the First Order Language, Formalized Mathematics 1(3), pages 459-469, 1990. MML Identifier: QC_LANG3
    Summary: We develop the first order language defined in \cite{QC_LANG1.ABS}. We continue the work done in the article \cite{QC_LANG2.ABS}. We prove some schemes of defining by structural induction. We deal with notions of closed subformulae and of still not bound variables in a formula. We introduce the concept of the set of all free variables and the set of all fixed variables occurring in a formula.
  7. Jaroslaw Kotowicz. Monotone Real Sequences. Subsequences, Formalized Mathematics 1(3), pages 471-475, 1990. MML Identifier: SEQM_3
    Summary: The article contains definitions of constant, increasing, decreasing, non decreasing, non increasing sequences, the definition of a subsequence and their basic properties.
  8. Jaroslaw Kotowicz. Convergent Real Sequences. Upper and Lower Bound of Sets of Real Numbers, Formalized Mathematics 1(3), pages 477-481, 1990. MML Identifier: SEQ_4
    Summary: The article contains theorems about convergent sequences and the limit of sequences occurring in \cite{SEQ_2.ABS} such as Bolzano-Weierstrass theorem, Cauchy theorem and others. Bounded sets of real numbers and lower and upper bound of subset of real numbers are defined.
  9. Michal Muzalewski. Midpoint algebras, Formalized Mathematics 1(3), pages 483-488, 1990. MML Identifier: MIDSP_1
    Summary: In this article basic properties of midpoint algebras are proved. We define a congruence relation $\equiv$ on bound vectors and free vectors as the equivalence classes of $\equiv$.
  10. Pawel Sadowski, Andrzej Trybulec, Konrad Raczkowski. The Fundamental Logic Structure in Quantum Mechanics, Formalized Mathematics 1(3), pages 489-494, 1990. MML Identifier: QMAX_1
    Summary: In this article we present the logical structure given by four axioms of Mackey \cite{MACKEY} in the set of propositions of Quantum Mechanics. The equivalence relation (PropRel(Q)) in the set of propositions (Prop Q) for given Quantum Mechanics Q is considered. The main text for this article is \cite{EQREL_1.ABS} where the structure of quotient space and the properties of equivalence relations, classes and partitions are studied.
  11. Andrzej Trybulec. Function Domains and Fr\aenkel Operator, Formalized Mathematics 1(3), pages 495-500, 1990. MML Identifier: FRAENKEL
    Summary: We deal with a non--empty set of functions and a non--empty set of functions from a set $A$ to a non--empty set $B$. In the case when $B$ is a non--empty set, $B^A$ is redefined. It yields a non--empty set of functions from $A$ to $B$. An element of such a set is redefined as a function from $A$ to $B$. Some theorems concerning these concepts are proved, as well as a number of schemes dealing with infinity and the Axiom of Choice. The article contains a number of schemes allowing for simple logical transformations related to terms constructed with the Fr{\ae}nkel Operator.
  12. Michal J. Trybulec. Integers, Formalized Mathematics 1(3), pages 501-505, 1990. MML Identifier: INT_1
    Summary: In the article the following concepts were introduced: the set of integers (${\Bbb Z }$) and its elements (integers), congruences ($i_1 \equiv i_2 (\mathop{\rm mod} i_3)$), the ceiling and floor functors ($\mathopen{\lceil} x \mathclose{\rceil}$ and $\mathopen{\lfloor} x \mathclose{\rfloor}$), also the fraction part of a real number (frac), the integer division ($\div$) and remainder of integer division (mod). The following schemes were also included: the separation scheme ({\it SepInt}), the schemes of integer induction ({\it Int\_Ind\_Down}, {\it Int\_Ind\_Up}, {\it Int\_Ind\_Full}), the minimum ({\it Int\_Min}) and maximum ({\it Int\_Max}) schemes (the existence of minimum and maximum integers enjoying a given property).
  13. Czeslaw Bylinski. The Complex Numbers, Formalized Mathematics 1(3), pages 507-513, 1990. MML Identifier: COMPLEX1
    Summary: We define the set $\Bbb C$ of complex numbers as the set of all ordered pairs $z =\langle a,b\rangle$ where $a$ and $b$ are real numbers and where addition and multiplication are defined. We define the real and imaginary parts of $z$ and denote this by $a = \Re(z)$, $b = \Im(z)$. These definitions satisfy all the axioms for a field. $0_{\Bbb C} = 0+0i$ and $1_{\Bbb C} = 1+0i$ are identities for addition and multiplication respectively, and there are multiplicative inverses for each non zero element in $\Bbb C$. The difference and division of complex numbers are also defined. We do not interpret the set of all real numbers $\Bbb R$ as a subset of $\Bbb C$. From here on we do not abandon the ordered pair notation for complex numbers. For example: $i^2 = (0+1i)^2 = -1+0i \neq -1$. We conclude this article by introducing two operations on $\Bbb C$ which are not field operations. We define the absolute value of $z$ denoted by $|z|$ and the conjugate of $z$ denoted by $z^\ast$.
  14. Grzegorz Bancerek. Ordinal Arithmetics, Formalized Mathematics 1(3), pages 515-519, 1990. MML Identifier: ORDINAL3
    Summary: At the beginning the article contains some auxiliary theorems concerning the constructors defined in papers \cite{ORDINAL1.ABS} and \cite{ORDINAL2.ABS}. Next simple properties of addition and multiplication of ordinals are shown, e.g. associativity of addition. Addition and multiplication of a transfinite sequence of ordinals and a ordinal are also introduced here. The goal of the article is the proof that the distributivity of multiplication wrt addition and the associativity of multiplication hold. Additionally new binary functors of ordinals are introduced: subtraction, exact division, and remainder and some of their basic properties are presented.
  15. Czeslaw Bylinski. The Modification of a Function by a Function and the Iteration of the Composition of a Function, Formalized Mathematics 1(3), pages 521-527, 1990. MML Identifier: FUNCT_4
    Summary: In the article we introduce some operations on functions. We define the natural ordering relation on functions. The fact that a function $f$ is less than a function $g$ we denote by $f \leq g$ and we define by $\hbox{graph} f \subseteq \hbox{graph} f$. In the sequel we define the modifications of a function $f$ by a function $g$ denoted $f \hbox{+$\cdot$} g$ and the $n$-th iteration of the composition of a function $f$ denoted by $f^n$. We prove some propositions related to the introduced notions.
  16. Czeslaw Bylinski. Finite Sequences and Tuples of Elements of a Non-empty Sets, Formalized Mathematics 1(3), pages 529-536, 1990. MML Identifier: FINSEQ_2
    Summary: The first part of the article is a continuation of \cite{FINSEQ_1.ABS}. Next, we define the identity sequence of natural numbers and the constant sequences. The main part of this article is the definition of tuples. The element of a set of all sequences of the length $n$ of $D$ is called a tuple of a non-empty set $D$ and it is denoted by element of $D^{n}$. Also some basic facts about tuples of a non-empty set are proved.
  17. Grzegorz Bancerek. Curried and Uncurried Functions, Formalized Mathematics 1(3), pages 537-541, 1990. MML Identifier: FUNCT_5
    Summary: In the article following functors are introduced: the projections of subsets of the Cartesian product, the functor which for every function $f:X \times Y \to Z$ gives some curried function ($X \to(Y \to Z)$), and the functor which from curried functions makes uncurried functions. Some of their properties and some properties of the set of all functions from a set into a set are also shown.
  18. Grzegorz Bancerek. Cardinal Arithmetics, Formalized Mathematics 1(3), pages 543-547, 1990. MML Identifier: CARD_2
    Summary: In the article addition, multiplication and power operation of cardinals are introduced. Presented are some properties of equipotence of Cartesian products, basic cardinal arithmetics laws (transformativity, associativity, distributivity), and some facts about finite sets.
  19. Eugeniusz Kusak, Wojciech Leonczuk. Fano-Desargues Parallelity Spaces, Formalized Mathematics 1(3), pages 549-553, 1990. MML Identifier: PARSP_2
    Summary: This article is the second part of Parallelity Space. It contains definition of a Fano-Desargues space, axioms of a Fano-Desargues parallelity space, definition of the relations: collinearity, parallelogram and directed congruence and some basic facts concerned with them.
  20. Henryk Oryszczyszyn , Krzysztof Prazmowski. Real Functions Spaces, Formalized Mathematics 1(3), pages 555-561, 1990. MML Identifier: FUNCSDOM
    Summary: This abstract contains a construction of the domain of functions defined in an arbitrary nonempty set, with values being real numbers. In every such set of functions we introduce several algebraic operations, which yield in this set the structures of a real linear space, of a ring, and of a real algebra. Formal definitions of such concepts are given.
  21. Grzegorz Bancerek. Tarski's Classes and Ranks, Formalized Mathematics 1(3), pages 563-567, 1990. MML Identifier: CLASSES1
    Summary: In the article the Tarski's classes (non-empty families of sets satisfying Tarski's axiom A given in \cite{TARSKI.ABS}) and the rank sets are introduced and some of their properties are shown. The transitive closure and the rank of a set is given here too.
  22. Wojciech A. Trybulec. Non-contiguous Substrings and One-to-one Finite Sequences, Formalized Mathematics 1(3), pages 569-573, 1990. MML Identifier: FINSEQ_3
    Summary: This text is a continuation of \cite{FINSEQ_1.ABS}. We prove a number of theorems concerning both notions introduced there and one-to-one finite sequences. We introduce a function that removes from a string elements of the string that belongs to a given set.
  23. Wojciech A. Trybulec. Pigeon Hole Principle, Formalized Mathematics 1(3), pages 575-579, 1990. MML Identifier: FINSEQ_4
    Summary: We introduce the notion of a predicate that states that a function is one-to-one at a given element of its domain (i.e. counterimage of image of the element is equal to its singleton). We also introduce some rather technical functors concerning finite sequences: the lowest index of the given element of the range of the finite sequence, the substring preceding (and succeeding) the first occurrence of given element of the range. At the end of the article we prove the pigeon hole principle.
  24. Wojciech A. Trybulec. Linear Combinations in Real Linear Space, Formalized Mathematics 1(3), pages 581-588, 1990. MML Identifier: RLVECT_2
    Summary: The article is continuation of \cite{RLVECT_1.ABS}. At the beginning we prove some theorems concerning sums of finite sequence of vectors. We introduce the following notions: sum of finite subset of vectors, linear combination, carrier of linear combination, linear combination of elements of a given set of vectors, sum of linear combination. We also show that the set of linear combinations is a real linear space. At the end of article we prove some auxiliary theorems that should be proved in \cite{BOOLE.ABS}, \cite{FUNCT_1.ABS}, \cite{FINSET_1.ABS}, \cite{NAT_1.ABS} or \cite{REAL_1.ABS}.
  25. Grzegorz Bancerek. K\"onig's Theorem, Formalized Mathematics 1(3), pages 589-593, 1990. MML Identifier: CARD_3
    Summary: In the article the sum and product of any number of cardinals are introduced and their relationships to addition, multiplication and to other concepts are shown. Then the K\"onig's theorem is proved. The theorem that the cardinal of union of increasing family of sets of power less than some cardinal {\bf m} is not greater than {\bf m}, is given too.
  26. Bogdan Nowak, Grzegorz Bancerek. Universal Classes, Formalized Mathematics 1(3), pages 595-600, 1990. MML Identifier: CLASSES2
    Summary: In the article we have shown that there exist universal classes, i.e. there are sets which are closed w.r.t. basic set theory operations.
  27. Henryk Oryszczyszyn, Krzysztof Prazmowski. Analytical Ordered Affine Spaces, Formalized Mathematics 1(3), pages 601-605, 1990. MML Identifier: ANALOAF
    Summary: In the article with a given arbitrary real linear space we correlate the (ordered) affine space defined in terms of a directed parallelity of segments. The abstract contains a construction of the ordered affine structure associated with a vector space; this is a structure of the type which frequently occurs in geometry and consists of the set of points and a binary relation on segments. For suitable underlying vector spaces we prove that the corresponding affine structures are ordered affine spaces or ordered affine planes, i.e. that they satisfy appropriate axioms. A formal definition of an arbitrary ordered affine space and an arbitrary ordered affine plane is given.
  28. Stanislawa Kanas, Adam Lecko, Mariusz Startek. Metric Spaces, Formalized Mathematics 1(3), pages 607-610, 1990. MML Identifier: METRIC_1
    Summary: In this paper we define the metric spaces. Two examples of metric spaces are given. We define the discrete metric and the metric on the real axis. Moreover the open ball, the close ball and the sphere in metric spaces are introduced. We also prove some theorems concerning these concepts.
  29. Henryk Oryszczyszyn, Krzysztof Prazmowski. Ordered Affine Spaces Defined in Terms of Directed Parallelity -- Part I, Formalized Mathematics 1(3), pages 611-615, 1990. MML Identifier: DIRAF
    Summary: In the article we consider several geometrical relations in given arbitrary ordered affine space defined in terms of directed parallelity. In particular we introduce the notions of the nondirected parallelity of segments, of collinearity, and the betweenness relation determined by the given relation of directed parallelity. The obtained structures satisfy commonly accepted axioms for affine spaces. At the end of the article we introduce a formal definition of affine space and affine plane (defined in terms of parallelity of segments).
  30. Henryk Oryszczyszyn, Krzysztof Prazmowski. Parallelity and Lines in Affine Spaces, Formalized Mathematics 1(3), pages 617-621, 1990. MML Identifier: AFF_1
    Summary: In the article we introduce basic notions concerning affine spaces and investigate their fundamental properties. We define the function which to every nondegenerate pair of points assigns the line joining them and we extend the relation of parallelity to a relation between segments and lines, and between lines.