Nuprl Definition : bounded-sequence
bounded-sequence(n.x[n]) == ∃b:ℝ. ∀n:ℕ. (|x[n]| ≤ b)
Definitions occuring in Statement :
rleq: x ≤ y,
rabs: |x|,
real: ℝ,
nat: ℕ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x]
Definitions occuring in definition :
exists: ∃x:A. B[x],
real: ℝ,
all: ∀x:A. B[x],
nat: ℕ,
rleq: x ≤ y,
rabs: |x|
FDL editor aliases :
bounded-sequence
bounded-sequence
Latex:
bounded-sequence(n.x[n]) == \mexists{}b:\mBbbR{}. \mforall{}n:\mBbbN{}. (|x[n]| \mleq{} b)
Date html generated:
2016_05_18-AM-07_37_00
Last ObjectModification:
2015_09_23-AM-09_02_09
Theory : reals
Home
Index