Nuprl Definition : ni-selector
ni-selector(p) == λn.(¬b(∃i<n + 1.¬b(p i∞))_b)
Definitions occuring in Statement :
nat2inf: n∞,
b-exists: (∃i<n.P[i])_b,
bnot: ¬bb,
apply: f a,
lambda: λx.A[x],
add: n + m,
natural_number: $n
Definitions occuring in definition :
lambda: λx.A[x],
b-exists: (∃i<n.P[i])_b,
add: n + m,
natural_number: $n,
bnot: ¬bb,
apply: f a,
nat2inf: n∞
FDL editor aliases :
ni-selector
Latex:
ni-selector(p) == \mlambda{}n.(\mneg{}\msubb{}(\mexists{}i<n + 1.\mneg{}\msubb{}(p i\minfty{}))\_b)
Date html generated:
2016_05_15-PM-01_47_12
Last ObjectModification:
2015_09_23-AM-07_37_10
Theory : basic
Home
Index