Projective Spaces

Wojciech Leonczuk

Warsaw University, Bialystok

Supported by RPBP.III-24.C6.

Krzysztof Prazmowski

Warsaw University, Bialystok

Supported by RPBP.III-24.C2.

Summary.

In the class of all collinearity structures a subclass of (dimension free) projective spaces, defined by means of a suitable axiom system, is singled out. Whenever a real vector space V is at least 3-dimensional, the structure ProjectiveSpace(V) is a projective space in the above meaning. Some narrower classes of projective spaces are defined: Fano projective spaces, projective planes, and Fano projective planes. For any of the above classes an explicit axiom system is given, as well as an analytical example. There is also a construction a of 3-dimensional and a 4-dimensional real vector space; these are needed to show appropriate examples of projective spaces.

MML Identifier: ANPROJ_2

Contents (PDF format)

Bibliography

[1] Czeslaw Bylinski. Binary operations. Journal of Formalized Mathematics, 1, 1989.

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

[3] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.

[4] Wojciech Leonczuk and Krzysztof Prazmowski. A construction of analytical projective space. Journal of Formalized Mathematics, 2, 1990.

[5] Henryk Oryszczyszyn and Krzysztof Prazmowski. Real functions spaces. Journal of Formalized Mathematics, 2, 1990.

[6] Wojciech Skaba. The collinearity structure. 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] Andrzej Trybulec. Function domains and Fr\aenkel operator. Journal of Formalized Mathematics, 2, 1990.

[10] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.

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

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