Nuprl Definition : fun-converges
λn.f[n; x]↓ for x ∈ I) == ∃g:I ⟶ℝ. lim n→∞.f[n; x] = λy.g y for x ∈ I
Definitions occuring in Statement :
fun-converges-to: lim n→∞.f[n; x] = λy.g[y] for x ∈ I,
rfun: I ⟶ℝ,
exists: ∃x:A. B[x],
apply: f a
Definitions occuring in definition :
exists: ∃x:A. B[x],
rfun: I ⟶ℝ,
fun-converges-to: lim n→∞.f[n; x] = λy.g[y] for x ∈ I,
apply: f a
FDL editor aliases :
fun-converges
Latex:
\mlambda{}n.f[n; x]\mdownarrow{} for x \mmember{} I) == \mexists{}g:I {}\mrightarrow{}\mBbbR{}. lim n\mrightarrow{}\minfty{}.f[n; x] = \mlambda{}y.g y for x \mmember{} I
Date html generated:
2016_05_18-AM-09_53_18
Last ObjectModification:
2015_09_23-AM-09_14_08
Theory : reals
Home
Index