# OpenMath Content Dictionary: plangeo4

Canonical URL:
http://www.openmath.org/cd/plangeo4.ocd
CD Base:
http://www.openmath.org/cd
CD File:
plangeo4.ocd
CD as XML Encoded OpenMath:
plangeo4.omcd
Defines:
affine_coordinates, coordinates, is_affine, set_affine_coordinates, set_coordinates
Date:
2004-06-01
Version:
0 (Revision 5)
Review Date:
2006-06-01
Status:
experimental

This CD defines symbols for planar Euclidean geometry. In particular, it is concerned with projective and affine coordinates of points and lines.

## set_coordinates

Description:

This symbol defines the coordinates of a point or a line. The coordinates are the projective coordinates and consist of a vector of length 3. Points whose third coordinates are zero are the points at infinity. The line whose first two coordinates are zero is the line at infinity.

Formal Mathematical property (FMP):
$\forall v.\exists A.\mathrm{set_coordinates}\left(A,v\right)⇒¬\left({v}_{1}=0\wedge {v}_{2}=0\wedge {v}_{3}=0\right)$
Signatures:
sts

 [Next: coordinates] [Last: set_affine_coordinates] [Top]

## coordinates

Description:

This function yields the coordinates vector if applied to a point or line with coordinates.

Formal Mathematical property (FMP):
$v=\mathrm{coordinates}\left(\mathrm{point}\left(A\right)\right)=w=\mathrm{coordinates}\left(\mathrm{line}\left(L\right)\right)\wedge {v}_{1}{w}_{1}+{v}_{2}{w}_{2}+{v}_{3}{w}_{3}=0⇒$
Example:
To extract the coordinates of a point A with coordinates (1,2,3):
$\mathrm{coordinates}\left(\mathrm{point}\left(A,\mathrm{set_coordinates}\left(A,\left(1,2,3\right)\right)\right)\right)$
Signatures:
sts

 [Next: is_affine] [Previous: set_coordinates] [Top]

## is_affine

Description:

Boolean function testing whether a point or line is affine.

Formal Mathematical property (FMP):
$\forall v.\exists A.\mathrm{point}\left(A,\mathrm{set_coordinates}\left(A,v\right),\mathrm{is_affine}\left(A\right)\right)⇒¬\left({v}_{3}=0\right)$
Formal Mathematical property (FMP):
$\forall v.\exists A.\mathrm{line}\left(A,\mathrm{set_coordinates}\left(A,v\right),\mathrm{is_affine}\left(A\right)\right)⇒¬\left({v}_{1}=0\wedge {v}_{2}=0\right)$
Example:
$\mathrm{is_affine}\left(A\right)$
Signatures:
sts

 [Next: affine_coordinates] [Previous: coordinates] [Top]

## affine_coordinates

Description:

This function yields the affine coordinates vector if applied to a point or line with coordinates in the affine plane.

Example:
The affine coordinates (1/3,2/3) are expressed as follows for the point A with projective coordinates (1,2,3).
$\mathrm{affine_coordinates}\left(\mathrm{point}\left(A,\mathrm{set_coordinates}\left(A,\left(1,2,3\right)\right)\right)\right)$
Signatures:
sts

 [Next: set_affine_coordinates] [Previous: is_affine] [Top]

## set_affine_coordinates

Description:

Defines the affine coordinates of an affine point or line.

Example:
Assign the affine coordinates (1/3,2/3) to A.
$\mathrm{set_affine_coordinates}\left(A,\left(\frac{1}{3},\frac{2}{3}\right)\right)$
Signatures:
sts

 [First: set_coordinates] [Previous: affine_coordinates] [Top]