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.III24.C6.

Krzysztof Prazmowski

Warsaw University, Bialystok

Supported by RPBP.III24.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
3dimensional, 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 3dimensional and
a 4dimensional real vector space; these are needed to show appropriate
examples of projective spaces.
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.
Received June 15, 1990
[
Download a postscript version,
MML identifier index,
Mizar home page]