Contribution: ProjectiveGeometry

Projective Geometry

Authors

Description

This contributions contains elements of formalization of projective geometry. In the plane: Two axiom systems are shown equivalent. We prove some results about the decidability of the the incidence and equality predicates. The classic notion of duality between points and lines is formalized thanks to a functor. The notion of 'flat' is defined and flats are characterized. Fano's plane, the smallest projective plane is defined. We show that Fano's plane is desarguesian. In the space: We prove Desargues' theorem.

Keywords

geometry, projective, fano, homogeneous coordinates model, flat, rank, desargues, moulton

Available files