Volume 1, 1990
Number 1
  1. Andrzej Trybulec. Tarski Grothendieck Set Theory, Formalized Mathematics 1(1), pages 9-11, 1990. MML Identifier: TARSKI
    Summary: This is the first part of the axiomatics of the Mizar system. It includes the axioms of the Tarski Grothendieck set theory. They are: the axiom stating that everything is a set, the extensionality axiom, the definitional axiom of the singleton, the definitional axiom of the pair, the definitional axiom of the union of a family of sets, the definitional axiom of the boolean (the power set) of a set, the regularity axiom, the definitional axiom of the ordered pair, the Tarski's axiom~A introduced in \cite{TARSKI:1} (see also \cite{TARSKI:2}), and the Fr\ae nkel scheme. Also, the definition of equinumerosity is introduced.
  2. Andrzej Trybulec. Built-in Concepts, Formalized Mathematics 1(1), pages 13-15, 1990. MML Identifier: AXIOMS
    Summary: This abstract contains the second part of the axiomatics of the Mizar system (the first part is in abstract \cite{TARSKI.ABS}). The axioms listed here characterize the Mizar built-in concepts that are automatically attached to every Mizar article. We give definitional axioms of the following concepts: element, subset, Cartesian product, domain (non empty subset), subdomain (non empty subset of a domain), set domain (domain consisting of sets). Axioms of strong arithmetics of real numbers are also included.
  3. Zinaida Trybulec, Halina Swiczkowska. Boolean Properties of Sets, Formalized Mathematics 1(1), pages 17-23, 1990. MML Identifier: BOOLE
    Summary: This article contains proofs of the theorems which are obvious if the directive 'requirements BOOLE;' will be added to enviroment declaration of the Mizar article.
  4. Andrzej Trybulec. Enumerated Sets, Formalized Mathematics 1(1), pages 25-34, 1990. MML Identifier: ENUMSET1
    Summary: We prove basic facts about enumerated sets: definitional theorems and their immediate consequences, some theorems related to the decomposition of an enumerated set into union of two sets, facts about removing elements that occur more than once, and facts about permutations of enumerated sets (with the length $\le$ 4). The article includes also schemes enabling instantiation of up to nine universal quantifiers.
  5. Krzysztof Hryniewiecki. Basic Properties of Real Numbers, Formalized Mathematics 1(1), pages 35-40, 1990. MML Identifier: REAL_1
    Summary: Basic facts of arithmetics of real numbers are presented: definitions and properties of the complement element, the inverse element, subtraction and division; some basic properties of the set REAL (e.g. density), and the scheme of separation for sets of reals.
  6. Grzegorz Bancerek. The Fundamental Properties of Natural Numbers, Formalized Mathematics 1(1), pages 41-46, 1990. MML Identifier: NAT_1
    Summary: Some fundamental properties of addition, multiplication, order relations, exact division, the remainder, divisibility, the least common multiple, the greatest common divisor are presented. A proof of Euclid algorithm is also given.
  7. Czeslaw Bylinski. Some Basic Properties of Sets, Formalized Mathematics 1(1), pages 47-53, 1990. MML Identifier: ZFMISC_1
    Summary: In this article some basic theorems about singletons, pairs, power sets, unions of families of sets, and the cartesian product of two sets are proved.
  8. Czeslaw Bylinski. Functions and Their Basic Properties, Formalized Mathematics 1(1), pages 55-65, 1990. MML Identifier: FUNCT_1
    Summary: The definitions of the mode Function and the graph of a function are introduced. The graph of a function is defined to be identical with the function. The following concepts are also defined: the domain of a function, the range of a function, the identity function, the composition of functions, the 1-1 function, the inverse function, the restriction of a function, the image and the inverse image. Certain basic facts about functions and the notions defined in the article are proved.
  9. Zinaida Trybulec. Properties of Subsets, Formalized Mathematics 1(1), pages 67-71, 1990. MML Identifier: SUBSET_1
    Summary: The text includes theorems concerning properties of subsets, and some operations on sets. The functions yielding improper subsets of a set, i.e. the empty set and the set itself are introduced. Functions and predicates introduced for sets are redefined. Some theorems about enumerated sets are proved.
  10. Edmund Woronowicz. Relations and Their Basic Properties, Formalized Mathematics 1(1), pages 73-83, 1990. MML Identifier: RELAT_1
    Summary: We define here: mode Relation as a set of pairs, the domain, the codomain, and the field of relation; the empty and the identity relations, the composition of relations, the image and the inverse image of a set under a relation. Two predicates, = and \subseteq, and three functions, $\cup$, $\cap$ and $\setminus$ are redefined. Basic facts about the above mentioned notions are presented.
  11. Edmund Woronowicz, Anna Zalewska. Properties of Binary Relations, Formalized Mathematics 1(1), pages 85-89, 1990. MML Identifier: RELAT_2
    Summary: The paper contains definitions of some properties of binary relations: reflexivity, irreflexivity, symmetry, asymmetry, antisymmetry, connectedness, strong connectedness, and transitivity. Basic theorems relating the above mentioned notions are given.
  12. Grzegorz Bancerek. The Ordinal Numbers, Formalized Mathematics 1(1), pages 91-96, 1990. MML Identifier: ORDINAL1
    Summary: In the beginning of the article we show some consequences of the regularity axiom. In the second part we introduce the successor of a set and the notions of transitivity and connectedness wrt membership relation. Then we define ordinal numbers as transitive and connected sets, and we prove some theorems of them and of their sets. Lastly we introduce the concept of a transfinite sequence and we show transfinite induction and schemes of defining by transfinite induction.
  13. Andrzej Trybulec. Tuples, Projections and Cartesian Products, Formalized Mathematics 1(1), pages 97-105, 1990. MML Identifier: MCART_1
    Summary: The purpose of this article is to define projections of ordered pairs, and to introduce triples and quadruples, and their projections. The theorems in this paper may be roughly divided into two groups: theorems describing basic properties of introduced concepts and theorems related to the regularity, analogous to those proved for ordered pairs by Cz. Byli\'nski \cite{ZFMISC_1.ABS}. Cartesian products of subsets are redefined as subsets of Cartesian products.
  14. Grzegorz Bancerek, Krzysztof Hryniewiecki. Segments of Natural Numbers and Finite Sequences, Formalized Mathematics 1(1), pages 107-114, 1990. MML Identifier: FINSEQ_1
    Summary: We define the notion of an initial segment of natural numbers and prove a number of their properties. Using this notion we introduce finite sequences, subsequences, the empty sequence, a sequence of a domain, and the operation of concatenation of two sequences.
  15. Andrzej Trybulec. Domains and Their Cartesian Products, Formalized Mathematics 1(1), pages 115-122, 1990. MML Identifier: DOMAIN_1
    Summary: The article includes: theorems related to domains, theorems related to Cartesian products presented earlier in various articles and simplified here by substituting domains for sets and omitting the assumption that the sets involved must not be empty. Several schemes and theorems related to Fraenkel operator are given. We also redefine subset yielding functions such as the pair of elements of a set and the union of two subsets of a set.
  16. Grzegorz Bancerek. The Well Ordering Relations, Formalized Mathematics 1(1), pages 123-129, 1990. MML Identifier: WELLORD1
    Summary: Some theorems about well ordering relations are proved. The goal of the article is to prove that every two well ordering relations are either isomorphic or one of them is isomorphic to a segment of the other. The following concepts are defined: the segment of a relation induced by an element, well founded relations, well ordering relations, the restriction of a relation to a set, and the isomorphism of two relations. A number of simple facts is presented.
  17. Grzegorz Bancerek. A Model of ZF Set Theory Language, Formalized Mathematics 1(1), pages 131-145, 1990. MML Identifier: ZF_LANG
    Summary: The goal of this article is to construct a language of the ZF set theory and to develop a notational and conceptual base which facilitates a convenient usage of the language.
  18. Beata Padlewska. Families of Sets, Formalized Mathematics 1(1), pages 147-152, 1990. MML Identifier: SETFAM_1
    Summary: The article contains definitions of the following concepts: family of sets, family of subsets of a set, the intersection of a family of sets. Functors $\cup$, $\cap$, and $\setminus$ are redefined for families of subsets of a set. Some properties of these notions are presented.
  19. Czeslaw Bylinski. Functions from a Set to a Set, Formalized Mathematics 1(1), pages 153-164, 1990. MML Identifier: FUNCT_2
    Summary: The article is a continuation of \cite{FUNCT_1.ABS}. We define the following concepts: a function from a set $X$ into a set $Y$, denoted by ``Function of $X$,$Y$'', the set of all functions from a set $X$ into a set $Y$, denoted by Funcs($X$,$Y$), and the permutation of a set (mode Permutation of $X$, where $X$ is a set). Theorems and schemes included in the article are reformulations of the theorems of \cite{FUNCT_1.ABS} in the new terminology. Also some basic facts about functions of two variables are proved.
  20. Agata Darmochwal. Finite Sets, Formalized Mathematics 1(1), pages 165-167, 1990. MML Identifier: FINSET_1
    Summary: The article contains the definition of a finite set based on the notion of finite sequence. Some theorems about properties of finite sets and finite families of sets are proved.
  21. Czeslaw Bylinski. Graphs of Functions, Formalized Mathematics 1(1), pages 169-173, 1990. MML Identifier: GRFUNC_1
    Summary: The graph of a function is defined in \cite{FUNCT_1.ABS}. In this paper the graph of a function is redefined as a Relation. Operations on functions are interpreted as the corresponding operations on relations. Some theorems about graphs of functions are proved.
  22. Czeslaw Bylinski. Binary Operations, Formalized Mathematics 1(1), pages 175-180, 1990. MML Identifier: BINOP_1
    Summary: In this paper we define binary and unary operations on domains. We also define the following predicates concerning the operations: $\dots$ is commutative, $\dots$ is associative, $\dots$ is the unity of $\dots$, and $\dots$ is distributive wrt $\dots$. A number of schemes useful in justifying the existence of the operations are proved.
  23. Edmund Woronowicz. Relations Defined on Sets, Formalized Mathematics 1(1), pages 181-186, 1990. MML Identifier: RELSET_1
    Summary: The article includes theorems concerning properties of relations defined as a subset of the Cartesian product of two sets (mode Relation of $X$,$Y$ where $X$,$Y$ are sets). Some notions, introduced in \cite{RELAT_1.ABS} such as domain, codomain, field of a relation, composition of relations, image and inverse image of a set under a relation are redefined.
  24. Andrzej Trybulec, Agata Darmochwal. Boolean Domains, Formalized Mathematics 1(1), pages 187-190, 1990. MML Identifier: FINSUB_1
    Summary: BOOLE DOMAIN is a SET DOMAIN that is closed under union and difference. This condition is equivalent to being closed under symmetric difference and one of the following operations: union, intersection or difference. We introduce the set of all finite subsets of a set $A$, denoted by Fin $A$. The mode Finite Subset of a set $A$ is introduced with the mother type: Element of Fin $A$. In consequence, ``Finite Subset of \dots '' is an elementary type, therefore one may use such types as ``set of Finite Subset of $A$'', ``[(Finite Subset of $A$), Finite Subset of $A$]'', and so on. The article begins with some auxiliary theorems that belong really to \cite{BOOLE.ABS} or \cite{ORDINAL1.ABS} but are missing there. Moreover, bool $A$ is redefined as a SET DOMAIN, for an arbitrary set $A$.
  25. Grzegorz Bancerek. Models and Satisfiability, Formalized Mathematics 1(1), pages 191-199, 1990. MML Identifier: ZF_MODEL
    Summary: The article includes schemes of defining by structural induction, and definitions and theorems related to: the set of variables which have free occurrences in a ZF-formula, the set of all valuations of variables in a model, the set of all valuations which satisfy a ZF-formula in a model, the satisfiability of a ZF-formula in a model by a valuation, the validity of a ZF-formula in a model, the axioms of ZF-language, the model of the ZF set theory.
  26. Grzegorz Bancerek. The Contraction Lemma, Formalized Mathematics 1(1), pages 201-203, 1990. MML Identifier: ZF_COLLA
    Summary: The article includes the proof of the contraction lemma which claims that every class in which the axiom of extensionality is valid is isomorphic with a transitive class. In this article the isomorphism (wrt membership relation) of two sets is defined. It is based on \cite{MOST:1}.
  27. Wojciech A. Trybulec. Axioms of Incidency, Formalized Mathematics 1(1), pages 205-213, 1990. MML Identifier: INCSP_1
    Summary: This article is based on {\it ``Foundations of Geometry''} by Karol Borsuk and Wanda Szmielew (\cite{BORSUK:1}). The fourth axiom of incidency is weakened. In \cite{BORSUK:1} it has the form {\it for any plane there exist three non-collinear points in the plane} and in the article {\it for any plane there exists one point in the plane}. The original axiom is proved. The article includes: theorems concerning collinearity of points and coplanarity of points and lines, basic theorems concerning lines and planes, fundamental existence theorems, theorems concerning intersection of lines and planes.
  28. Stanislaw Zukowski. Introduction to Lattice Theory, Formalized Mathematics 1(1), pages 215-222, 1990. MML Identifier: LATTICES
    Summary: A lattice is defined as an algebra on a nonempty set with binary operations join and meet which are commutative and associative, and satisfy the absorption identities. The following kinds of lattices are considered: distributive, modular, bounded (with zero and unit elements), complemented, and Boolean (with complement). The article includes also theorems which immediately follow from definitions.
  29. Beata Padlewska, Agata Darmochwal. Topological Spaces and Continuous Functions, Formalized Mathematics 1(1), pages 223-230, 1990. MML Identifier: PRE_TOPC
    Summary: The paper contains a definition of topological space. The following notions are defined: point of topological space, subset of topological space, subspace of topological space, and continuous function.
  30. Miroslaw Wysocki, Agata Darmochwal. Subsets of Topological Spaces, Formalized Mathematics 1(1), pages 231-237, 1990. MML Identifier: TOPS_1
    Summary: The article contains some theorems about open and closed sets. The following topological operations on sets are defined: closure, interior and frontier. The following notions are introduced: dense set, boundary set, nowheredense set and set being domain (closed domain and open domain), and some basic facts concerning them are proved.
  31. Beata Padlewska. Connected Spaces, Formalized Mathematics 1(1), pages 239-244, 1990. MML Identifier: CONNSP_1
    Summary: The following notions are defined: separated sets, connected spaces, connected sets, components of a topological space, the component of a point. The definition of the boundary of a set is also included. The singleton of a point of a topological space is redefined as a subset of the space. Some theorems about these notions are proved.
  32. Czeslaw Bylinski. Basic Functions and Operations on Functions, Formalized Mathematics 1(1), pages 245-254, 1990. MML Identifier: FUNCT_3
    Summary: We define the following mappings: the characteristic function of a subset of a set, the inclusion function (injection or embedding), the projections from a Cartesian product onto its arguments and diagonal function (inclusion of a set into its Cartesian square). Some operations on functions are also defined: the products of two functions (the complex function and the more general product-function), the function induced on power sets by the image and inverse-image. Some simple propositions related to the introduced notions are proved.
