Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990
Association of Mizar Users
Translations in Affine Planes

Henryk Oryszczyszyn

Warsaw University, Bialystok

Krzysztof Prazmowski

Warsaw University, Bialystok
Summary.

Connections between Minor Desargues Axiom and
the transitivity of translation groups are investigated.
A formal proof of the theorem
which establishes the equivalence of these two properties of affine
planes is given. We also prove that, under additional requirement,
the plane in question satisfies Fano Axiom; its translation group is
uniquely twodivisible.
Supported by RPBP.III24.C2.
The terminology and notation used in this paper have been
introduced in the following articles
[2]
[1]
[3]
[5]
[6]
[4]
[7]
Contents (PDF format)
Bibliography
 [1]
Czeslaw Bylinski.
Functions from a set to a set.
Journal of Formalized Mathematics,
1, 1989.
 [2]
Czeslaw Bylinski.
Partial functions.
Journal of Formalized Mathematics,
1, 1989.
 [3]
Henryk Oryszczyszyn and Krzysztof Prazmowski.
Analytical ordered affine spaces.
Journal of Formalized Mathematics,
2, 1990.
 [4]
Henryk Oryszczyszyn and Krzysztof Prazmowski.
Classical configurations in affine planes.
Journal of Formalized Mathematics,
2, 1990.
 [5]
Henryk Oryszczyszyn and Krzysztof Prazmowski.
Ordered affine spaces defined in terms of directed parallelity  part I.
Journal of Formalized Mathematics,
2, 1990.
 [6]
Henryk Oryszczyszyn and Krzysztof Prazmowski.
Parallelity and lines in affine spaces.
Journal of Formalized Mathematics,
2, 1990.
 [7]
Henryk Oryszczyszyn and Krzysztof Prazmowski.
Transformations in affine spaces.
Journal of Formalized Mathematics,
2, 1990.
Received June 12, 1990
[
Download a postscript version,
MML identifier index,
Mizar home page]