Nuprl Definition : totally-bounded
totally-bounded(A) ==
∀e:ℝ. ((r0 < e) ⇒ (∃n:ℕ+. ∃a:ℕn ⟶ ℝ. ((∀i:ℕn. (a i ∈ A)) ∧ (∀x:ℝ. ((x ∈ A) ⇒ (∃i:ℕn. (|x - a i| < e)))))))
Definitions occuring in Statement :
rset-member: x ∈ A,
rless: x < y,
rabs: |x|,
rsub: x - y,
int-to-real: r(n),
real: ℝ,
int_seg: {i..j-},
nat_plus: ℕ+,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n
Definitions occuring in definition :
int-to-real: r(n),
nat_plus: ℕ+,
function: x:A ⟶ B[x],
and: P ∧ Q,
all: ∀x:A. B[x],
real: ℝ,
implies: P ⇒ Q,
rset-member: x ∈ A,
exists: ∃x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
rless: x < y,
rabs: |x|,
rsub: x - y,
apply: f a
FDL editor aliases :
totally-bounded
totally-bounded
Latex:
totally-bounded(A) ==
\mforall{}e:\mBbbR{}
((r0 < e)
{}\mRightarrow{} (\mexists{}n:\mBbbN{}\msupplus{}. \mexists{}a:\mBbbN{}n {}\mrightarrow{} \mBbbR{}. ((\mforall{}i:\mBbbN{}n. (a i \mmember{} A)) \mwedge{} (\mforall{}x:\mBbbR{}. ((x \mmember{} A) {}\mRightarrow{} (\mexists{}i:\mBbbN{}n. (|x - a i| < e)))))))
Date html generated:
2016_05_18-AM-08_14_36
Last ObjectModification:
2015_09_23-AM-09_04_54
Theory : reals
Home
Index