Теорема о квадрате
This commit is contained in:
18
Сивочуб Алексей/README.md
Normal file
18
Сивочуб Алексей/README.md
Normal file
@@ -0,0 +1,18 @@
|
||||
# Теорема о квадрате
|
||||
## Ссылка на видеоразбор
|
||||
https://youtu.be/0Yp5sgddlko
|
||||
## Код из сайта
|
||||
START_INTERACTIVE;;
|
||||
let coordinations =
|
||||
["perpendicular", (** Lines (1,2) and (3,4) are perpendicular **)
|
||||
<<(1_x - 2_x) * (3_x - 4_x) + (1_y - 2_y) * (3_y - 4_y) = 0>>;
|
||||
"lengths_eq", (** Lines (1,2) and (3,4) have the same length **)
|
||||
<<(1_x - 2_x)^2 + (1_y - 2_y)^2 = (3_x - 4_x)^2 + (3_y - 4_y)^2>>;
|
||||
"is_midpoint", (** Point 1 is the midpoint of line (2,3) **)
|
||||
<<2 * 1_x = 2_x + 3_x /\ 2 * 1_y = 2_y + 3_y>>];;
|
||||
#Square theorem
|
||||
|
||||
(grobner_decide ** originate)
|
||||
<<is_midpoint(m,a,c) /\ perpendicular(a,c,m,b)
|
||||
==> lengths_eq(a,b,b,c)>>;;
|
||||
END_INTERACTIVE;
|
||||
Reference in New Issue
Block a user