package coq-projective-geometry
- Overview
- No Docs
You can search for identifiers within the package.
in-package search v0.2.0
Projective Geometry
Install
Dune Dependency
Authors
Maintainers
Sources
v8.10.0.tar.gz
md5=d6807a8a37bfd7aee33f251ef1709f54
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.
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page