Journal of Formalized Mathematics, Volume 2, 1990

Table of contents

  1. Function Domains and Fr\aenkel Operator
    by Andrzej Trybulec
  2. Integers
    by Michal J. Trybulec
  3. The Complex Numbers
    by Czeslaw Bylinski
  4. Ordinal Arithmetics
    by Grzegorz Bancerek
  5. The Modification of a Function by a Function and the Iteration of the Composition of a Function
    by Czeslaw Bylinski
  6. Finite Sequences and Tuples of Elements of a Non-empty Sets
    by Czeslaw Bylinski
  7. Curried and Uncurried Functions
    by Grzegorz Bancerek
  8. Cardinal Arithmetics
    by Grzegorz Bancerek
  9. Fano-Desargues Parallelity Spaces
    by Eugeniusz Kusak and Wojciech Leonczuk
  10. Real Functions Spaces
    by Henryk Oryszczyszyn and Krzysztof Prazmowski
  11. Tarski's Classes and Ranks
    by Grzegorz Bancerek
  12. Non-contiguous Substrings and One-to-one Finite Sequences
    by Wojciech A. Trybulec
  13. Pigeon Hole Principle
    by Wojciech A. Trybulec
  14. Linear Combinations in Real Linear Space
    by Wojciech A. Trybulec
  15. K\"onig's Theorem
    by Grzegorz Bancerek
  16. Universal Classes
    by Bogdan Nowak and Grzegorz Bancerek
  17. Analytical Ordered Affine Spaces
    by Henryk Oryszczyszyn and Krzysztof Prazmowski
  18. Metric Spaces
    by Stanislawa Kanas, Adam Lecko, and Mariusz Startek
  19. Ordered Affine Spaces Defined in Terms of Directed Parallelity - Part I
    by Henryk Oryszczyszyn and Krzysztof Prazmowski
  20. Parallelity and Lines in Affine Spaces
    by Henryk Oryszczyszyn and Krzysztof Prazmowski
  21. Classical Configurations in Affine Planes
    by Henryk Oryszczyszyn and Krzysztof Prazmowski
  22. Affine Localizations of Desargues Axiom
    by Eugeniusz Kusak, Henryk Oryszczyszyn, and Krzysztof Prazmowski
  23. Binary Operations Applied to Finite Sequences
    by Czeslaw Bylinski
  24. Semigroup Operations on Finite Subsets
    by Czeslaw Bylinski
  25. The Collinearity Structure
    by Wojciech Skaba
  26. The Sum and Product of Finite Sequences of Real Numbers
    by Czeslaw Bylinski
  27. A Classical First Order Language
    by Czeslaw Bylinski
  28. Classical and Non-classical Pasch Configurations in Ordered Affine Planes
    by Henryk Oryszczyszyn, Krzysztof Prazmowski, and Malgorzata Prazmowska
  29. The Lattice of Real Numbers. The Lattice of Real Functions
    by Marek Chmur
  30. A Construction of an Abstract Space of Congruence of Vectors
    by Grzegorz Lewandowski and Krzysztof Prazmowski
  31. A First-Order Predicate Calculus
    by Agata Darmochwal
  32. Partial Functions from a Domain to a Domain
    by Jaroslaw Kotowicz
  33. Partial Functions from a Domain to the Set of Real Numbers
    by Jaroslaw Kotowicz
  34. Increasing and Continuous Ordinal Sequences
    by Grzegorz Bancerek
  35. Transformations in Affine Spaces
    by Henryk Oryszczyszyn and Krzysztof Prazmowski
  36. Subcategories and Products of Categories
    by Czeslaw Bylinski
  37. Many-Argument Relations
    by Edmund Woronowicz
  38. Interpretation and Satisfiability in the First Order Logic
    by Edmund Woronowicz
  39. Probability
    by Andrzej Nedzusiak
  40. Translations in Affine Planes
    by Henryk Oryszczyszyn and Krzysztof Prazmowski
  41. Introduction to Probability
    by Jan Popiolek
  42. A Construction of Analytical Projective Space
    by Wojciech Leonczuk and Krzysztof Prazmowski
  43. Projective Spaces
    by Wojciech Leonczuk and Krzysztof Prazmowski
  44. Topological Properties of Subsets in Real Numbers
    by Konrad Raczkowski and Pawel Sadowski
  45. Properties of Real Functions
    by Jaroslaw Kotowicz
  46. Real Function Continuity
    by Konrad Raczkowski and Pawel Sadowski
  47. Real Function Uniform Continuity
    by Jaroslaw Kotowicz and Konrad Raczkowski
  48. Real Function Differentiability
    by Konrad Raczkowski and Pawel Sadowski
  49. Average Value Theorems for Real Functions of One Variable
    by Jaroslaw Kotowicz, Konrad Raczkowski, and Pawel Sadowski
  50. Construction of Rings and Left-, Right-, and Bi-Modules over a Ring
    by Michal Muzalewski
  51. Properties of Fields
    by Jozef Bialas
  52. Filters - Part I. Implicative Lattices
    by Grzegorz Bancerek
  53. Groups
    by Wojciech A. Trybulec
  54. The Divisibility of Integers and Integer Relatively Primes
    by Rafal Kwiatek and Grzegorz Zwara
  55. From Loops to Abelian Multiplicative Groups with Zero
    by Michal Muzalewski and Wojciech Skaba
  56. Basic Properties of Rational Numbers
    by Andrzej Kondracki
  57. Basis of Real Linear Space
    by Wojciech A. Trybulec
  58. Finite Sums of Vectors in Vector Space
    by Wojciech A. Trybulec
  59. Subgroup and Cosets of Subgroups
    by Wojciech A. Trybulec
  60. Subspaces and Cosets of Subspaces in Vector Space
    by Wojciech A. Trybulec
  61. Operations on Subspaces in Vector Space
    by Wojciech A. Trybulec
  62. Linear Combinations in Vector Space
    by Wojciech A. Trybulec
  63. Basis of Vector Space
    by Wojciech A. Trybulec
  64. Factorial and Newton Coeffitients
    by Rafal Kwiatek
  65. Analytical Metric Affine Spaces and Planes
    by Henryk Oryszczyszyn and Krzysztof Prazmowski
  66. Some Elementary Notions of the Theory of Petri Nets
    by Waldemar Korczynski
  67. Classes of Conjugation. Normal Subgroups
    by Wojciech A. Trybulec
  68. Replacing of Variables in Formulas of ZF Theory
    by Grzegorz Bancerek
  69. The Reflection Theorem
    by Grzegorz Bancerek
  70. Binary Operations on Finite Sequences
    by Wojciech A. Trybulec
  71. Finite Join and Finite Meet, and Dual Lattices
    by Andrzej Trybulec
  72. Consequences of the Reflection Theorem
    by Grzegorz Bancerek
  73. Desargues Theorem In Projective 3-Space
    by Eugeniusz Kusak
  74. The Limit of a Real Function at Infinity
    by Jaroslaw Kotowicz
  75. The One-Side Limits of a Real Function at a Point
    by Jaroslaw Kotowicz
  76. Lattice of Subgroups of a Group. Frattini Subgroup
    by Wojciech A. Trybulec
  77. Equalities and Inequalities in Real Numbers
    by Andrzej Kondracki
  78. Countable Sets and Hessenberg's Theorem
    by Grzegorz Bancerek
  79. The Limit of a Real Function at a Point
    by Jaroslaw Kotowicz
  80. The Limit of a Composition of Real Functions
    by Jaroslaw Kotowicz
  81. Locally Connected Spaces
    by Beata Padlewska
  82. Construction of Finite Sequence over Ring and Left-, Right-, and Bi-Modules over a Ring
    by Michal Muzalewski and Leslaw W. Szczerba
  83. Relations of Tolerance
    by Krzysztof Hryniewiecki
  84. Real Normed Space
    by Jan Popiolek
  85. Schemes of Existence of Some Types of Functions
    by Jaroslaw Kotowicz
  86. Integer and Rational Exponents
    by Konrad Raczkowski
  87. Homotheties and Shears in Affine Planes
    by Henryk Oryszczyszyn and Krzysztof Prazmowski
  88. Directed Geometrical Bundles and Their Analytical Representation
    by Grzegorz Lewandowski, Krzysztof Prazmowski, and Bozena Lewandowska
  89. Definable Functions
    by Grzegorz Bancerek
  90. Propositional Calculus
    by Grzegorz Bancerek, Agata Darmochwal, and Andrzej Trybulec
  91. Complex Spaces
    by Czeslaw Bylinski and Andrzej Trybulec
  92. Several Pepoerties of Fields. Field Theory
    by Jozef Bialas
  93. Infimum and Supremum of the Set of Real Numbers. Measure Theory
    by Jozef Bialas
  94. Series of Positive Real Numbers. Measure Theory
    by Jozef Bialas
  95. From Double Loops to Fields
    by Wojciech Skaba and Michal Muzalewski
  96. Metrics in Cartesian Product
    by Stanislawa Kanas and Jan Stankiewicz
  97. Submetric Spaces - Part I
    by Adam Lecko and Mariusz Startek
  98. On Pseudometric Spaces
    by Adam Lecko and Mariusz Startek
  99. Real Exponents and Logarithms
    by Konrad Raczkowski and Andrzej Nedzusiak
  100. Hessenberg Theorem
    by Eugeniusz Kusak and Wojciech Leonczuk
  101. Three-Argument Operations and Four-Argument Operations
    by Michal Muzalewski and Wojciech Skaba
  102. Incidence Projective Spaces
    by Wojciech Leonczuk and Krzysztof Prazmowski
  103. One-Dimensional Congruence of Segments, Basic Facts and Midpoint Relation
    by Barbara Konstanta, Urszula Kowieska, Grzegorz Lewandowski, and Krzysztof Prazmowski
  104. Algebra of Normal Forms
    by Andrzej Trybulec
  105. Ordered Rings - Part I
    by Michal Muzalewski and Leslaw W. Szczerba
  106. Ordered Rings - Part II
    by Michal Muzalewski and Leslaw W. Szczerba
  107. Ordered Rings - Part III
    by Michal Muzalewski and Leslaw W. Szczerba
  108. $N$-Tuples and Cartesian Products for $n=5$
    by Michal Muzalewski and Wojciech Skaba
  109. $N$-Tuples and Cartesian Products for $n=6$
    by Michal Muzalewski and Wojciech Skaba
  110. $N$-Tuples and Cartesian Products for $n=7$
    by Michal Muzalewski and Wojciech Skaba
  111. $N$-Tuples and Cartesian Products for $n=8$
    by Michal Muzalewski and Wojciech Skaba
  112. $N$-Tuples and Cartesian Products for $n=9$
    by Michal Muzalewski and Wojciech Skaba
  113. Ternary Fields
    by Michal Muzalewski and Wojciech Skaba
  114. The $\sigma$-additive Measure Theory
    by Jozef Bialas
  115. Incidence Projective Space ( a reduction theorem in a plane)
    by Eugeniusz Kusak and Wojciech Leonczuk
  116. Groups, Rings, Left- and Right-Modules
    by Michal Muzalewski and Wojciech Skaba
  117. Linear Independence in Left Module over Domain
    by Michal Muzalewski and Wojciech Skaba
  118. Submodules and Cosets of Submodules in Right Module over Associative Ring
    by Michal Muzalewski and Wojciech Skaba
  119. Operations on Submodules in Right Module over Associative Ring
    by Michal Muzalewski and Wojciech Skaba
  120. Linear Combinations in Right Module over Associative Ring
    by Michal Muzalewski and Wojciech Skaba
  121. Linear Independence in Right Module over Domain
    by Michal Muzalewski and Wojciech Skaba
  122. Calculus of Propositions
    by Jan Popiolek and Andrzej Trybulec
  123. Calculus of Quantifiers. Deduction Theorem
    by Agata Darmochwal
  124. A Construction of Analytical Ordered Trapezium Spaces
    by Henryk Oryszczyszyn and Krzysztof Prazmowski
  125. On Projections in Projective Planes - Part II
    by Eugeniusz Kusak, Wojciech Leonczuk, and Krzysztof Prazmowski
  126. Metric-Affine Configurations in Metric Affine Planes - Part I
    by Jolanta Swierzynska and Bogdan Swierzynski
  127. Metric-Affine Configurations in Metric Affine Planes - Part II
    by Jolanta Swierzynska and Bogdan Swierzynski
  128. Fanoian, Pappian and Desarguesian Affine Spaces
    by Krzysztof Prazmowski
  129. Elementary Variants of Affine Configurational Theorems
    by Krzysztof Prazmowski and Krzysztof Radziszewski
  130. Semi-Affine Space
    by Eugeniusz Kusak and Krzysztof Radziszewski
  131. Planes in Affine Spaces
    by Wojciech Leonczuk, Henryk Oryszczyszyn, and Krzysztof Prazmowski
  132. Graphs
    by Krzysztof Hryniewiecki
  133. Mostowski's Fundamental Operations - Part I
    by Andrzej Kondracki
  134. A Projective Closure and Projective Horizon of an Affine Space
    by Henryk Oryszczyszyn and Krzysztof Prazmowski
  135. Schemes
    by Stanislaw T. Czuba

[MML identifier index, Mizar home page]