Nuprl Definition : nat2inf
n∞ == λi.i <z n
Definitions occuring in Statement :
lt_int: i <z j,
lambda: λx.A[x]
Definitions occuring in definition :
lambda: λx.A[x],
lt_int: i <z j
FDL editor aliases :
nat2inf
Latex:
n\minfty{} == \mlambda{}i.i <z n
Date html generated:
2016_05_15-PM-01_46_47
Last ObjectModification:
2015_09_23-AM-07_37_08
Theory : basic
Home
Index