GeoCoq Figures

Table of Contents

• Chapter 0 : Axioms

  • Five segments
  • Five segments
  • Segment construction
  • Segment construction
  • Inner Pasch
  • Inner Pasch
  • Upper dimension
  • Upper dimension

• Definitions

  • Definition of coplanar.
  • Is image spec
  • One side
  • One side
  • Definition of Per
  • Definition of Per
  • Perpendicular Bisector
  • Definition of Perpendicular Bisector
  • Two sides
  • Two sides
  • Perpendicular at
  • Perpendicular at

• Chapter 6

  • Lemma 6.21
  • Lemma 6.21

• Chapter 7

  • Lemma 7.13

• Chapter 8

  • Lemma 8.18
  • Lemma 8.18

• Chapter 9

  • Lemma 9.8.2
  • Lemma 9.8.2
  • Lemma 9.13
  • Lemma 9.13
  • Lemma 9.17
  • Lemma 9.19
  • Lemma 9.19
  • Lemma 9.31

• Chapter 10

  • Lemma 10.15
  • Lemma 10.15

• Chapter 12

  • Lemma 12.6
  • Lemma 12.6
  • Lemma 12.9
  • Lemma 12.9
  • Lemma 12.10
  • Lemma 12.10
  • Lemma 12.17
  • Lemma 12.17

• 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

  • Pseudo transitivity of coplanar
  • Outer Pasch
  • Outer Pasch
  • Pasch Hilbert
  • Pasch Hilbert
  • Perp bisector and collinearity
  • Perp perp col
  • Perp perp col
  • Cong perp bisect col

• Equivalence between postulates

  • Circumcenter implies Tarski's postulate
  • Euclid 5th implies SPP

• Triangle centers

  • Circumcenter
  • Euler Line
  • Orthocenter
  • Gravity center

• Highschool examples

  • Varignon's theorem