Nuprl Lemma : Editor aliases for Constructive Geometry


All theorems of constructive geometry have the form
⌈∀e:EuclideanPlane. [prop]⌉
(to enter that type "all" and then "eu-pl" in the [type] slot).
  
To edit formulas about geometry use the following editor aliases:

eu-pt  ⌈eu-point([term])⌉ --then fill in e  (your EuclideanPlane) and it will
                             display as ⌈Point⌉
eu-cong  ⌈ab=cd⌉    --- first slot is e (your EuclideanPlane) then a, b, c, d.

eu-bt  ⌈a-b-c⌉  -- this is strict betweeness,  first slot is e.
eu-be  ⌈a_b_c⌉  -- non-strict betweeness ( ⌈a = b ∈ Point⌉ and ⌈b = c ∈ Point⌉ are allowed).

⋅

Latex:

All  theorems  of  constructive  geometry  have  the  form
\mkleeneopen{}\mforall{}e:EuclideanPlane.  [prop]\mkleeneclose{}
(to  enter  that  type  "all"  and  then  "eu-pl"  in  the  [type]  slot).
   
To  edit  formulas  about  geometry  use  the  following  editor  aliases:

eu-pt    \mkleeneopen{}eu-point([term])\mkleeneclose{}  --then  fill  in  e    (your  EuclideanPlane)  and  it  will
                                                          display  as  \mkleeneopen{}Point\mkleeneclose{}
eu-cong    \mkleeneopen{}ab=cd\mkleeneclose{}        ---  first  slot  is  e  (your  EuclideanPlane)  then  a,  b,  c,  d.

eu-bt    \mkleeneopen{}a-b-c\mkleeneclose{}    --  this  is  strict  betweeness,    first  slot  is  e.
eu-be    \mkleeneopen{}a\_b\_c\mkleeneclose{}    --  non-strict  betweeness  (  \mkleeneopen{}a  =  b\mkleeneclose{}  and  \mkleeneopen{}b  =  c\mkleeneclose{}  are  allowed).

\mcdot{}


Date html generated: 2015_07_17-PM-06_21_45
Last ObjectModification: 2015_07_17-AM-00_01_36

Home Index