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