Nuprl Definition : rv-unbounded

(X[n]─→∞ as n─→∞==  λs.∀B:ℚ. ∃n:ℕ. ∀m:ℕ((n ≤ m)  (B ≤ (X[m] s)))



Definitions occuring in Statement :  nat: le: A ≤ B all: x:A. B[x] exists: x:A. B[x] implies:  Q apply: a lambda: λx.A[x] rationals:
Definitions :  lambda: λx.A[x] rationals: exists: x:A. B[x] all: x:A. B[x] nat: implies:  Q le: A ≤ B qle: Error :qle,  apply: a
FDL editor aliases :  rv-unbounded
(X[n]{}\mrightarrow{}\minfty{}  as  n{}\mrightarrow{}\minfty{})  ==    \mlambda{}s.\mforall{}B:\mBbbQ{}.  \mexists{}n:\mBbbN{}.  \mforall{}m:\mBbbN{}.  ((n  \mleq{}  m)  {}\mRightarrow{}  (B  \mleq{}  (X[m]  s)))



Date html generated: 2015_07_17-AM-08_01_23
Last ObjectModification: 2008_02_27-PM-05_49_52

Home Index