---

Step * 2 of Lemma m-TB-iff


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)
BY
{ ((Skolemize (-1) `B' THENA Auto)
   THEN (Skolemize (-1) `xs' THENA Auto)
   THEN (Skolemize (-1) `c' THENA Auto)
   THEN UseWitness ⌜<B, xs, λx,y. (c y x)>⌝⋅
   THEN Unfold `m-TB` 0
   THEN MemTypeCD
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  [X]  :  Type
2.  [d]  :  metric(X)
3.  \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)))
\mvdash{}  m-TB(X;d)


By

---

Latex:
((Skolemize  (-1)  `B'  THENA  Auto)
  THEN  (Skolemize  (-1)  `xs'  THENA  Auto)
  THEN  (Skolemize  (-1)  `c'  THENA  Auto)
  THEN  UseWitness  \mkleeneopen{}<B,  xs,  \mlambda{}x,y.  (c  y  x)>\mkleeneclose{}\mcdot{}
  THEN  Unfold  `m-TB`  0
  THEN  MemTypeCD
  THEN  Reduce  0
  THEN  Auto)

---

Home Index