---

Step * 1 1 of Lemma m-TB-iff


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)))
BY
{ ((D 0 With ⌜B k⌝  THENA Auto) THEN (D 0 With ⌜t2 k⌝  THEN Auto) THEN D 0 With ⌜t3 x k⌝  THEN Auto) }

---

Latex:

---

Latex:

1.  [X]  :  Type
2.  [d]  :  metric(X)
3.  B  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}
4.  t2  :  k:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B  k  {}\mrightarrow{}  X
5.  t3  :  X  {}\mrightarrow{}  k:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B  k
6.  [\%2]  :  \mforall{}p:X.  \mforall{}k:\mBbbN{}.    (mdist(d;p;t2  k  (t3  p  k))  \mleq{}  (r1/r(k  +  1)))
7.  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  0  With  \mkleeneopen{}B  k\mkleeneclose{}    THENA  Auto)  THEN  (D  0  With  \mkleeneopen{}t2  k\mkleeneclose{}    THEN  Auto)  THEN  D  0  With  \mkleeneopen{}t3  x  k\mkleeneclose{}    THEN  Auto)

---

Home Index