Nuprl Definition : rlessw
rlessw(x;y) == quick-find(λn.(x n) + 4 <z y n;1)
Definitions occuring in Statement :
lt_int: i <z j,
apply: f a,
lambda: λx.A[x],
add: n + m,
natural_number: $n,
quick-find: quick-find(p;n)
Definitions occuring in definition :
quick-find: quick-find(p;n),
lambda: λx.A[x],
lt_int: i <z j,
add: n + m,
apply: f a,
natural_number: $n
FDL editor aliases :
rlessw
Latex:
rlessw(x;y) == quick-find(\mlambda{}n.(x n) + 4 <z y n;1)
Date html generated:
2016_05_18-AM-07_04_14
Last ObjectModification:
2015_09_23-AM-09_01_16
Theory : reals
Home
Index