---

Step * 1 of Lemma m-TB-iff


1. [X] : Type
2. [d] : metric(X)
3. m-TB(X;d)
4. k : ℕ
⊢ ∃n:ℕ+. ∃xs:ℕn ⟶ X. ∀x:X. ∃i:ℕn. (mdist(d;x;xs i) ≤ (r1/r(k + 1)))
BY
{ (D -2 THEN RepeatFor 2 (D -3) THEN All Reduce) }

1
1. [X] : Type
2. [d] : metric(X)
3. B : ℕ ⟶ ℕ+
4. t2 : k:ℕ ⟶ ℕB k ⟶ X
5. t3 : X ⟶ k:ℕ ⟶ ℕB k
6. [%2] : ∀p:X. ∀k:ℕ.  (mdist(d;p;t2 k (t3 p k)) ≤ (r1/r(k + 1)))
7. k : ℕ
⊢ ∃n:ℕ+. ∃xs:ℕn ⟶ X. ∀x:X. ∃i:ℕn. (mdist(d;x;xs i) ≤ (r1/r(k + 1)))

---

Latex:

---

Latex:

1.  [X]  :  Type
2.  [d]  :  metric(X)
3.  m-TB(X;d)
4.  k  :  \mBbbN{}
\mvdash{}  \mexists{}n:\mBbbN{}\msupplus{}.  \mexists{}xs:\mBbbN{}n  {}\mrightarrow{}  X.  \mforall{}x:X.  \mexists{}i:\mBbbN{}n.  (mdist(d;x;xs  i)  \mleq{}  (r1/r(k  +  1)))


By

---

Latex:
(D  -2  THEN  RepeatFor  2  (D  -3)  THEN  All  Reduce)

---

Home Index