Nuprl Definition : p2J

p2J(a;b) ==
  λi.if (i =z 0) then ((a 1) * (b 2)) - (b 1) * (a 2)
     if (i =z 1) then ((a 2) * (b 0)) - (b 2) * (a 0)
     else ((a 1) * (b 0)) - (b 1) * (a 0)
     fi 


Definitions occuring in Statement :  rsub: x - y,  rmul: a * b,  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 :  lambda: λx.A[x],  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  rsub: x - y,  rmul: a * b,  apply: f a,  natural_number: $n
FDL editor aliases :  p2J
Latex:
p2J(a;b)  ==
    \mlambda{}i.if  (i  =\msubz{}  0)  then  ((a  1)  *  (b  2))  -  (b  1)  *  (a  2)
          if  (i  =\msubz{}  1)  then  ((a  2)  *  (b  0))  -  (b  2)  *  (a  0)
          else  ((a  1)  *  (b  0))  -  (b  1)  *  (a  0)
          fi 


Date html generated: 2017_10_05-AM-00_20_07
Last ObjectModification: 2017_06_17-AM-10_09_32

Theory : inner!product!spaces


Home Index