Planes in Affine Spaces

Wojciech Leonczuk

Warsaw University, Bialystok

Henryk Oryszczyszyn

Warsaw University, Bialystok

Krzysztof Prazmowski

Warsaw University, Bialystok

Summary.

We introduce the notion of plane in affine space and investigate fundamental properties of them. Further we introduce the relation of parallelism defined for arbitrary subsets. In particular we are concerned with parallelisms which hold between lines and planes and between planes. We also define a function which assigns to every line and every point the unique line passing through the point and parallel to the given line. With the help of the introduced notions we prove that every at least 3-dimensional affine space is Desarguesian and translation.

Supported by RPBP.III-24.C2.

MML Identifier: AFF_4

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] Henryk Oryszczyszyn and Krzysztof Prazmowski. Parallelity and lines in affine spaces. Journal of Formalized Mathematics, 2, 1990.

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

[5] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.