Nuprl Definition : rless_ibs

rless_ibs(x;y) ==  λn.if (∃m∈upto(n + 1).(x (m + 1)) + 4 <z y (m + 1))_b then 1 else 0 fi 


Definitions occuring in Statement :  bl-exists: (∃x∈L.P[x])_b,  upto: upto(n),  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  apply: f a,  lambda: λx.A[x],  add: n + m,  natural_number: $n
Definitions occuring in definition :  lambda: λx.A[x],  ifthenelse: if b then t else f fi ,  bl-exists: (∃x∈L.P[x])_b,  upto: upto(n),  lt_int: i <z j,  apply: f a,  add: n + m,  natural_number: $n
FDL editor aliases :  rless_ibs
Latex:
rless\_ibs(x;y)  ==    \mlambda{}n.if  (\mexists{}m\mmember{}upto(n  +  1).(x  (m  +  1))  +  4  <z  y  (m  +  1))\_b  then  1  else  0  fi 


Date html generated: 2019_10_30-AM-10_15_50
Last ObjectModification: 2019_06_28-PM-01_55_41

Theory : real!vectors


Home Index