Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990
Association of Mizar Users
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.III24.C6.
The terminology and notation used in this paper have been
introduced in the following articles
[3]
[5]
[6]
[7]
[4]
[2]
[1]
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.
Received October 16, 1990
[
Download a postscript version,
MML identifier index,
Mizar home page]