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