Email Gateway (Aug 22 2022 at 17:36): Email Gateway (Aug 22 2022 at 17:36):From: Tobias Nipkow <nipkow@in.tum.de>
Projective Geometry
Anthony Bordg
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.
https://www.isa-afp.org/entries/Projective_Geometry.html
Enjoy!
smime.p7s
Last updated: Apr 26 2024 at 01:06 UTC