Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

## 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

The terminology and notation used in this paper have been introduced in the following articles [8] [12] [10] [2] [3] [1] [7] [11] [9] [5] [6] [4]

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.