Formalized Mathematics    (ISSN 0777-4028)
Volume 2, Number 3 (1991): pdf, ps, dvi.
  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-dimensional affine space is Desarguesian and translation.
  10. Krzysztof Hryniewiecki. Graphs, Formalized Mathematics 2(3), pages 365-370, 1991. MML Identifier: GRAPH_1
    Summary: Definitions of graphs are introduced and their basic properties are proved. The following notions related to graph theory are introduced: subgraph, finite graph, chain and oriented chain - as a finite sequence of edges, path and oriented path - as a finite sequence of different edges, cycle and oriented cycle, incidency of graph's vertices, a sum of two graphs, a degree of a vertice, a set of all subgraphs of a graph. Many ideas of this article have been taken from \cite{Wilson}.
  11. Andrzej Kondracki. Mostowski's Fundamental Operations -- Part I, Formalized Mathematics 2(3), pages 371-375, 1991. MML Identifier: ZF_FUND1
    Summary: In the chapter II.4 of his book \cite {MOST:1} A.~Mostowski introduces what he calls fundamental operations:\\ \indent $A_{1}(a,b)=\lbrace\lbrace\langle0,x\rangle,\langle1,y\rangle\rbrace: x\in y \wedge x\in a \wedge y\in a \rbrace$,\\ \indent $A_{2}(a,b)=\lbrace a,b\rbrace$,\\ \indent $A_{3}(a,b)=\bigcup a$,\\ \indent $A_{4}(a,b)=\lbrace\lbrace\langle x,y\rangle\rbrace: x\in a \wedge y\in b \rbrace$,\\ \indent $A_{5}(a,b)=\lbrace x\cup y : x\in a \wedge y\in b \rbrace$,\\ \indent $A_{6}(a,b)=\lbrace x\setminus y : x\in a \wedge y\in b \rbrace$,\\ \indent $A_{7}(a,b)=\lbrace x\circ y : x\in a \wedge y\in b \rbrace$.\\ He proves that if a non-void class is closed under these operations then it is predicatively closed. Then he formulates sufficient criteria for a class to be a model of ZF set theory (theorem 4.12). \par The article includes the translation of this part of Mostowski's book. The fundamental operations are defined (to be precise not these operations, but the notions of closure of a class with respect to them). Some properties of classes closed under these operations are proved. At last it is proved that if a non-void class $X$ is closed with respect to the operations $A_{1}-A_{7}$ then $D_{H}(a)\in X$ for every $a$ in $X$ and every $H$ being formula of ZF language ($D_{H}(a)$ consists of all finite sequences with terms belonging to $a$ which satisfy $H$ in $a$).
  12. Henryk Oryszczyszyn, Krzysztof Prazmowski. A Projective Closure and Projective Horizon of an Affine Space, Formalized Mathematics 2(3), pages 377-384, 1991. MML Identifier: AFPROJ
    Summary: With every affine space $A$ we correlate two incidence structures. The first, called Inc-ProjSp($A$), is the usual projective closure of $A$, i.e. the structure obtained from $A$ by adding directions of lines and planes of $A$. The second, called projective horizon of $A$, is the structure built from directions. We prove that Inc-ProjSp($A$) is always a projective space, and projective horizon of $A$ is a projective space provided $A$ is at least 3-dimensional. Some evident relationships between projective and affine configurational axioms that may hold in $A$ and in Inc-ProjSp($A$) are established.
  13. Stanislaw T. Czuba. Schemes, Formalized Mathematics 2(3), pages 385-391, 1991. MML Identifier: SCHEMS_1
    Summary: Some basic schemes of quantifier calculus are proved.
  14. Andrzej Trybulec. Algebra of Normal Forms Is a Heyting Algebra, Formalized Mathematics 2(3), pages 393-396, 1991. MML Identifier: HEYTING1
    Summary: We prove that the lattice of normal forms over an arbitrary set, introduced in \cite{NORMFORM.ABS}, is an implicative lattice. The relative pseudo-complement $\alpha\Rightarrow\beta$ is defined as $\bigsqcup_{\alpha_1\cup\alpha_2=\alpha}-\alpha_1\sqcap \alpha_2\rightarrowtail\beta$, where $-\alpha$ is the pseudo-complement of $\alpha$ and $\alpha\rightarrowtail\beta$ is a rather strong implication introduced in this paper.
  15. Grzegorz Bancerek. K\"onig's Lemma, Formalized Mathematics 2(3), pages 397-402, 1991. MML Identifier: TREES_2
    Summary: A continuation of \cite{TREES_1.ABS}. The notion of finite--order trees, succesors of an element of a tree, and chains, levels and branches of a tree are introduced. That notion has been used to formalize K\"onig's Lemma which claims that there is a infinite branch of a finite-order tree if the tree has arbitrary long finite chains. Besides, the concept of decorated trees is introduced and some concepts dealing with trees are applied to decorated trees.
  16. Jaroslaw Kotowicz. Monotonic and Continuous Real Function, Formalized Mathematics 2(3), pages 403-405, 1991. MML Identifier: FCONT_3
    Summary: A continuation of \cite{FCONT_1.ABS} and \cite{FCONT_2.ABS}. We prove a few theorems about real functions monotonic and continuous on interval, on halfline and on the set of real numbers and continuity of the inverse function. At the beginning of the paper we show some facts about topological properties of the set of real numbers, halflines and intervals which rather belong to \cite{RCOMP_1.ABS}.
  17. Jaroslaw Kotowicz, Konrad Raczkowski. Real Function Differentiability -- Part II, Formalized Mathematics 2(3), pages 407-411, 1991. MML Identifier: FDIFF_2
    Summary: A continuation of \cite{FDIFF_1.ABS}. We prove equivalent definition of the derivative of the real function at the point and theorems about derivative of composite functions, inverse function and derivative of quotient of two functions. At the beginning of the paper a few facts which rather belong to \cite{SEQ_2.ABS}, \cite{SEQM_3.ABS} and \cite{SEQ_4.ABS} are proved.
  18. Wojciech Zielonka. Preliminaries to the Lambek calculus, Formalized Mathematics 2(3), pages 413-418, 1991. MML Identifier: PRELAMB
    Summary: Some preliminary facts concerning completeness and decidability problems for the Lambek Calculus \cite{LAMBEK:1} are proved as well as some theses and derived rules of the calculus itself.
  19. Czeslaw Bylinski. Opposite Categories and Contravariant Functors, Formalized Mathematics 2(3), pages 419-424, 1991. MML Identifier: OPPCAT_1
    Summary: The opposite category of a category, contravariant functors and duality functors are defined.
  20. Grzegorz Bancerek, Andrzej Kondracki. Mostowski's Fundamental Operations -- Part II, Formalized Mathematics 2(3), pages 425-427, 1991. MML Identifier: ZF_FUND2
    Summary: The article consists of two parts. The first part is translation of chapter II.3 of \cite{MOST:1}. A section of $D_{H}(a)$ determined by $f$ (symbolically $S_{H}(a,f)$) and a notion of predicative closure of a class are defined. It is proved that if following assumptions are satisfied: (o) $A=\bigcup_{\xi}A_{\xi}$, (i) $A_{\xi} \subset A_{\eta}$ for $\xi < \eta$, (ii) $A_{\lambda}=\bigcup_{\xi<\lambda}A_{\lambda}$ ($\lambda$ is a limit number), (iii) $A_{\xi}\in A$, (iv) $A_{\xi}$ is transitive, (v) $(x,y\in A) \rightarrow (x\cap y\in A)$, (vi) $A$ is predicatively closed, then the axiom of power sets and the axiom of substitution are valid in $A$. The second part is continuation of \cite{ZF_FUND1.ABS}. It is proved that if a non-void, transitive class is closed with respect to the operations $A_{1}-A_{7}$ then it is predicatively closed. At last sufficient criteria for a class to be a model of ZF-theory are formulated: if $A_{\xi}$ satisfies o -- iv and $A$ is closed under the operations $A_{1}-A_{7}$ then $A$ is a model of ZF.
  21. Henryk Oryszczyszyn, Krzysztof Prazmowski. Fundamental Types of Metric Affine Spaces, Formalized Mathematics 2(3), pages 429-432, 1991. MML Identifier: EUCLMETR
    Summary: We distinguish in the class of metric affine spaces some fundamental types of them. First we can assume the underlying affine space to satisfy classical affine configurational axiom; thus we come to Pappian, Desarguesian, Moufangian, and translation spaces. Next we distinguish the spaces satisfying theorem on three perpendiculars and the homogeneous spaces; these properties directly refer to some axioms involving orthogonality. Some known relationships between the introduced classes of structures are established. We also show that the commonly investigated models of metric affine geometry constructed in a real linear space with the help of a symmetric bilinear form belong to all the classes introduced in the paper.
  22. Grzegorz Bancerek. Filters -- Part II. Quotient Lattices Modulo Filters and Direct Product of Two Lattices, Formalized Mathematics 2(3), pages 433-438, 1991. MML Identifier: FILTER_1
    Summary: Binary and unary operation preserving binary relations and quotients of those operations modulo equivalence relations are introduced. It is shown that the quotients inherit some important properties (commutativity, associativity, distributivity, etc.). Based on it, the quotient (also called factor) lattice modulo a filter (i.e. modulo the equivalence relation w.r.t the filter) is introduced. Similarly, some properties of the direct product of two binary (unary) operations are present and then the direct product of two lattices is introduced. Besides, the heredity of distributivity, modularity, completeness, etc., for the product of lattices is also shown. Finally, the concept of isomorphic lattices is introduced, and there is shown that every Boolean lattice $B$ is isomorphic with the direct product of the factor lattice $B/[a]$ and the lattice latt$[a]$, where $a$ is an element of $B$.
  23. Jolanta Swierzynska, Bogdan Swierzynski. Shear Theorems and their role in Affine Geometry, Formalized Mathematics 2(3), pages 439-444, 1991. MML Identifier: CONMETR1
    Summary: Investigations on affine shear theorems, major and minor, direct and indirect. We prove logical relationships which hold between these statements and between them and other classical affine configurational axioms (eg. minor and major Pappus Axiom, Desargues Axioms et al.). For the shear, Desargues, and Pappus Axioms formulated in terms of metric affine spaces we prove they are equivalent to corresponding statements formulated in terms of affine reduct of the given space.