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