Number 2
  1. Agata Darmochwal. Families of Subsets, Subspaces and Mappings in Topological Spaces, Formalized Mathematics 1(2), pages 257-261, 1990. MML Identifier: TOPS_2
    Summary: This article is a continuation of \cite{TOPS_1.ABS}. Some basic theorems about families of sets in a topological space have been proved. Following redefinitions have been made: singleton of a set as a family in the topological space and results of boolean operations on families as a family of the topological space. Notion of a family of complements of sets and a closed (open) family have been also introduced. Next some theorems refer to subspaces in a topological space: some facts about types in a subspace, theorems about open and closed sets and families in a subspace. A notion of restriction of a family has been also introduced and basic properties of this notion have been proved. The last part of the article is about mappings. There are proved necessary and sufficient conditions for a mapping to be continuous. A notion of homeomorphism has been defined next. Theorems about homeomorphisms of topological spaces have been also proved.
  2. Jan Popiolek. Some Properties of Functions Modul and Signum, Formalized Mathematics 1(2), pages 263-264, 1990. MML Identifier: ANAL_1
    Summary:
  3. Jan Popiolek. Some Properties of Functions Modul and Signum, Formalized Mathematics 1(2), pages 263-264, 1990. MML Identifier: ABSVALUE
    Summary: The article includes definitions and theorems concerning basic properties of the following functions: $|x|$ -- modul of real number, sgn $x$ -- signum of real number.
  4. Grzegorz Bancerek. Zermelo Theorem and Axiom of Choice, Formalized Mathematics 1(2), pages 265-267, 1990. MML Identifier: WELLORD2
    Summary: The article is continuation of \cite{WELLORD1.ABS} and \cite{ORDINAL1.ABS}, and the goal of it is show that Zermelo theorem (every set has a relation which well orders it - proposition (26)) and axiom of choice (for every non-empty family of non-empty and separate sets there is set which has exactly one common element with arbitrary family member - proposition (27)) are true. It is result of the Tarski's axiom A introduced in \cite{TARSKI:1} and repeated in \cite{TARSKI.ABS}. Inclusion as a settheoretical binary relation is introduced, the correspondence of well ordering relations to ordinal numbers is shown, and basic properties of equinumerosity are presented. Some facts are based on \cite{KURAT-MOST:1}.
  5. Jaroslaw Kotowicz. Real Sequences and Basic Operations on Them, Formalized Mathematics 1(2), pages 269-272, 1990. MML Identifier: SEQ_1
    Summary: Definition of real sequence and operations on sequences (multiplication of sequences and multiplication by a real number, addition, subtraction, division and absolute value of sequence) are given.
  6. Jaroslaw Kotowicz. Convergent Sequences and the Limit of Sequences, Formalized Mathematics 1(2), pages 273-275, 1990. MML Identifier: SEQ_2
    Summary: The article contains definitions and same basic properties of bounded sequences (above and below), convergent sequences and the limit of sequences. In the article there are some properties of real numbers useful in the other theorems of this article.
  7. Grzegorz Bancerek. Properties of ZF Models, Formalized Mathematics 1(2), pages 277-280, 1990. MML Identifier: ZFMODEL1
    Summary: The article deals with the concepts of satisfiability of ZF set theory language formulae in a model (a non-empty family of sets) and the axioms of ZF theory introduced in \cite{MOST:1}. It is shown that the transitive model satisfies the axiom of extensionality and that it satisfies the axiom of pairs if and only if it is closed to pair operation; it satisfies the axiom of unions if and only if it is closed to union operation, etc. The conditions which are satisfied by arbitrary model of ZF set theory are also shown. Besides introduced are definable and parametrically definable functions.
  8. Grzegorz Bancerek. Sequences of Ordinal Numbers, Formalized Mathematics 1(2), pages 281-290, 1990. MML Identifier: ORDINAL2
    Summary: In the first part of the article we introduce the following operations: On $X$ that yields the set of all ordinals which belong to the set $X$, Lim $X$ that yields the set of all limit ordinals which belong to $X$, and inf $X$ and sup $X$ that yield the minimal ordinal belonging to $X$ and the minimal ordinal greater than all ordinals belonging to $X$, respectively. The second part of the article starts with schemes that can be used to justify the correctness of definitions based on the transfinite induction (see \cite{ORDINAL1.ABS} or \cite{KURAT-MOST:1}). The schemes are used to define addition, product and power of ordinal numbers. The operations of limes inferior and limes superior of sequences of ordinals are defined and the concepts of limit of ordinal sequence and increasing and continuous sequence are introduced.
  9. Wojciech A. Trybulec. Vectors in Real Linear Space, Formalized Mathematics 1(2), pages 291-296, 1990. MML Identifier: RLVECT_1
    Summary: In this article we introduce a notion of real linear space, operations on vectors: addition, multiplication by real number, inverse vector, subtraction. The sum of finite sequence of the vectors is also defined. Theorems that belong rather to \cite{NAT_1.ABS} or \cite{FINSEQ_1.ABS} are proved.
  10. Wojciech A. Trybulec. Subspaces and Cosets of Subspaces in Real Linear Space, Formalized Mathematics 1(2), pages 297-301, 1990. MML Identifier: RLSUB_1
    Summary: The following notions are introduced in the article: subspace of a real linear space, zero subspace and improper subspace, coset of a subspace. The relation of a subset of the vectors being linearly closed is also introduced. Basic theorems concerning those notions are proved in the article.
  11. Piotr Rudnicki, Andrzej Trybulec. A First Order Language, Formalized Mathematics 1(2), pages 303-311, 1990. MML Identifier: QC_LANG1
    Summary: In the paper a first order language is constructed. It includes the universal quantifier and the following propositional connectives: truth, negation, and conjunction. The variables are divided into three kinds: bound variables, fixed variables, and free variables. An infinite number of predicates for each arity is provided. Schemes of structural induction and schemes justifying definitions by structural induction have been proved. The concept of a closed formula (a formula without free occurrences of bound variables) is introduced.
  12. Wojciech A. Trybulec. Partially Ordered Sets, Formalized Mathematics 1(2), pages 313-319, 1990. MML Identifier: ORDERS_1
    Summary: In the beginning of this article we define the choice function of a non-empty set family that does not contain $\emptyset$ as introduced in \cite[pages 88--89]{KURAT:1}. We define order of a set as a relation being reflexive, antisymmetric and transitive in the set, partially ordered set as structure non-empty set and order of the set, chains, lower and upper cone of a subset, initial segments of element and subset of partially ordered set. Some theorems that belong rather to \cite{ZFMISC_1.ABS} or \cite{RELAT_2.ABS} are proved.
  13. Krzysztof Hryniewiecki. Recursive Definitions, Formalized Mathematics 1(2), pages 321-328, 1990. MML Identifier: RECDEF_1
    Summary: The text contains some schemes which allow elimination of definitions by recursion.
  14. Andrzej Trybulec. Binary Operations Applied to Functions, Formalized Mathematics 1(2), pages 329-334, 1990. MML Identifier: FUNCOP_1
    Summary: In the article we introduce functors yielding to a binary operation its composition with an arbitrary functions on its left side, its right side or both. We prove theorems describing the basic properties of these functors. We introduce also constant functions and converse of a function. The recent concept is defined for an arbitrary function, however is meaningful in the case of functions which range is a subset of a Cartesian product of two sets. Then the converse of a function has the same domain as the function itself and assigns to an element of the domain the mirror image of the ordered pair assigned by the function. In the case of functions defined on a non-empty set we redefine the above mentioned functors and prove simplified versions of theorems proved in the general case. We prove also theorems stating relationships between introduced concepts and such properties of binary operations as commutativity or associativity.
  15. Eugeniusz Kusak, Wojciech Leonczuk, Michal Muzalewski. Abelian Groups, Fields and Vector Spaces, Formalized Mathematics 1(2), pages 335-342, 1990. MML Identifier: VECTSP_1
    Summary: This text includes definitions of the Abelian group, field and vector space over a field and some elementary theorems about them.
  16. Eugeniusz Kusak, Wojciech Leonczuk, Michal Muzalewski. Parallelity Spaces, Formalized Mathematics 1(2), pages 343-348, 1990. MML Identifier: PARSP_1
    Summary: In the monography \cite{SZMIELEW:1} W. Szmielew introduced the parallelity planes $\langle S$; $\parallel \rangle$, where $\parallel \subseteq S\times S\times S\times S$. In this text we omit upper bound axiom which must be satisfied by the parallelity planes (see also E.Kusak \cite{KUSAK:1}). Further we will list those theorems which remain true when we pass from the parallelity planes to the parallelity spaces. We construct a model of the parallelity space in Abelian group $\langle F\times F\times F; +_F, -_F, {\bf 0}_F \rangle$, where $F$ is a field.
  17. Eugeniusz Kusak, Wojciech Leonczuk, Michal Muzalewski. Construction of a bilinear antisymmetric form in simplectic vector space, Formalized Mathematics 1(2), pages 349-352, 1990. MML Identifier: SYMSP_1
    Summary: In this text we will present unpublished results by Eu\-ge\-niusz Ku\-sak. It contains an axiomatic description of the class of all spaces $\langle V$; $\perp_\xi \rangle$, where $V$ is a vector space over a field F, $\xi: V \times V \to F$ is a bilinear antisymmetric form i.e. $\xi(x,y) = -\xi(y,x)$ and $x \perp_\xi y $ iff $\xi(x,y) = 0$ for $x$, $y \in V$. It also contains an effective construction of bilinear antisymmetric form $\xi$ for given symplectic space $\langle V$; $\perp \rangle$ such that $\perp = \perp_\xi$. The basic tool used in this method is the notion of orthogonal projection J$(a,b,x)$ for $a,b,x \in V$. We should stress the fact that axioms of orthogonal and symplectic spaces differ only by one axiom, namely: $x\perp y+\varepsilon z \>\&\> y\perp z+\varepsilon x \Rightarrow z\perp x+\varepsilon y. $ For $\varepsilon=+1$ we get the axiom characterizing symplectic geometry. For $\varepsilon=-1$ we get the axiom on three perpendiculars characterizing orthogonal geometry - see \cite{ORTSP_1.ABS}.
  18. Eugeniusz Kusak, Wojciech Leonczuk, Michal Muzalewski. Construction of a bilinear symmetric form in orthogonal vector space, Formalized Mathematics 1(2), pages 353-356, 1990. MML Identifier: ORTSP_1
    Summary: In this text we present unpublished results by Eu\-ge\-niusz Ku\-sak and Wojciech Leo\'nczuk. They contain an axiomatic description of the class of all spaces $\langle V$; $\perp_\xi \rangle$, where $V$ is a vector space over a field F, $\xi: V \times V \to F$ is a bilinear symmetric form i.e. $\xi(x,y) = \xi(y,x)$ and $x \perp_\xi y$ iff $\xi(x,y) = 0$ for $x$, $y \in V$. They also contain an effective construction of bilinear symmetric form $\xi$ for given orthogonal space $\langle V$; $\perp \rangle$ such that $\perp = \perp_\xi$. The basic tool used in this method is the notion of orthogonal projection J$(a,b,x)$ for $a,b,x \in V$. We should stress the fact that axioms of orthogonal and symplectic spaces differ only by one axiom, namely: $x\perp y+\varepsilon z \>\&\> y\perp z+\varepsilon x \Rightarrow z\perp x+\varepsilon y.$ For $\varepsilon=-1$ we get the axiom on three perpendiculars characterizing orthogonal geometry. For $\varepsilon=+1$ we get the axiom characterizing symplectic geometry - see \cite{SYMSP_1.ABS}.
  19. Czeslaw Bylinski. Partial Functions, Formalized Mathematics 1(2), pages 357-367, 1990. MML Identifier: PARTFUN1
    Summary: In the article we define partial functions. We also define the following notions related to partial functions and functions themselves: the empty function, the restriction of a function to a partial function from a set into a set, the set of all partial functions from a set into a set, the total functions, the relation of tolerance of two functions and the set of all total functions which are tolerated by a partial function. Some simple propositions related to the introduced notions are proved. In the beginning of this article we prove some auxiliary theorems and schemes related to the articles: \cite{FUNCT_1.ABS} and \cite{FUNCT_2.ABS}.
  20. Andrzej Trybulec. Semilattice Operations on Finite Subsets, Formalized Mathematics 1(2), pages 369-376, 1990. MML Identifier: SETWISEO
    Summary: In the article we deal with a binary operation that is associative, commutative. We define for such an operation a functor that depends on two more arguments: a finite set of indices and a function indexing elements of the domain of the operation and yields the result of applying the operation to all indexed elements. The definition has a restriction that requires that either the set of indices is non empty or the operation has the unity. We prove theorems describing some properties of the functor introduced. Most of them we prove in two versions depending on which requirement is fulfilled. In the second part we deal with the union of finite sets that enjoys mentioned above properties. We prove analogs of the theorems proved in the first part. We precede the main part of the article with auxiliary theorems related to boolean properties of sets, enumerated sets, finite subsets, and functions. We define a casting function that yields to a set the empty set typed as a finite subset of the set. We prove also two schemes of the induction on finite sets.
  21. Grzegorz Bancerek. Cardinal Numbers, Formalized Mathematics 1(2), pages 377-382, 1990. MML Identifier: CARD_1
    Summary: We present the choice function rule in the beginning of the article. In the main part of the article we formalize the base of cardinal theory. In the first section we introduce the concept of cardinal numbers and order relations between them. We present here Cantor-Bernstein theorem and other properties of order relation of cardinals. In the second section we show that every set has cardinal number equipotence to it. We introduce notion of alephs and we deal with the concept of finite set. At the end of the article we show two schemes of cardinal induction. Some definitions are based on \cite{GUZ-ZBIER:1} and \cite{KURAT-MOST:1}.
  22. Agata Darmochwal. Compact Spaces, Formalized Mathematics 1(2), pages 383-386, 1990. MML Identifier: COMPTS_1
    Summary: The article contains definition of a compact space and some theorems about compact spaces. The notions of a cover of a set and a centered family are defined in the article to be used in these theorems. A set is compact in the topological space if and only if every open cover of the set has a finite subcover. This definition is equivalent, what has been shown next, to the following definition: a set is compact if and only if a subspace generated by that set is compact. Some theorems about mappings and homeomorphisms of compact spaces have been also proved. The following schemes used in proofs of theorems have been proved in the article: FuncExChoice -- the scheme of choice of a function, BiFuncEx -- the scheme of parallel choice of two functions and the theorem about choice of a finite counter image of a finite image.
  23. Wojciech A. Trybulec, Grzegorz Bancerek. Kuratowski -- Zorn Lemma, Formalized Mathematics 1(2), pages 387-393, 1990. MML Identifier: ORDERS_2
    Summary: The goal of this article is to prove Kuratowski - Zorn lemma. We prove it in a number of forms (theorems and schemes). We introduce the following notions: a relation is a quasi (or partial, or linear) order, a relation quasi (or partially, or linearly) orders a set, minimal and maximal element in a relation, inferior and superior element of a relation, a set has lower (or upper) Zorn property w.r.t. a relation. We prove basic theorems concerning those notions and theorems that relate them to the notions introduced in \cite{ORDERS_1.ABS}. At the end of the article we prove some theorems that belong rather to \cite{RELAT_1.ABS}, \cite{RELAT_2.ABS} or \cite{WELLORD1.ABS}.
  24. Wojciech A. Trybulec. Operations on Subspaces in Real Linear Space, Formalized Mathematics 1(2), pages 395-399, 1990. MML Identifier: RLSUB_2
    Summary: In this article the following operations on subspaces of real linear space are intoduced: sum, intersection and direct sum. Some theorems about those notions are proved. We define linear complement of a subspace. Some theorems about decomposition of a vector onto two subspaces and onto subspace and its linear complement are proved. We also show that a set of subspaces with operations sum and intersection is a lattice. At the end of the article theorems that belong rather to \cite{BOOLE.ABS}, \cite{RLVECT_1.ABS}, \cite{RLSUB_1.ABS} or \cite{LATTICES.ABS} are proved.
  25. Andrzej Ndzusiak. $\sigma$-Fields and Probability, Formalized Mathematics 1(2), pages 401-407, 1990. MML Identifier: PROB_1
    Summary: This article contains definitions and theorems concerning basic properties of following objects: - a field of subsets of given nonempty set; - a sequence of subsets of given nonempty set; - a $\sigma$-field of subsets of given nonempty set and events from this $\sigma$-field; - a probability i.e. $\sigma$-additive normed measure defined on previously introduced $\sigma$-field; - a $\sigma$-field generated by family of subsets of given set; - family of Borel Sets.
  26. Czeslaw Bylinski. Introduction to Categories and Functors, Formalized Mathematics 1(2), pages 409-420, 1990. MML Identifier: CAT_1
    Summary: The category is introduced as an ordered 5-tuple of the form $\langle O, M, dom, cod, \cdot, id \rangle$ where $O$ (objects) and $M$ (morphisms) are arbitrary nonempty sets, $dom$ and $cod$ map $M$ onto $O$ and assign to a morphism domain and codomain, $\cdot$ is a partial binary map from $M \times M$ to $M$ (composition of morphisms), $id$ applied to an object yields the identity morphism. We define the basic notions of the category theory such as hom, monic, epi, invertible. We next define functors, the composition of functors, faithfulness and fullness of functors, isomorphism between categories and the identity functor.
  27. Grzegorz Bancerek. Introduction to Trees, Formalized Mathematics 1(2), pages 421-427, 1990. MML Identifier: TREES_1
    Summary: The article consists of two parts: the first one deals with the concept of the prefixes of a finite sequence, the second one introduces and deals with the concept of tree. Besides some auxiliary propositions concerning finite sequences are presented. The trees are introduced as non-empty sets of finite sequences of natural numbers which are closed on prefixes and on sequences of less numbers (i.e. if $\langle n_1$, $n_2$, $\dots$, $n_k\rangle$ is a vertex (element) of a tree and $m_i \leq n_i$ for $i = 1$, $2$, $\dots$, $k$, then $\langle m_1$, $m_2$, $\dots$, $m_k\rangle$ also is). Finite trees, elementary trees with $n$ leaves, the leaves and the subtrees of a tree, the inserting of a tree into another tree, with a node used for determining the place of insertion, antichains of prefixes, and height and width of finite trees are introduced.
