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: P
⇒ Q
,
apply: f a
,
lambda: λx.A[x]
,
rationals: ℚ
Definitions :
lambda: λx.A[x]
,
rationals: ℚ
,
exists: ∃x:A. B[x]
,
all: ∀x:A. B[x]
,
nat: ℕ
,
implies: P
⇒ Q
,
le: A ≤ B
,
qle: Error :qle,
apply: f 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