Analytical Metric Affine Spaces and Planes

Henryk Oryszczyszyn

Warsaw University, Bialystok

Krzysztof Prazmowski

Warsaw University, Bialystok

Summary.

We introduce relations of orthogonality of vectors and of orthogonality of segments (considered as pairs of vectors) in real linear space of dimension two. This enables us to show an example of (in fact anisotropic and satisfying theorem on three perpendiculars) metric affine space (and plane as well). These two types of objects are defined formally as "Mizar" modes. They are to be understood as structures consisting of a point universe and two binary relations on segments - a parallelity relation and orthogonality relation, satisfying appropriate axioms. With every such structure we correlate a structure obtained as a reduct of the given one to the parallelity relation only. Some relationships between metric affine spaces and their affine parts are proved; they enable us to use "affine" facts and constructions in investigating metric affine geometry. We define the notions of line, parallelity of lines and two derived relations of orthogonality: between segments and lines, and between lines. Some basic properties of the introduced notions are proved.

Supported by RPBP.III-24.C2.

MML Identifier: ANALMETR

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

[5] Henryk Oryszczyszyn and Krzysztof Prazmowski. Ordered affine spaces defined in terms of directed parallelity --- part I. Journal of Formalized Mathematics, 2, 1990.

[6] Henryk Oryszczyszyn and Krzysztof Prazmowski. Parallelity and lines in affine spaces. Journal of Formalized Mathematics, 2, 1990.

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

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

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

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

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