Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990
Association of Mizar Users
A Construction of Analytical Ordered Trapezium Spaces

Henryk Oryszczyszyn

Warsaw University, Bialystok

Krzysztof Prazmowski

Warsaw University, Bialystok
Summary.

We define, in a given real linear space, the midpoint
operation on vectors and, with the help of the notions of directed
parallelism of vectors and orthogonality of vectors, we define the
relation of directed trapezium. We consider structures being enrichments
of affine structures by one binary operation, together with a function
which assigns to every such a structure its ``affine" reduct.
Theorems concerning midpoint operation and trapezium relation are proved
which enables us to introduce an abstract notion of (regular in fact)
ordered trapezium space with midpoint, ordered trapezium space, and
(unordered) trapezium space.
Supported by RPBP.III24.C2.
The terminology and notation used in this paper have been
introduced in the following articles
[9]
[2]
[11]
[8]
[3]
[7]
[12]
[10]
[4]
[6]
[1]
[5]
Contents (PDF format)
Bibliography
 [1]
Czeslaw Bylinski.
Binary operations.
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]
Michal Muzalewski.
Midpoint algebras.
Journal of Formalized Mathematics,
1, 1989.
 [5]
Henryk Oryszczyszyn and Krzysztof Prazmowski.
Analytical metric affine spaces and planes.
Journal of Formalized Mathematics,
2, 1990.
 [6]
Henryk Oryszczyszyn and Krzysztof Prazmowski.
Analytical ordered affine spaces.
Journal of Formalized Mathematics,
2, 1990.
 [7]
Henryk Oryszczyszyn and Krzysztof Prazmowski.
Ordered affine spaces defined in terms of directed parallelity  part I.
Journal of Formalized Mathematics,
2, 1990.
 [8]
Andrzej Trybulec.
Domains and their Cartesian products.
Journal of Formalized Mathematics,
1, 1989.
 [9]
Andrzej Trybulec.
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Axiomatics, 1989.
 [10]
Wojciech A. Trybulec.
Vectors in real linear space.
Journal of Formalized Mathematics,
1, 1989.
 [11]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
 [12]
Edmund Woronowicz.
Relations defined on sets.
Journal of Formalized Mathematics,
1, 1989.
Received October 29, 1990
[
Download a postscript version,
MML identifier index,
Mizar home page]