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
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:
2020_05_20-PM-00_04_01
Last ObjectModification:
2019_12_13-PM-02_41_02
Theory : reals
Home
Index