OpenMath Content Dictionary: plangeo4

Canonical URL:

http://www.openmath.org/cd/plangeo4.ocd

CD File:

plangeo4.ocd

CD as XML Encoded OpenMath:

plangeo4.omcd

Defines:

affine_coordinates, set_affine_coordinates, coordinates, is_affine, 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):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMBIND>
<OMS cd="quant1" name="forall"/>
  <OMBVAR>
    <OMV name="v"/>
  </OMBVAR>
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMBIND>
      <OMS cd="quant1" name="exists"/>
      <OMBVAR>
        <OMV name="A"/>
      </OMBVAR>
      <OMA>
        <OMS cd="plangeo4" name="set_coordinates"/>
        <OMV name="A"/>
        <OMV name="v"/>
      </OMA>
    </OMBIND>   
    <OMA>
      <OMS cd="logic1" name="not"/>
      <OMA>
        <OMS cd="logic1" name="and"/>
        <OMA>
          <OMS cd="relation1" name="eq"/>
          <OMA>
            <OMS cd="linalg1" name="vector_selector"/>
            <OMI>1</OMI>
            <OMV name="v"/>
          </OMA>
          <OMS cd="alg1" name="zero"/>
        </OMA>
        <OMA>
          <OMS cd="relation1" name="eq"/>
          <OMA>
            <OMS cd="linalg1" name="vector_selector"/>
            <OMI>2</OMI>
            <OMV name="v"/>
          </OMA>
          <OMS cd="alg1" name="zero"/>
        </OMA>
        <OMA>
          <OMS cd="relation1" name="eq"/>
          <OMA>
            <OMS cd="linalg1" name="vector_selector"/>
            <OMI>3</OMI>
            <OMV name="v"/>
          </OMA>
          <OMS cd="alg1" name="zero"/>
        </OMA>
      </OMA>
    </OMA>
  </OMA>
</OMBIND>
</OMOBJ>

forall [ v ] . (implies (exists [ A ] . (set_coordinates ( A, v) ) , not (and (eq (vector_selector (1, v) , zero) , eq (vector_selector (2, v) , zero) , eq (vector_selector (3, v) , zero) ) ) ) )

$$\forall \hspace{0.17em}v.\exists \hspace{0.17em}A.\mathrm{set\_coordinates}(A,v)\Rightarrow \neg (v_1=0\wedge v_2=0\wedge v_3=0)$$

Signatures:

sts

coordinates

Description:

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

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0"> 
<OMA>
  <OMS cd="logic1" name="implies"/>
  <OMA> 
    <OMS cd="logic1" name="and"/>
    <OMA>
     <OMS cd="relation1" name="eq"/>
     <OMV name="v"/>
     <OMA>
       <OMS cd="plangeo4" name="coordinates"/>
       <OMA>
         <OMS cd="plangeo1" name="point"/>
         <OMV name="A"/>
       </OMA>
     </OMA>
    <OMA>
     <OMS cd="relation1" name="eq"/>
     <OMV name="w"/>
     <OMA>
       <OMS cd="plangeo4" name="coordinates"/>
       <OMA>
         <OMS cd="plangeo1" name="line"/>
         <OMV name="L"/>
       </OMA>
     </OMA>
    </OMA>
  </OMA> 
  <OMA>
   <OMS cd="relation1" name="eq"/>
   <OMA>
     <OMS cd="arith1" name="plus"/>
     <OMA>
       <OMS cd="arith1" name="times"/>
       <OMA>
         <OMS cd="linalg1" name="vector_selector"/>
         <OMI>1</OMI>
         <OMV name="v"/>
       </OMA>
       <OMA>
         <OMS cd="linalg1" name="vector_selector"/>
         <OMI>1</OMI>
         <OMV name="w"/>
       </OMA>
     </OMA>
     <OMA>
       <OMS cd="arith1" name="times"/>
       <OMA>
         <OMS cd="linalg1" name="vector_selector"/>
         <OMI>2</OMI>
         <OMV name="v"/>
       </OMA>
       <OMA>
         <OMS cd="linalg1" name="vector_selector"/>
         <OMI>2</OMI>
         <OMV name="w"/>
       </OMA>
     </OMA>
     <OMA>
       <OMS cd="arith1" name="times"/>
       <OMA>
         <OMS cd="linalg1" name="vector_selector"/>
         <OMI>3</OMI>
         <OMV name="v"/>
       </OMA>
       <OMA>
         <OMS cd="linalg1" name="vector_selector"/>
         <OMI>3</OMI>
         <OMV name="w"/>
       </OMA>
     </OMA>
    </OMA>
    <OMS cd="alg1" name="zero"/>
  </OMA>
