Formalized Mathematics    (ISSN 0777-4028)
Volume 1, Number 2 (1990): pdf, ps, dvi.
  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.