---

Step * of Lemma m-TB-iff

∀[X:Type]. ∀[d:metric(X)].  (m-TB(X;d) ⇐⇒ ∀k:ℕ. ∃n:ℕ+. ∃xs:ℕn ⟶ X. ∀x:X. ∃i:ℕn. (mdist(d;x;xs i) ≤ (r1/r(k + 1))))
BY
{ Auto }

1
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)))

2
1. [X] : Type
2. [d] : metric(X)
3. ∀k:ℕ. ∃n:ℕ+. ∃xs:ℕn ⟶ X. ∀x:X. ∃i:ℕn. (mdist(d;x;xs i) ≤ (r1/r(k + 1)))
⊢ m-TB(X;d)

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[d:metric(X)].
    (m-TB(X;d)  \mLeftarrow{}{}\mRightarrow{}  \mforall{}k:\mBbbN{}.  \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:
Auto

---

Home Index