Projective Geometry

Title:	Projective Geometry
Author:	Anthony Bordg
Submission date:	2018-06-14
Abstract:	We formalize the basics of projective geometry. In particular, we give a proof of the so-called Hessenberg's theorem in projective plane geometry. We also provide a proof of the so-called Desargues's theorem based on an axiomatization of (higher) projective space geometry using the notion of rank of a matroid. This last approach allows to handle incidence relations in an homogeneous way dealing only with points and without the need of talking explicitly about lines, planes or any higher entity.
BibTeX:	@article{Projective_Geometry-AFP, author = {Anthony Bordg}, title = {Projective Geometry}, journal = {Archive of Formal Proofs}, month = jun, year = 2018, note = {\url{http://isa-afp.org/entries/Projective_Geometry.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.