Nuprl Definition : r2-perp
r2-perp(x) ==  λi.if (i =z 0) then (-(x 1)/||x||) else (x 0/||x||) fi 
Definitions occuring in Statement : 
real-vec-norm: ||x||
, 
rdiv: (x/y)
, 
rminus: -(x)
, 
ifthenelse: if b then t else f fi 
, 
eq_int: (i =z j)
, 
apply: f a
, 
lambda: λx.A[x]
, 
natural_number: $n
Definitions occuring in definition : 
natural_number: $n
, 
real-vec-norm: ||x||
, 
apply: f a
, 
rdiv: (x/y)
, 
rminus: -(x)
, 
eq_int: (i =z j)
, 
ifthenelse: if b then t else f fi 
, 
lambda: λx.A[x]
FDL editor aliases : 
r2-perp
Latex:
r2-perp(x)  ==    \mlambda{}i.if  (i  =\msubz{}  0)  then  (-(x  1)/||x||)  else  (x  0/||x||)  fi 
Date html generated:
2016_10_28-AM-07_42_06
Last ObjectModification:
2016_09_28-PM-01_49_28
Theory : reals!model!euclidean!geometry
Home
Index