Incidence Projective Space (a reduction theorem in a plane)

Eugeniusz Kusak

Warsaw University, Bialystok

Wojciech Leonczuk

Warsaw University, Bialystok

Summary.

The article begins with basic facts concerning arbitrary projective spaces. Further we are concerned with Fano projective spaces (we prove it has rank at least four). Finally we restrict ourselves to Desarguesian planes; we define the notion of perspectivity and we prove the reduction theorem for projectivities with concurrent axes.

Supported by RPBP.III-24.C6.

MML Identifier: PROJRED1

Contents (PDF format)

Bibliography

[1] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[2] Wojciech Leonczuk and Krzysztof Prazmowski. Incidence projective spaces. Journal of Formalized Mathematics, 2, 1990.

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

[4] Wojciech A. Trybulec. Axioms of incidency. Journal of Formalized Mathematics, 1, 1989.

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

[6] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.

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