plangeo3
http://www.openmath.org/cd
http://www.openmath.org/cd/plangeo3.ocd
2006-06-01
experimental
2004-06-01
0
3
This CD defines symbols for planar Euclidean geometry related to distance.
distance
The distance between two affine points is the Euclidean distance.
The distance between two geometric objects O and O' is the infimum of the
distances between two affine points, one on O and one on O'.
The distance between two points A and B.
perpendicular
perpendicular is a binary boolean function with input two lines,
halflines or segments.
Its value is true whenever the two inputs are perpendicular to each other.
Testing perpendicularity of two lines L and M.
parallel
parallel is a binary boolean function with input two lines,
halflines or segments.
Its value is true whenever the two inputs are parallel.
Testing parallelism of two lines L and M.
circle
The symbol represents a circle.
The circle may be subject to constraints.
The circle C with center A and radius 1 is given by
1
radius
The radius of a circle.
The assertion that the radius of the circle C is 1:
1
radius_of
Gives the radius of a circle.
The radius of the circle C is given by
center
Defines the center of a circle.
The circle C with center A and radius 1 is given by
1
center_of
Gives the center of the circle
If C is the circle of the previous example then the following gives A.
are_on_circle
The statement that a set of points is on one circle.
This example states that A, B, C, and D lie on one circle.
angle
Angle of a corner, always measured in positive (anti-clockwise) direction.
Notice that
are not the same.
midpoint
The midpoint between two points or two endpoints of a segment.
The midpoint of two points A and B
is the same as the midpoint of the segment S on A and B.
equals
is_midpoint
The statement that one point is the midpoint of two others.
This example states that C is the midpoint of A and B.
center_of_gravity
Center of gravity of a number of points.
The center of gravity G of three points A, B and C is defined as follows.
perpbisector
Given two distinct points A and B, this is the line of all points at
equal
distance to both A and B.
altitude
Given a point p and a line L, this defines the segment starting at p
and ending in the unique point of L closest to p.
perpline
Given a point p and a line L, this defines the line through p
perpendicular to L.
polarline Given a point p
and a circle C this defines the polar line of p with respect to C.
If p is incident with the circle C, the polar line of p with
respect to C is the tangent line at p with respect to C.
tangent
Given a line L and a circle C this boolean checks whether
L is a tangent line to C.
arc
an arc of a circle M from A to B is the set of points of M that are
encountered when traversing the circle clockwise from A to B.