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.III-24.C2.

MML Identifier: GEOMTRAP

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.