GeoCoq Figures

Julien Narboux, 2015. 10. 28.

Figure used in our formalization of foundations of geometry in Coq.

차례

  1. Chapter 0 : Axioms
    1. Five segments
    2. Five segments
    3. Segment construction
    4. Segment construction
    5. Inner Pasch
    6. Inner Pasch
    7. Upper dimension
    8. Upper dimension
  2. Definitions
    1. Definition of coplanar.
    2. Is image spec
    3. One side
    4. One side
    5. Definition of Per
    6. Definition of Per
    7. Perpendicular Bisector
    8. Definition of Perpendicular Bisector
    9. Two sides
    10. Two sides
    11. Perpendicular at
    12. Perpendicular at
  3. Chapter 6
    1. Lemma 6.21
    2. Lemma 6.21
  4. Chapter 7
    1. Lemma 7.13
  5. Chapter 8
    1. Lemma 8.18
    2. Lemma 8.18
  6. Chapter 9
    1. Lemma 9.8.2
    2. Lemma 9.8.2
    3. Lemma 9.13
    4. Lemma 9.13
    5. Lemma 9.17
    6. Lemma 9.19
    7. Lemma 9.19
    8. Lemma 9.31
  7. Chapter 10
    1. Lemma 10.15
    2. Lemma 10.15
  8. Chapter 11
  9. Chapter 12
    1. Lemma 12.6
    2. Lemma 12.6
    3. Lemma 12.9
    4. Lemma 12.9
    5. Lemma 12.10
    6. Lemma 12.10
    7. Lemma 12.17
    8. Lemma 12.17
  10. Parallel postulates
    1. Euclid 5th Postulate
    2. Euclid 5th postulate
    3. Par Perp2 Par
    4. Par Perp2 Par
    5. Perpendicular transversal
    6. Perpendicular transversal
    7. Proclus postulate
    8. Proclus postulate
    9. Strong parallel postulate
    10. Legendre postulate
    11. Legendre postulate
    12. Transitivity of parallelism
    13. Transitivity of parallelism
    14. Triangle circumscription principle
    15. Triangle circumscription principle
    16. Playfair's postulate
    17. Playfair's postulate
    18. Midpoint postulate
    19. Midpoint postulate
  11. Misc
    1. Pseudo transitivity of coplanar
    2. Outer Pasch
    3. Outer Pasch
    4. Pasch Hilbert
    5. Pasch Hilbert
    6. Perp bisector and collinearity
    7. Perp perp col
    8. Perp perp col
    9. Cong perp bisect col
  12. Equivalence between postulates
    1. Circumcenter implies Tarski's postulate
    2. Euclid 5th implies SPP
  13. Triangle centers
    1. Circumcenter
    2. Euler Line
    3. Orthocenter
    4. Gravity center
  14. Highschool examples
    1. Varignon's theorem
  15. Euclid's Elements - Book 1

1.

Chapter 0 : Axioms

  • 1. Five segments
  • 2. Five segments
  • 3. Segment construction
  • 4. Segment construction
  • 5. Inner Pasch
  • 6. Inner Pasch
  • 7. Upper dimension
  • 8. Upper dimension

1.1.

–

1.2.

–

1.3.

–

1.4.

–

1.5.

–

1.6.

–

1.7.

–

1.8.

–

2.

Definitions

  • 1. Definition of coplanar.
  • 2. Is image spec
  • 3. One side
  • 4. One side
  • 5. Definition of Per
  • 6. Definition of Per
  • 7. Perpendicular Bisector
  • 8. Definition of Perpendicular Bisector
  • 9. Two sides
  • 10. Two sides
  • 11. Perpendicular at
  • 12. Perpendicular at

2.1.

–

2.2.

–

2.3.

–

2.4.

–

2.5.

–

2.6.

–

2.7.

–

2.8.

–

2.9.

–

2.10.

–

2.11.

–

2.12.

–

3.

Chapter 6

  • 1. Lemma 6.21
  • 2. Lemma 6.21

3.1.

–

3.2.

–

4.

Chapter 7

  • 1. Lemma 7.13

4.1.

–

5.

Chapter 8

  • 1. Lemma 8.18
  • 2. Lemma 8.18

5.1.

–

5.2.

–

6.

Chapter 9

  • 1. Lemma 9.8.2
  • 2. Lemma 9.8.2
  • 3. Lemma 9.13
  • 4. Lemma 9.13
  • 5. Lemma 9.17
  • 6. Lemma 9.19
  • 7. Lemma 9.19
  • 8. Lemma 9.31

6.1.

–

6.2.

–

6.3.

–

6.4.

–

6.5.

–

6.6.

–

6.7.

–

6.8.

–

7.

Chapter 10

  • 1. Lemma 10.15
  • 2. Lemma 10.15

7.1.

–

7.2.

–

8.

Chapter 11


    이 장은 자료를 포함하고 있지 않습니다.

9.

Chapter 12

  • 1. Lemma 12.6
  • 2. Lemma 12.6
  • 3. Lemma 12.9
  • 4. Lemma 12.9
  • 5. Lemma 12.10
  • 6. Lemma 12.10
  • 7. Lemma 12.17
  • 8. Lemma 12.17

9.1.

–

9.2.

–

9.3.

–

9.4.

–

9.5.

–

9.6.

–

9.7.

–

9.8.

–

10.

Parallel postulates

  • 1. Euclid 5th Postulate
  • 2. Euclid 5th postulate
  • 3. Par Perp2 Par
  • 4. Par Perp2 Par
  • 5. Perpendicular transversal
  • 6. Perpendicular transversal
  • 7. Proclus postulate
  • 8. Proclus postulate
  • 9. Strong parallel postulate
  • 10. Legendre postulate
  • 11. Legendre postulate
  • 12. Transitivity of parallelism
  • 13. Transitivity of parallelism
  • 14. Triangle circumscription principle
  • 15. Triangle circumscription principle
  • 16. Playfair's postulate
  • 17. Playfair's postulate
  • 18. Midpoint postulate
  • 19. Midpoint postulate

10.1.

–

10.2.

–

10.3.

–

10.4.

–

10.5.

–

10.6.

–

10.7.

–

10.8.

–

10.9.

–

10.10.

–

10.11.

–

10.12.

–

10.13.

–

10.14.

–

10.15.

–

10.16.

–

10.17.

–

10.18.

–

10.19.

–

11.

Misc

  • 1. Pseudo transitivity of coplanar
  • 2. Outer Pasch
  • 3. Outer Pasch
  • 4. Pasch Hilbert
  • 5. Pasch Hilbert
  • 6. Perp bisector and collinearity
  • 7. Perp perp col
  • 8. Perp perp col
  • 9. Cong perp bisect col

11.1.

–

11.2.

–

11.3.

–

11.4.

–

11.5.

–

11.6.

–

11.7.

–

11.8.

–

11.9.

–

12.

Equivalence between postulates

Figures used in the proof of equivalence between different versions of the parallel postulate.

  • 1. Circumcenter implies Tarski's postulate
  • 2. Euclid 5th implies SPP

12.1.

–

12.2.

–

13.

Triangle centers

  • 1. Circumcenter
  • 2. Euler Line
  • 3. Orthocenter
  • 4. Gravity center

13.1.

–

13.2.

–

13.3.

–

13.4.

–

14.

Highschool examples

  • 1. Varignon's theorem

14.1.

–

15.

Euclid's Elements - Book 1


    이 장은 자료를 포함하고 있지 않습니다.

정보