Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992 Association of Mizar Users

## Reper Algebras

Michal Muzalewski
Warsaw University, Bialystok

### Summary.

We shall describe $n$-dimensional spaces with the reper operation [7, pages 72-79]. An inspiration to such approach comes from the monograph  and so-called Leibniz program. Let us recall that the Leibniz program is a program of algebraization of geometry using purely geometric notions. Leibniz formulated his program in opposition to algebraization method developed by Descartes. The Euclidean geometry in Szmielew's approach  {SZMIELEW:1} is a theory of structures $\langle S$; $\parallel, \oplus, O \rangle$, where $\langle S$; $\parallel, \oplus, O \rangle$ is Desarguesian midpoint plane and $O \subseteq S\times S\times S$ is the relation of equi-orthogonal basis. Points $o, p, q$ are in relation $O$ if they form an isosceles triangle with the right angle in vertex $a$. If we fix vertices $a, p$, then there exist exactly two points $q, q'$ such that $O(apq)$, $O(apq')$. Moreover $q \oplus q' = a$. In accordance with the Leibniz program we replace the relation of equi-orthogonal basis by a binary operation $\ast : S\times S \rightarrow S$, called the reper operation. A standard model for the Euclidean geometry in the above sense is the oriented plane over the field of real numbers with the reper operations $\ast$ defined by the condition: $a \ast b = q$ iff the point $q$ is the result of rotating of $p$ about right angle around the center $a$.

#### MML Identifier: MIDSP_3

The terminology and notation used in this paper have been introduced in the following articles          

#### Contents (PDF format)

1. Substitutions in tuples
2. Reper Algebra Structure and its Properties
3. Reper Algebra and its Atlas

#### Bibliography

 Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.
 Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Journal of Formalized Mathematics, 1, 1989.
 Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
 Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
 Czeslaw Bylinski. Finite sequences and tuples of elements of a non-empty sets. Journal of Formalized Mathematics, 2, 1990.
 Michal Muzalewski. Midpoint algebras. Journal of Formalized Mathematics, 1, 1989.
 Michal Muzalewski. \em Foundations of Metric-Affine Geometry. Dzial Wydawnictw Filii UW w Bialymstoku, Filia UW w Bialymstoku, 1990.
 Michal Muzalewski. Atlas of midpoint algebra. Journal of Formalized Mathematics, 3, 1991.
 Wanda Szmielew. \em From Affine to Euclidean Geometry, volume 27. PWN -- D.Reidel Publ. Co., Warszawa -- Dordrecht, 1983.
 Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
 Wojciech A. Trybulec. Vectors in real linear space. Journal of Formalized Mathematics, 1, 1989.
 Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.