---

Step * 1 of Lemma m-TB-product


1. m : ℕ
2. [X] : ℕm ⟶ Type
3. [d] : i:ℕm ⟶ metric(X[i])
4. ∀i:ℕm. ∀k:ℕ.  ∃n:ℕ+. ∃xs:ℕn ⟶ X[i]. ∀x:X[i]. ∃i1:ℕn. (mdist(d[i];x;xs i1) ≤ (r1/r(k + 1)))
5. k : ℕ
⊢ ∃n:ℕ+. ∃xs:ℕn ⟶ i:ℕm ⟶ X[i]. ∀x:i:ℕm ⟶ X[i]. ∃i:ℕn. (mdist(prod-metric(m;d);x;xs i) ≤ (r1/r(k + 1)))
BY
{ ((Assert ∀i:ℕm. ∃n:ℕ+. ∃xs:ℕn ⟶ X[i]. ∀x:X[i]. ∃i1:ℕn. (mdist(d[i];x;xs i1) ≤ (r1/r((m * (k + 1)) + 1))) BY
          (ParallelOp -2 THEN Auto))
   THEN Thin (-3)
   ) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
((Assert  \mforall{}i:\mBbbN{}m
                      \mexists{}n:\mBbbN{}\msupplus{}
                        \mexists{}xs:\mBbbN{}n  {}\mrightarrow{}  X[i].  \mforall{}x:X[i].  \mexists{}i1:\mBbbN{}n.  (mdist(d[i];x;xs  i1)  \mleq{}  (r1/r((m  *  (k  +  1))  +  1)))  BY
                (ParallelOp  -2  THEN  Auto))
  THEN  Thin  (-3)
  )

---

Home Index