Number 3
  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.
Number 4
  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.
Number 5
  1. Jozef Bialas. Properties of Fields, Formalized Mathematics 1(5), pages 807-812, 1990. MML Identifier: REALSET2
    Summary: The second part of considerations concerning groups and fields. It includes a definition and properties of commutative field $F$ as a structure defined by: the set, a support of $F$, containing two different elements, by two binary operations ${\bf +}_{F}$, ${\bf \cdot}_{F}$ on this set, called addition and multiplication, and by two elements from the support of $F$, ${\bf 0}_{F}$ being neutral for addition and ${\bf 1}_{F}$ being neutral for multiplication. This structure is named a field if $\langle$the support of $F$, ${\bf +}_{F}$, ${\bf 0}_{F} \rangle$ and $\langle$the support of $F$, ${\bf \cdot}_{F}$, ${\bf 1}_{F} \rangle$ are commutative groups and multiplication has the property of left-hand and right-hand distributivity with respect to addition. It is demonstrated that the field $F$ satisfies the definition of a field in the axiomatic approach.
  2. Grzegorz Bancerek. Filters -- Part I, Formalized Mathematics 1(5), pages 813-819, 1990. MML Identifier: FILTER_0
    Summary: Filters of a lattice, maximal filters (ultrafilters), operation to create a filter generating by an element or by a non-empty subset of the lattice are discussed. Besides, there are introduced implicative lattices such that for every two elements there is an element being pseudo-complement of them. Some facts concerning these concepts are presented too, i.e. for any proper filter there exists an ultrafilter consisting it.
  3. Wojciech A. Trybulec. Groups, Formalized Mathematics 1(5), pages 821-827, 1990. MML Identifier: GROUP_1
    Summary: Notions of group and abelian group are introduced. The power of an element of a group, order of group and order of an element of a group are defined. Basic theorems concerning those notions are presented.
  4. Rafal Kwiatek, Grzegorz Zwara. The Divisibility of Integers and Integer Relative Primes, Formalized Mathematics 1(5), pages 829-832, 1990. MML Identifier: INT_2
    Summary: { We introduce the following notions: 1)
  5. Michal Muzalewski, Wojciech Skaba. From Loops to Abelian Multiplicative Groups with Zero, Formalized Mathematics 1(5), pages 833-840, 1990. MML Identifier: ALGSTR_1
    Summary: Elementary axioms and theorems on the theory of algebraic structures, taken from the book \cite{SZMIELEW:1}. First a loop structure $\langle G, 0, +\rangle$ is defined and six axioms corresponding to it are given. Group is defined by extending the set of axioms with $(a+b)+c = a+(b+c)$. At the same time an alternate approach to the set of axioms is shown and both sets are proved to yield the same algebraic structure. A trivial example of loop is used to ensure the existence of the modes being constructed. A multiplicative group is contemplated, which is quite similar to the previously defined additive group (called simply a group here), but is supposed to be of greater interest in the future considerations of algebraic structures. The final section brings a slightly more sophisticated structure i.e: a multiplicative loop/group with zero: $\langle G, \cdot, 1, 0\rangle$. Here the proofs are a more challenging and the above trivial example is replaced by a more common (and comprehensive) structure built on the foundation of real numbers.
  6. Andrzej Kondracki. Basic Properties of Rational Numbers, Formalized Mathematics 1(5), pages 841-845, 1990. MML Identifier: RAT_1
    Summary: A definition of rational numbers and some basic properties of them. Operations of addition, subtraction, multiplication are redefined for rational numbers. Functors numerator (num $p$) and denominator (den $p$) ($p$ is rational) are defined and some properties of them are presented. Density of rational numbers is also given.
  7. Wojciech A. Trybulec. Basis of Real Linear Space, Formalized Mathematics 1(5), pages 847-850, 1990. MML Identifier: RLVECT_3
    Summary: Notions of linear independence and dependence of set of vectors, the subspace generated by a set of vectors and basis of real linear space are introduced. Some theorems concerning those notions are proved.
  8. Wojciech A. Trybulec. Finite Sums of Vectors in Vector Space, Formalized Mathematics 1(5), pages 851-854, 1990. MML Identifier: VECTSP_3
    Summary: We define the sum of finite sequences of vectors in vector space. Theorems concerning those sums are proved.
  9. Wojciech A. Trybulec. Subgroup and Cosets of Subgroups, Formalized Mathematics 1(5), pages 855-864, 1990. MML Identifier: GROUP_2
    Summary: We introduce notion of subgroup, coset of a subgroup, sets of left and right cosets of a subgroup. We define multiplication of two subset of a group, subset of reverse elemens of a group, intersection of two subgroups. We define the notion of an index of a subgroup and prove Lagrange theorem which states that in a finite group the order of the group equals the order of a subgroup multiplied by the index of the subgroup. Some theorems that belong rather to \cite{CARD_1.ABS} are proved.
  10. Wojciech A. Trybulec. Subspaces and Cosets of Subspaces in Vector Space, Formalized Mathematics 1(5), pages 865-870, 1990. MML Identifier: VECTSP_4
    Summary: We introduce the notions of subspace of vector space and coset of a subspace. We prove a number of theorems concerning those notions. Some theorems that belong rather to \cite{VECTSP_1.ABS} are proved.
  11. Wojciech A. Trybulec. Operations on Subspaces in Vector Space, Formalized Mathematics 1(5), pages 871-876, 1990. MML Identifier: VECTSP_5
    Summary: Sum, direct sum and intersection of subspaces are introduced. We prove some theorems concerning those notions and the decomposition of vector onto two subspaces. Linear complement of a subspace is also defined. We prove theorems that belong rather to \cite{VECTSP_1.ABS}.
  12. Wojciech A. Trybulec. Linear Combinations in Vector Space, Formalized Mathematics 1(5), pages 877-882, 1990. MML Identifier: VECTSP_6
    Summary: The notion of linear combination of vectors is introduced as a function from the carrier of a vector space to the carrier of the field. Definition of linear combination of set of vectors is also presented. We define addition and subtraction of combinations and multiplication of combination by element of the field. Sum of finite set of vectors and sum of linear combination is defined. We prove theorems that belong rather to \cite{VECTSP_1.ABS}.
  13. Wojciech A. Trybulec. Basis of Vector Space, Formalized Mathematics 1(5), pages 883-885, 1990. MML Identifier: VECTSP_7
    Summary: We prove the existence of a basis of a vector space, i.e., a set of vectors that generates the vector space and is linearly independent. We also introduce the notion of a subspace generated by a set of vectors and linear independence of set of vectors.
  14. Rafal Kwiatek. Factorial and Newton coefficients, Formalized Mathematics 1(5), pages 887-890, 1990. MML Identifier: NEWTON
    Summary: We define the following functions: exponential function (for natural exponent), factorial function and Newton coefficients. We prove some basic properties of notions introduced. There is also a proof of binominal formula. We prove also that $\sum_{k=0}^n {n \choose k}=2^n$.
  15. Henryk Oryszczyszyn, Krzysztof Prazmowski. Analytical Metric Affine Spaces and Planes, Formalized Mathematics 1(5), pages 891-899, 1990. MML Identifier: ANALMETR
    Summary: We introduce relations of orthogonality of vectors and of orthogonality of segments (considered as pairs of vectors) in real linear space of dimension two. This enables us to show an example of (in fact anisotropic and satisfying theorem on three perpendiculars) metric affine space (and plane as well). These two types of objects are defined formally as "Mizar" modes. They are to be understood as structures consisting of a point universe and two binary relations on segments --- a parallelity relation and orthogonality relation, satisfying appropriate axioms. With every such structure we correlate a structure obtained as a reduct of the given one to the parallelity relation only. Some relationships between metric affine spaces and their affine parts are proved; they enable us to use "affine" facts and constructions in investigating metric affine geometry. We define the notions of line, parallelity of lines and two derived relations of orthogonality: between segments and lines, and between lines. Some basic properties of the introduced notions are proved.
  16. Wojciech Leonczuk, Krzysztof Prazmowski. Projective Spaces -- part II, Formalized Mathematics 1(5), pages 901-907, 1990. MML Identifier: ANPROJ_3
    Summary:
  17. Wojciech Leonczuk, Krzysztof Prazmowski. Projective Spaces -- part III, Formalized Mathematics 1(5), pages 909-918, 1990. MML Identifier: ANPROJ_4
    Summary:
  18. Wojciech Leonczuk, Krzysztof Prazmowski. Projective Spaces -- part IV, Formalized Mathematics 1(5), pages 919-927, 1990. MML Identifier: ANPROJ_5
    Summary:
  19. Wojciech Leonczuk, Krzysztof Prazmowski. Projective Spaces -- part V, Formalized Mathematics 1(5), pages 929-938, 1990. MML Identifier: ANPROJ_6
    Summary:
  20. Wojciech Leonczuk, Krzysztof Prazmowski. Projective Spaces -- part VI, Formalized Mathematics 1(5), pages 939-947, 1990. MML Identifier: ANPROJ_7
    Summary:
  21. Waldemar Korczynski. Some Elementary Notions of the Theory of Petri Nets, Formalized Mathematics 1(5), pages 949-953, 1990. MML Identifier: NET_1
    Summary: Some fundamental notions of the theory of Petri nets are described in Mizar formalism. A Petri net is defined as a triple of the form $\langle {\rm places},\,{\rm transitions},\,{\rm flow} \rangle$ with places and transitions being disjoint sets and flow being a relation included in ${\rm places} \times {\rm transitions}$.
  22. Wojciech A. Trybulec. Classes of Conjugation. Normal Subgroups, Formalized Mathematics 1(5), pages 955-962, 1990. MML Identifier: GROUP_3
    Summary: Theorems that were not proved in \cite{GROUP_1.ABS} and in \cite{GROUP_2.ABS} are discussed. In the article we define notion of conjugation for elements, subsets and subgroups of a group. We define the classes of conjugation. Normal subgroups of a group and normalizator of a subset of a group or of a subgroup are introduced. We also define the set of all subgroups of a group. An auxiliary theorem that belongs rather to \cite{CARD_2.ABS} is proved.
  23. Grzegorz Bancerek. Replacing of Variables in Formulas of ZF Theory, Formalized Mathematics 1(5), pages 963-972, 1990. MML Identifier: ZF_LANG1
    Summary: Part one is a supplement to papers \cite{ZF_LANG.ABS}, \cite{ZF_MODEL.ABS}, and \cite{ZFMODEL1.ABS}. It deals with concepts of selector functions, atomic, negative, conjunctive formulas and etc., subformulas, free variables, satisfiability and models (it is shown that axioms of the predicate and the quantifier calculus are satisfied in an arbitrary set). In part two there are introduced notions of variables occurring in a formula and replacing of variables in a formula.
  24. Grzegorz Bancerek. The Reflection Theorem, Formalized Mathematics 1(5), pages 973-977, 1990. MML Identifier: ZF_REFLE
    Summary: The goal is show that the reflection theorem holds. The theorem is as usual in the Morse-Kelley theory of classes (MK). That theory works with universal class which consists of all sets and every class is a subclass of it. In this paper (and in another Mizar articles) we work in Tarski-Grothendieck (TG) theory (see \cite{TARSKI.ABS}) which ensures the existence of sets that have properties like universal class (i.e. this theory is stronger than MK). The sets are introduced in \cite{CLASSES2.ABS} and some concepts of MK are modeled. The concepts are: the class $On$ of all ordinal numbers belonging to the universe, subclasses, transfinite sequences of non-empty elements of universe, etc. The reflection theorem states that if $A_\xi$ is an increasing and continuous transfinite sequence of non-empty sets and class $A = \bigcup_{\xi \in On} A_\xi$, then for every formula $H$ there is a strictly increasing continuous mapping $F: On \to On$ such that if $\varkappa$ is a critical number of $F$ (i.e. $F(\varkappa) = \varkappa > 0$) and $f \in A_\varkappa^{\bf VAR}$, then $A,f\models H \equiv\ {A_\varkappa},f\models H$. The proof is based on \cite{MOST:1}. Besides, in the article it is shown that every universal class is a model of ZF set theory if $\omega$ (the first infinite ordinal number) belongs to it. Some propositions concerning ordinal numbers and sequences of them are also present.
  25. Wojciech A. Trybulec. Binary Operations on Finite Sequences, Formalized Mathematics 1(5), pages 979-981, 1990. MML Identifier: FINSOP_1
    Summary: We generalize the semigroup operation on finite sequences introduced in \cite{SETWOP_2.ABS} for binary operations that have a unity or for non-empty finite sequences.
  26. Andrzej Trybulec. Finite Join and Finite Meet and Dual Lattices, Formalized Mathematics 1(5), pages 983-988, 1990. MML Identifier: LATTICE2
    Summary: The concepts of finite join and finite meet in a lattice are introduced. Some properties of the finite join are proved. After introducing the concept of dual lattice in view of dualism we obtain analogous properties of the meet. We prove these properties of binary operations in a lattice, which are usually included in axioms of the lattice theory. We also introduce the concept of Heyting lattice (a bounded lattice with relative pseudo-complements).
  27. Grzegorz Bancerek. Consequences of the Reflection Theorem, Formalized Mathematics 1(5), pages 989-993, 1990. MML Identifier: ZFREFLE1
    Summary: Some consequences of the reflection theorem are discussed. To formulate them the notions of elementary equivalence and subsystems, and of models for a set of formulae are introduced. Besides, the concept of cofinality of a ordinal number with second one is used. The consequences of the reflection theorem (it is sometimes called the Scott-Scarpellini lemma) are: (i) If $A_\xi$ is a transfinite sequence as in the reflection theorem (see \cite{ZF_REFLE.ABS}) and $A = \bigcup_{\xi \in On} A_\xi$, then there is an increasing and continuous mapping $\phi$ from $On$ into $On$ such that for every critical number $\kappa$ the set $A_\kappa$ is an elementary subsystem of $A$ ($A_\kappa \prec A$). (ii) There is an increasing continuous mapping $\phi: On \to On$ such that ${\bf R}_\kappa \prec V$ for each of its critical numbers $\kappa$ ($V$ is the universal class and $On$ is the class of all ordinals belonging to $V$). (iii) There are ordinal numbers $\alpha$ cofinal with $\omega$ for which ${\bf R}_\alpha$ are models of ZF set theory. (iv) For each set $X$ from universe $V$ there is a model of ZF $M$ which belongs to $V$ and has $X$ as an element.
