Nuprl Definition : real-ball-slice
real-ball-slice(p;i;t) ==  λj.if j <z i then p j if i <z j then p (j - 1) else t fi 
Definitions occuring in Statement : 
ifthenelse: if b then t else f fi , 
lt_int: i <z j, 
apply: f a, 
lambda: λx.A[x], 
subtract: n - m, 
natural_number: $n
Definitions occuring in definition : 
lambda: λx.A[x], 
ifthenelse: if b then t else f fi , 
lt_int: i <z j, 
apply: f a, 
subtract: n - m, 
natural_number: $n
FDL editor aliases : 
real-ball-slice
Latex:
real-ball-slice(p;i;t)  ==    \mlambda{}j.if  j  <z  i  then  p  j  if  i  <z  j  then  p  (j  -  1)  else  t  fi 
Date html generated:
2019_10_30-AM-10_14_59
Last ObjectModification:
2019_06_28-PM-01_52_14
Theory : real!vectors
Home
Index