---

Step * 1 1 of Lemma m-TB-product


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)))
BY
{ (MoveToConcl (-1)
   THEN (GenConcl ⌜(m * (k + 1)) = N ∈ ℕ⌝⋅ THENA Auto)
   THEN (D 0 THENA Auto)
   THEN (Skolemize (-1) `B' THENA Auto)) }

1
1. m : ℕ
2. [X] : ℕm ⟶ Type
3. [d] : i:ℕm ⟶ metric(X[i])
4. k : ℕ
5. N : ℕ
6. (m * (k + 1)) = N ∈ ℕ
7. ∀i:ℕm. ∃n:ℕ+. ∃xs:ℕn ⟶ X[i]. ∀x:X[i]. ∃i1:ℕn. (mdist(d[i];x;xs i1) ≤ (r1/r(N + 1)))
8. B : i:ℕm ⟶ ℕ+
9. ∀i:ℕm. ∃xs:ℕB i ⟶ X[i]. ∀x:X[i]. ∃i1:ℕB i. (mdist(d[i];x;xs i1) ≤ (r1/r(N + 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.  k  :  \mBbbN{}
5.  \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)))
\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:
(MoveToConcl  (-1)
  THEN  (GenConcl  \mkleeneopen{}(m  *  (k  +  1))  =  N\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  (Skolemize  (-1)  `B'  THENA  Auto))

---

Home Index