Volume 2, 1991
Number 1
  1. Michal Muzalewski. Construction of Rings and Left-, Right-, and Bi-Modules over a Ring, Formalized Mathematics 2(1), pages 3-11, 1991. MML Identifier: VECTSP_2
    Summary: Definitions of some classes of rings and left-, right-, and bi-modules over a ring and some elementary theorems on rings and skew fields.
  2. Eugeniusz Kusak. Desargues Theorem In Projective 3-Space, Formalized Mathematics 2(1), pages 13-16, 1991. MML Identifier: PROJDES1
    Summary: Proof of the Desargues theorem in Fanoian projective at least 3-dimensional space.
  3. Jaroslaw Kotowicz. The Limit of a Real Function at Infinity, Formalized Mathematics 2(1), pages 17-28, 1991. MML Identifier: LIMFUNC1
    Summary:
  4. Jaroslaw Kotowicz. One-Side Limits of a Real Function at a Point, Formalized Mathematics 2(1), pages 29-40, 1991. MML Identifier: LIMFUNC2
    Summary: We introduce the left-side and the right-side limit of a real function at a point. We prove a few properties of the operations on the proper and improper one-side limits and show that Cauchy and Heine characterizations of the one-side limit are equivalent.
  5. Wojciech A. Trybulec. Lattice of Subgroups of a Group. Frattini Subgroup, Formalized Mathematics 2(1), pages 41-47, 1991. MML Identifier: GROUP_4
    Summary: We define the notion of a subgroup generated by a set of element of a group and two closely connected notions. Namely lattice of subgroups and Frattini subgroup. The operations in the lattice are the intersection of subgroups (introduced in \cite{GROUP_2.ABS}) and multiplication of subgroups which result is defined as a subgroup generated by a sum of carriers of the two subgroups. In order to define Frattini subgroup and to prove theorems concerning it we introduce notion of maximal subgroup and non-generating element of the group (see \cite[page 30]{KARGAP:1}). Frattini subgroup is defined as in \cite{KARGAP:1} as an intersection of all maximal subgroups. We show that an element of the group belongs to Frattini subgroup of the group if and only if it is a non-generating element. We also prove theorems that should be proved in \cite{NAT_1.ABS} but are not.
  6. Andrzej Kondracki. Equalities and Inequalities in Real Numbers, Formalized Mathematics 2(1), pages 49-63, 1991. MML Identifier: REAL_2
    Summary: The aim of the article is to give a number of useful theorems concerning equalities and inequalities in real numbers. Some of the theorems are extensions of \cite{REAL_1.ABS} theorems, others were found to be needed in practice.
  7. Grzegorz Bancerek. Countable Sets and Hessenberg's Theorem, Formalized Mathematics 2(1), pages 65-69, 1991. MML Identifier: CARD_4
    Summary: The concept of countable sets is introduced and there are shown some facts which deal with finite and countable sets. Besides, the article includes theorems and lemmas on the sum and product of infinite cardinals. The most important of them is Hessenberg's theorem which says that for every infinite cardinal {\bf m} the product ${\bf m} \cdot {\bf m}$ is equal to {\bf m}.
  8. Jaroslaw Kotowicz. The Limit of a Real Function at a Point, Formalized Mathematics 2(1), pages 71-80, 1991. MML Identifier: LIMFUNC3
    Summary: We define the proper and the improper limit of a real function at a point. The main properties of the operations on the limit of function are proved. The connection between the one-side limits and the limit of function at a point are exposed. Equivalent Cauchy and Heine characterizations of the limit of real function at a point are proved.
  9. Jaroslaw Kotowicz. The Limit of a Composition of Real Functions, Formalized Mathematics 2(1), pages 81-92, 1991. MML Identifier: LIMFUNC4
    Summary: The theorem on the proper and improper limit of a composition of real functions at a point, at infinity and one-side limits at a point are presented.
  10. Beata Padlewska. Locally Connected Spaces, Formalized Mathematics 2(1), pages 93-96, 1991. MML Identifier: CONNSP_2
    Summary: This article is a continuation of \cite{CONNSP_1.ABS}. We define a neighbourhood of a point and a neighbourhood of a set and prove some facts about them. Then the definitions of a locally connected space and a locally connected set are introduced. Some theorems about locally connected spaces are given (based on \cite{KURAT:1}). We also define a quasi-component of a point and prove some of its basic properties.
  11. Michal Muzalewski, Leslaw W. Szczerba. Construction of Finite Sequences over Ring and Left-, Right-, and Bi-Modules over a Ring, Formalized Mathematics 2(1), pages 97-104, 1991. MML Identifier: ALGSEQ_1
    Summary: This text includes definitions of finite sequences over rings and left-, right-, and bi-module over a ring treated as functions defined for {\sl all} natural numbers, but with almost everywhere equal to zero. Some elementary theorems are proved, in particular for each category of sequences the scheme about existence is proved. In all four cases, i.e. for rings, left-, right and bi- modules are almost exactly the same, hovewer we do not know how to do the job in Mizar in a different way. The paper is mostly based on the paper \cite{FINSEQ_1.ABS}. In particular the notion of initial segment of natural numbers is introduced which differs from that of \cite{FINSEQ_1.ABS} by starting with zero. This proved to be more convenient for algebraic purposes.
  12. Krzysztof Hryniewiecki. Relations of Tolerance, Formalized Mathematics 2(1), pages 105-109, 1991. MML Identifier: TOLER_1
    Summary: Introduces notions of relations of tolerance, tolerance set and neighbourhood of an element. The basic properties of relations of tolerance are proved.
  13. Jan Popiolek. Real Normed Space, Formalized Mathematics 2(1), pages 111-115, 1991. MML Identifier: NORMSP_1
    Summary: We construct a real normed space $\langle V,~\Vert.\Vert\rangle$, where $V$ is a real vector space and $\Vert.\Vert$ is a norm. Auxillary properties of the norm are proved. Next, we introduce a notion of sequence in the real normed space. The basic operations on sequences (addition, subtraction, multiplication by real number) are defined. We study some properties of sequences in the real normed space and the operations on them.
  14. Jaroslaw Kotowicz. Schemes of Existence of some Types of Functions, Formalized Mathematics 2(1), pages 117-123, 1991. MML Identifier: SCHEME1
    Summary: We prove some useful schemes of existence of real sequences, partial functions from a domain into a domain, partial functions from a set to a set and functions from a domain into a domain. At the beginning we prove some related auxiliary theorems related to the article \cite{NAT_1.ABS}.
  15. Konrad Raczkowski. Integer and Rational Exponents, Formalized Mathematics 2(1), pages 125-130, 1991. MML Identifier: PREPOWER
    Summary: The article includes definitios and theorems which are needed to define real exponent. The following notions are defined: natural exponent, integer exponent and rational exponent.
  16. Henryk Oryszczyszyn, Krzysztof Prazmowski. Homotheties and Shears in Affine Planes, Formalized Mathematics 2(1), pages 131-133, 1991. MML Identifier: HOMOTHET
    Summary: We study connections between Major Desargues Axiom and the transitivity of group of homotheties. A formal proof of the theorem which establishes an equivalence of these two properties of affine planes is given. We also study connections between trapezium version of Major Desargues Axiom and the existence of the shears in affine planes. The article contains investigations on ``Scherungssatz".
  17. Grzegorz Lewandowski, Krzysztof Prazmowski, Bozena Lewandowska. Directed Geometrical Bundles and Their Analytical Representation, Formalized Mathematics 2(1), pages 135-141, 1991. MML Identifier: AFVECT0
    Summary: We introduce the notion of weak directed geometrical bundle. We prove representation theorems for directed and weak directed geometrical bundles which establishes a one-to-one correspondence between such structures and appropriate 2-divisible abelian groups. To this aim we construct over arbitrary weak directed geometrical bundle a group defined entirely in terms of geometrical notions -- the group of (abstract) ``free vectors".
  18. Grzegorz Bancerek. Definable Functions, Formalized Mathematics 2(1), pages 143-145, 1991. MML Identifier: ZFMODEL2
    Summary: The article is continuation of \cite{ZF_LANG1.ABS} and \cite{ZFMODEL1.ABS}. It deals with concepts of variables occurring in a formula and free variables, replacing of variables in a formula and definable functions. The goal of it is to create a base of facts which are neccesary to show that every model of ZF set theory is a good model, i.e. it is closed with respect to fundamental settheoretical operations (union, intersection, Cartesian product etc.). The base includes the facts concerning with the composition and conditional sum of two definable functions.
  19. Grzegorz Bancerek, Agata Darmochwal, Andrzej Trybulec. Propositional Calculus, Formalized Mathematics 2(1), pages 147-150, 1991. MML Identifier: LUKASI_1
    Summary: We develop the classical propositional calculus, following \cite{LUKA:1}.
  20. Czeslaw Bylinski, Andrzej Trybulec. Complex Spaces, Formalized Mathematics 2(1), pages 151-158, 1991. MML Identifier: COMPLSP1
    Summary: We introduce the concept of $n$-dimensional complex space. We prove a number of simple but useful propositions concerning addition, nultiplication by scalars and similar basic concepts. We introduce metric and topology. We prove that $n$-dimensional complex space is a Hausdorff space and that it is regular.
  21. Jozef Bialas. Several Properties of Fields. Field Theory, Formalized Mathematics 2(1), pages 159-162, 1991. MML Identifier: REALSET3
    Summary: The article includes a continuation of the paper \cite{REALSET2.ABS}. Some simple theorems concerning basic properties of a field are proved.
  22. Jozef Bialas. Infimum and Supremum of the Set of Real Numbers. Measure Theory, Formalized Mathematics 2(1), pages 163-171, 1991. MML Identifier: SUPINF_1
    Summary: We introduce some properties of the least upper bound and the greatest lower bound of the subdomain of $\overline{\Bbb R}$ numbers, where $\overline{\Bbb R}$ denotes the enlarged set of real numbers, $\overline{\Bbb R} = {\Bbb R} \cup \{-\infty,+\infty\}$. The paper contains definitions of majorant and minorant elements, bounded from above, bounded from below and bounded sets, sup and inf of set, for nonempty subset of $\overline{\Bbb R}$. We prove theorems describing the basic relationships among those definitions. The work is the first part of the series of articles concerning the Lebesgue measure theory.
  23. Jozef Bialas. Series of Positive Real Numbers. Measure Theory, Formalized Mathematics 2(1), pages 173-183, 1991. MML Identifier: SUPINF_2
    Summary: We introduce properties of a series of nonnegative $\overline{\Bbb R}$ numbers, where $\overline{\Bbb R}$ denotes the enlarged set of real numbers, $\overline{\Bbb R} = {\Bbb R} \cup \{-\infty,+\infty\}$. The paper contains definition of sup $F$ and inf $F$, for $F$ being function, and a definition of a sumable subset of $\overline{\Bbb R}$. We proved the basic theorems regarding the definitions mentioned above. The work is the second part of a series of articles concerning the Lebesgue measure theory.
  24. Wojciech Skaba, Michal Muzalewski. From Double Loops to Fields, Formalized Mathematics 2(1), pages 185-191, 1991. MML Identifier: ALGSTR_2
    Summary: This paper contains the second part of the set of articles concerning the theory of algebraic structures, based on \cite[pp. 9-12]{SZMIELEW:1} (pages 4--6 of the English edition).\par First the basic structure $\langle F, +, \cdot, 1, 0\rangle$ is defined. Following it the consecutive structures are contemplated in details, including double loop, left quasi-field, right quasi-field, double sided quasi-field, skew field and field. These structures are created by gradually augmenting the basic structure with new axioms of commutativity, associativity, distributivity etc. Each part of the article begins with the set of auxiliary theorems related to the structure under consideration, that are necessary for the existence proof of each defined mode. Next the mode and proof of its existence is included. If the current set of axioms may be replaced with a different and equivalent one, the appropriate proof is performed following the definition of that mode. With the introduction of double loop the ``-'' function is defined. Some interesting features of this function are also included.
