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 two-divisible.

Supported by RPBP.III-24.C2.

MML Identifier: TRANSLAC

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]