概述
GeoCoq Figures
Figure used in our formalization of foundations of geometry in Coq.
内容目录
Chapter 0 : Axioms
Definitions
Chapter 6
Chapter 7
Chapter 8
Chapter 9
Chapter 10
Chapter 12
Parallel postulates
- Euclid 5th Postulate
- Euclid 5th postulate
- Par Perp2 Par
- Par Perp2 Par
- Perpendicular transversal
- Perpendicular transversal
- Proclus postulate
- Proclus postulate
- Strong parallel postulate
- Legendre postulate
- Legendre postulate
- Transitivity of parallelism
- Transitivity of parallelism
- Triangle circumscription principle
- Triangle circumscription principle
- Playfair's postulate
- Playfair's postulate
- Midpoint postulate
- Midpoint postulate
Misc
Equivalence between postulates
Triangle centers
Highschool examples