One-Dimensional Congruence of Segments, Basic Facts and Midpoint Relation

Barbara Konstanta

Siedlce Agricultural, and Pedagogical University

Urszula Kowieska

Siedlce Agricultural, and Pedagogical University

Grzegorz Lewandowski

Siedlce Agricultural, and Pedagogical University

Krzysztof Prazmowski

Warsaw University, Bialystok

Summary.

We study a theory of one-dimensional congruence of segments. The theory is characterized by a suitable formal axiom system; as a model of this system one can take the structure obtained from any weak directed geometrical bundle, with the congruence interpreted as in the case of ``classical" vectors. Preliminary consequences of our axiom system are proved, basic relations of maximal distance and of midpoint are defined, and several fundamental properties of them are established.

Supported by RPBP.III-24.C3.

MML Identifier: AFVECT01

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

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

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

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