Number 2
  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.
Number 3
  1. Henryk Oryszczyszyn, Krzysztof Prazmowski. A construction of analytical Ordered Trapezium Spaces, Formalized Mathematics 2(3), pages 315-322, 1991. MML Identifier: ANALTRAP
    Summary:
  2. Henryk Oryszczyszyn, Krzysztof Prazmowski. A construction of analytical Ordered Trapezium Spaces, Formalized Mathematics 2(3), pages 315-322, 1991. MML Identifier: GEOMTRAP
    Summary: We define, in a given real linear space, the midpoint operation on vectors and, with the help of the notions of directed parallelism of vectors and orthogonality of vectors, we define the relation of directed trapezium. We consider structures being enrichments of affine structures by one binary operation, together with a function which assigns to every such a structure its ``affine" reduct. Theorems concerning midpoint operation and trapezium relation are proved which enables us to introduce an abstract notion of (regular in fact) ordered trapezium space with midpoint, ordered trapezium space, and (unordered) trapezium space.
  3. Eugeniusz Kusak, Wojciech Leonczuk, Krzysztof Prazmowski. On Projections in Projective Planes (Part II ), Formalized Mathematics 2(3), pages 323-329, 1991. MML Identifier: PROJRED2
    Summary: We study in greater details projectivities on Desarguesian projective planes. We are particularly interested in the situation when the composition of given two projectivities can be replaced by another two, with given axis or centre of one of them.
  4. Jolanta Swierzynska, Bogdan Swierzynski. Metric-Affine Configurations in Metric Affine Planes -- Part I, Formalized Mathematics 2(3), pages 331-334, 1991. MML Identifier: CONAFFM
    Summary: We introduce several configurational axioms for metric affine planes such as theorem on three perpendiculars, orthogonalization of major Desargues Axiom, orthogonalization of the trapezium variant of Desargues Axiom, axiom on parallel projection together with its indirect forms. For convenience we also consider affine Major Desargues Axiom. The aim is to prove logical relationships which hold between the introduced statements.
  5. Jolanta Swierzynska, Bogdan Swierzynski. Metric-Affine Configurations in Metric Affine Planes -- Part II, Formalized Mathematics 2(3), pages 335-340, 1991. MML Identifier: CONMETR
    Summary: A continuation of \cite{CONAFFM.ABS}. We introduce more configurational axioms i.e. orthogonalizations of ``scherungssatzes" (direct and indirect), ``Scherungssatz" with orthogonal axes, Pappus axiom with orthogonal axes; we also consider the affine Major Pappus Axiom and affine minor Desargues Axiom. We prove a number of implications which hold between the above axioms.
  6. Krzysztof Prazmowski. Fanoian, Pappian and Desarguesian Affine Spaces, Formalized Mathematics 2(3), pages 341-346, 1991. MML Identifier: PAPDESAF
    Summary: We introduce basic types of affine spaces such as Desarguesian, Fanoian, Pappian, and translation affine and ordered affine sapces and we prove that suitably choosen analytically defined affine structures satisfy the required properties.
  7. Krzysztof Prazmowski, Krzysztof Radziszewski. Elementary Variants of Affine Configurational Theorems, Formalized Mathematics 2(3), pages 347-348, 1991. MML Identifier: PARDEPAP
    Summary: We present elementary versions of Pappus, Major Desargues and Minor Desargues Axioms (i.e. statements formulated entirely in the language of points and parallelity of segments). Evidently they are consequences of appropriate configurational axioms introduced in the article \cite{AFF_2.ABS}. In particular it follows that there exists an affine plane satisfying all of them.
  8. Eugeniusz Kusak, Krzysztof Radziszewski. Semi_Affine Space, Formalized Mathematics 2(3), pages 349-356, 1991. MML Identifier: SEMI_AF1
    Summary: A brief survey on semi-affine geometry, which results from the classical Pappian and Desarguesian affine (dimension free) geometry by weakening the so called trapezium axiom. With the help of the relation of parallelogram in every semi-affine space we define the operation of ``addition" of ``vectors". Next we investigate in greater details the relation of (affine) trapezium in such spaces.
  9. Wojciech Leonczuk, Henryk Oryszczyszyn, Krzysztof Prazmowski. Planes in Affine Spaces, Formalized Mathematics 2(3), pages 357-363, 1991. MML Identifier: AFF_4
    Summary: We introduce the notion of plane in affine space and investigate fundamental properties of them. Further we introduce the relation of parallelism defined for arbitrary subsets. In particular we are concerned with parallelisms which hold between lines and planes and between planes. We also define a function which assigns to every line and every point the unique line passing through the point and parallel to the given line. With the help of the introduced notions we prove that every at least 3-d