</OMA>
</OMA>
</OMOBJ>

implies (and (eq ( v, coordinates (point ( A) ) , eq ( w, coordinates (line ( L) ) ) ) , eq (plus (times (vector_selector (1, v) , vector_selector (1, w) ) , times (vector_selector (2, v) , vector_selector (2, w) ) , times (vector_selector (3, v) , vector_selector (3, w) ) ) , zero) ) )

$$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\Rightarrow$$

Example:

To extract the coordinates of a point A with coordinates (1,2,3):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0"> 
<OMA>
   <OMS cd="plangeo4" name="coordinates"/> 
   <OMA>
     <OMS cd="plangeo1" name="point"/>
     <OMV name="A"/>
     <OMA>
       <OMS cd="plangeo4" name="set_coordinates"/>
       <OMV name="A"/>
       <OMA>
         <OMS cd="linalg2" name="vector"/>
         <OMI>1</OMI>
         <OMI>2</OMI>
         <OMI>3</OMI>
       </OMA>
     </OMA>
   </OMA>
</OMA>
</OMOBJ>

coordinates (point ( A, set_coordinates ( A, vector (1, 2, 3) ) ) )

$$\mathrm{coordinates}\left(\mathrm{point}(A,\mathrm{set\_coordinates}(A,(1,2,3)))\right)$$

Signatures:

sts

is_affine

Description:

Boolean function testing whether a point or line is affine.

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMBIND><OMS cd="quant1" name="forall"/>
     <OMBVAR><OMV name="v"/></OMBVAR>
     <OMA><OMS cd="logic1" name="implies"/>
          <OMBIND><OMS cd="quant1" name="exists"/>
               <OMBVAR><OMV name="A"/></OMBVAR>
               <OMA><OMS cd="plangeo1" name="point"/>
                    <OMV name="A"/>
                    <OMA><OMS cd="plangeo4" name="set_coordinates"/>
                         <OMV name="A"/><OMV name="v"/>
                    </OMA>
                    <OMA><OMS cd="plangeo4" name="is_affine"/>
                         <OMV name="A"/>
                    </OMA>
               </OMA>
          </OMBIND>   
          <OMA><OMS cd="logic1" name="not"/>
               <OMA><OMS cd="relation1" name="eq"/>
                    <OMA><OMS cd="linalg1" name="vector_selector"/>
                         <OMI>3</OMI>  <OMV name="v"/>
                    </OMA>
                    <OMS cd="alg1" name="zero"/>
               </OMA>
          </OMA>
     </OMA>
</OMBIND>
</OMOBJ>

forall [ v] . (implies (exists [ A] . (point ( A, set_coordinates ( A, v) , is_affine ( A) ) ) , not (eq (vector_selector (3, v) , zero) ) ) )

