Nuprl Definition : infn
infn(n;I) == primrec(n;λf.(f ⋅);λi,r,f. inf{r (λa.(f a++z)) | z ∈ I})
Definitions occuring in Statement :
real-vec-extend: a++z,
range_inf: inf{f[x] | x ∈ I},
primrec: primrec(n;b;c),
it: ⋅,
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
primrec: primrec(n;b;c),
it: ⋅,
range_inf: inf{f[x] | x ∈ I},
lambda: λx.A[x],
apply: f a,
real-vec-extend: a++z
FDL editor aliases :
infn
Latex:
infn(n;I) == primrec(n;\mlambda{}f.(f \mcdot{});\mlambda{}i,r,f. inf\{r (\mlambda{}a.(f a++z)) | z \mmember{} I\})
Date html generated:
2019_10_30-AM-08_23_44
Last ObjectModification:
2019_05_28-PM-03_11_45
Theory : reals
Home
Index