Parallelity and Lines in Affine Spaces

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

Parallelity and Lines in Affine Spaces

Henryk Oryszczyszyn: Warsaw University, Bialystok
Krzysztof Prazmowski: Warsaw University, Bialystok

Summary.

In the article we introduce basic notions concerning affine spaces and investigate their fundamental properties. We define the function which to every nondegenerate pair of points assigns the line joining them and we extend the relation of parallelity to a relation between segments and lines, and between lines.

Supported by RPBP.III-24.C2.

MML Identifier: AFF_1

The terminology and notation used in this paper have been introduced in the following articles [3] [1] [2]

Contents (PDF format)

Bibliography

[1] Henryk Oryszczyszyn and Krzysztof Prazmowski. Analytical ordered affine spaces. Journal of Formalized Mathematics, 2, 1990.

[2] Henryk Oryszczyszyn and Krzysztof Prazmowski. Ordered affine spaces defined in terms of directed parallelity --- part I. Journal of Formalized Mathematics, 2, 1990.

[3] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.

Received May 4, 1990

[ Download a postscript version, MML identifier index, Mizar home page]