Nuprl Definition : m-TB

This is a useful formulation of "metric total boundedness".
The lemma Error :m-TB-iff proves that it is equivalent to
∀k:ℕ. ∃n:ℕ⁺. ∃xs:ℕn ⟶ X. ∀x:X. ∃i:ℕn. (mdist(d;x;xs i) ≤ (r1/r(k + 1)))

This says that for every epsilon (1/(k+1)) there is a finite collection, xs,
of points in X (some might call it a "subfinite" collection) such that
every point in X is within distance epsilon from some point in xs.

The constructive content of this is
1) the function B from k in ℕ to n in ℕ⁺
2) for given k, the xs:ℕB k ⟶ X
3) the "decider" or "chooser" c that for a given x in X finds
the index in ℕB k of the point in the xs for which the distance to x is
less than epsilon.⋅

m-TB(X;d) ==
  {tb:B:ℕ ⟶ ℕ⁺ × k:ℕ ⟶ ℕB k ⟶ X × (X ⟶ k:ℕ ⟶ ℕB k)|
   let B,xs,c = tb in
   ∀p:X. ∀k:ℕ.  (mdist(d;p;xs k (c p k)) ≤ (r1/r(k + 1)))}

Definitions occuring in Statement : mdist: mdist(d;x;y), rdiv: (x/y), rleq: x ≤ y, int-to-real: r(n), int_seg: {i..j^-}, nat_plus: ℕ⁺, nat: ℕ, spreadn: spread3, all: ∀x:A. B[x], set: {x:A| B[x]} , apply: f a, function: x:A ⟶ B[x], product: x:A × B[x], add: n + m, natural_number: $n
Definitions occuring in definition : set: {x:A| B[x]} , nat_plus: ℕ⁺, product: x:A × B[x], function: x:A ⟶ B[x], int_seg: {i..j^-}, spreadn: spread3, all: ∀x:A. B[x], nat: ℕ, rleq: x ≤ y, mdist: mdist(d;x;y), apply: f a, rdiv: (x/y), int-to-real: r(n), add: n + m, natural_number: $n
FDL editor aliases : m-TB

Latex:
m-TB(X;d) == \{tb:B:\mBbbN{} {}\mrightarrow{} \mBbbN{}\msupplus{} \mtimes{} k:\mBbbN{} {}\mrightarrow{} \mBbbN{}B k {}\mrightarrow{} X \mtimes{} (X {}\mrightarrow{} k:\mBbbN{} {}\mrightarrow{} \mBbbN{}B k)| let B,xs,c = tb in \mforall{}p:X. \mforall{}k:\mBbbN{}. (mdist(d;p;xs k (c p k)) \mleq{} (r1/r(k + 1)))\} Date html generated: 2019_10_30-AM-06_50_11 Last ObjectModification: 2019_10_11-PM-00_13_20 Theory : reals Home Index