$$\forall \hspace{0.17em}v.\exists \hspace{0.17em}A.\mathrm{point}(A,\mathrm{set\_coordinates}(A,v),\mathrm{is\_affine}\left(A\right))\Rightarrow \neg (v_3=0)$$

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMBIND>
<OMS cd="quant1" name="forall"/>
  <OMBVAR>
    <OMV name="v"/>
  </OMBVAR>
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMBIND>
      <OMS cd="quant1" name="exists"/>
      <OMBVAR><OMV name="A"/></OMBVAR>
        <OMA>
          <OMS cd="plangeo1" name="line"/>
          <OMV name="A"/>
          <OMA>
            <OMS cd="plangeo4" name="set_coordinates"/>
            <OMV name="A"/>
            <OMV name="v"/>
          </OMA>
          <OMA>
            <OMS cd="plangeo4" name="is_affine"/>
            <OMV name="A"/>
          </OMA>
        </OMA>
    </OMBIND>   
    <OMA>
      <OMS cd="logic1" name="not"/>
      <OMA>
        <OMS cd="logic1" name="and"/>
        <OMA>
          <OMS cd="relation1" name="eq"/>
          <OMA>
            <OMS cd="linalg1" name="vector_selector"/>
            <OMI>1</OMI>
            <OMV name="v"/>
          </OMA>
          <OMS cd="alg1" name="zero"/>
        </OMA>
        <OMA>
          <OMS cd="relation1" name="eq"/>
          <OMA>
            <OMS cd="linalg1" name="vector_selector"/>
            <OMI>2</OMI>
            <OMV name="v"/>
          </OMA>
          <OMS cd="alg1" name="zero"/>
        </OMA>
      </OMA>
    </OMA>
  </OMA>
</OMBIND>
</OMOBJ>

forall [ v ] . (implies (exists [ A] . (line ( A, set_coordinates ( A, v) , is_affine ( A) ) ) , not (and (eq (vector_selector (1, v) , zero) , eq (vector_selector (2, v) , zero) ) ) ) )

$$\forall \hspace{0.17em}v.\exists \hspace{0.17em}A.\mathrm{line}(A,\mathrm{set\_coordinates}(A,v),\mathrm{is\_affine}\left(A\right))\Rightarrow \neg (v_1=0\wedge v_2=0)$$

Example:

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMA>
  <OMS cd="plangeo4" name="is_affine"/>
   <OMV name="A"/>
</OMA>
</OMOBJ>

is_affine ( A)

$$\mathrm{is\_affine}\left(A\right)$$

Signatures:

sts

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).

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMA>
  <OMS cd="plangeo4" name="affine_coordinates"/>
   <OMA>
     <OMS cd="plangeo1" name="point"/>
     <OMV name="A"/>
     <OMA>
       <OMS cd="plangeo4" name="set_coordinates"/>
       <OMV name="A"/>
       <OMA>
         <OMS cd="linalg2" name="vector"/>
         <OMI>1</OMI>
         <OMI>2</OMI>
         <OMI>3</OMI>
       </OMA>
     </OMA>
   </OMA>
</OMA>
</OMOBJ>

affine_coordinates (point ( A, set_coordinates ( A, vector (1, 2, 3) ) ) )

$$\mathrm{affine\_coordinates}\left(\mathrm{point}(A,\mathrm{set\_coordinates}(A,(1,2,3)))\right)$$

Signatures:

sts

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.

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMA>
  <OMS cd="plangeo4" name="set_affine_coordinates"/>
  <OMV name="A"/>
     <OMA>
       <OMS cd="linalg2" name="vector"/>
       <OMA>
         <OMS cd="nums1" name="rational"/>
         <OMI> 1 </OMI>
         <OMI> 3 </OMI>
       </OMA>
       <OMA>
         <OMS cd="nums1" name="rational"/>
         <OMI> 2 </OMI>
         <OMI> 3 </OMI>
       </OMA>
     </OMA>
</OMA>
</OMOBJ>

set_affine_coordinates ( A, vector (rational ( 1 , 3 ) , rational ( 2 , 3 ) ) )

$$\mathrm{set\_affine\_coordinates}(A,(\frac{1}{3},\frac{2}{3}))$$

Signatures:

sts