Analytical Ordered Affine Spaces

Henryk Oryszczyszyn

Warsaw University, Bialystok

Krzysztof Prazmowski

Warsaw University, Bialystok

Summary.

In the article with a given arbitrary real linear space we correlate the (ordered) affine space defined in terms of a directed parallelity of segments. The abstract contains a construction of the ordered affine structure associated with a vector space; this is a structure of the type which frequently occurs in geometry and consists of the set of points and a binary relation on segments. For suitable underlying vector spaces we prove that the corresponding affine structures are ordered affine spaces or ordered affine planes, i.e. that they satisfy appropriate axioms. A formal definition of an arbitrary ordered affine space and an arbitrary ordered affine plane is given.

Supported by RPBP.III-24.C6.

MML Identifier: ANALOAF

Contents (PDF format)

Bibliography

[1] Jozef Bialas. Group and field definitions. Journal of Formalized Mathematics, 1, 1989.

[2] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.

[3] Krzysztof Hryniewiecki. Basic properties of real numbers. Journal of Formalized Mathematics, 1, 1989.

[4] Andrzej Trybulec. Domains and their Cartesian products. Journal of Formalized Mathematics, 1, 1989.

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

[6] Wojciech A. Trybulec. Vectors in real linear space. Journal of Formalized Mathematics, 1, 1989.

[7] Edmund Woronowicz. Relations defined on sets. Journal of Formalized Mathematics, 1, 1989.