VOLUME 2, NUMBER 1 (1991), Formalized Mathematics, ISSN 0777-4028

Formalized Mathematics (ISSN 0777-4028)
Volume 2, Number 1 (1991): pdf, ps, dvi.

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.
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.
Jaroslaw Kotowicz. The Limit of a Real Function at Infinity, Formalized Mathematics 2(1), pages 17-28, 1991. MML Identifier: LIMFUNC1
Summary:
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.
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.
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.
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}.
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.
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.
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.
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.
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.
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.
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}.
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.
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".
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".
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.
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}.
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.
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.
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.
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.
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.