Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990
Association of Mizar Users
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.III24.C6.
MML Identifier:
ANALOAF
The terminology and notation used in this paper have been
introduced in the following articles
[5]
[2]
[4]
[3]
[7]
[6]
[1]
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.
Received April 11, 1990
[
Download a postscript version,
MML identifier index,
Mizar home page]