Nuprl Definition : cube-face

cube-face(i;up;c) ==
  let l,u = c 
  in if up then <λj.if (j =z i) then u j else l j fi , u> else <l, λj.if (j =z i) then l j else u j fi > fi 


Definitions occuring in Statement :  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>
Definitions occuring in definition :  spread: spread def,  pair: <a, b>,  lambda: λx.A[x],  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  apply: f a
FDL editor aliases :  cube-face
Latex:
cube-face(i;up;c)  ==
    let  l,u  =  c 
    in  if  up
          then  <\mlambda{}j.if  (j  =\msubz{}  i)  then  u  j  else  l  j  fi  ,  u>
          else  <l,  \mlambda{}j.if  (j  =\msubz{}  i)  then  l  j  else  u  j  fi  >
          fi 


Date html generated: 2019_10_30-AM-11_31_58
Last ObjectModification: 2019_09_27-PM-01_45_00

Theory : real!vectors


Home Index