Line | |
---|
1 | ;; Prove Desargues Theorem.
|
---|
2 | ;;
|
---|
3 | ;; Desargues Theorem (Wikipedia): In a projective space, two triangles
|
---|
4 | ;; are in perspective axially if and only if they are in perspective
|
---|
5 | ;; centrally.
|
---|
6 |
|
---|
7 | (translate-theorem
|
---|
8 | (
|
---|
9 | ;; If
|
---|
10 |
|
---|
11 | ;; Triangles are in perspective centrally
|
---|
12 | ;; O is the center of projectivity
|
---|
13 | (collinear A0 A1 O)
|
---|
14 | (collinear B0 B1 O)
|
---|
15 | (collinear C0 C1 O)
|
---|
16 |
|
---|
17 | ;; and X, Y, Z are points on the axis of projectivity
|
---|
18 | (collinear A0 C0 Y)
|
---|
19 | (collinear B0 C0 X)
|
---|
20 | (collinear A0 B0 Z)
|
---|
21 |
|
---|
22 | (collinear A1 C1 Y)
|
---|
23 | (collinear B1 C1 X)
|
---|
24 | (collinear A1 B1 Z)
|
---|
25 | )
|
---|
26 | ;; Then
|
---|
27 | ((collinear X Y Z)
|
---|
28 |
|
---|
29 | ;; What if X Y X are at infinity?
|
---|
30 | ;; Or one of the triangles is degenerate?
|
---|
31 |
|
---|
32 | ;;(identical-points A0 C0)
|
---|
33 | ;;(identical-points A0 B0)
|
---|
34 | ;;(identical-points B0 C0)
|
---|
35 |
|
---|
36 | ;;(identical-points A1 C1)
|
---|
37 | ;;(identical-points A1 B1)
|
---|
38 | ;;(identical-points B1 C1)
|
---|
39 |
|
---|
40 | )
|
---|
41 | ;; :order #'grlex>
|
---|
42 | )
|
---|
43 |
|
---|
Note:
See
TracBrowser
for help on using the repository browser.