---

Step * 1 1 1 1 1 of Lemma m-TB-product


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)))
10. ∃xs:(i:ℕm ⟶ ℕB i) ⟶ i:ℕm ⟶ X[i]
     ∀x:i:ℕm ⟶ X[i]. ∃f:i:ℕm ⟶ ℕB i. ∀i:ℕm. (mdist(d[i];x i;xs f i) ≤ (r1/r(N + 1)))
11. i:ℕm ⟶ ℕB[i] ~ ℕΠ(B[i] | i < m)
⊢ ∃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
{ ((D 0 With ⌜Π(B[i] | i < m)⌝  THENA Auto) THEN ExRepD) }

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)))
10. xs : (i:ℕm ⟶ ℕB i) ⟶ i:ℕm ⟶ X[i]
11. ∀x:i:ℕm ⟶ X[i]. ∃f:i:ℕm ⟶ ℕB i. ∀i:ℕm. (mdist(d[i];x i;xs f i) ≤ (r1/r(N + 1)))
12. i:ℕm ⟶ ℕB[i] ~ ℕΠ(B[i] | i < m)
⊢ ∃xs:ℕΠ(B[i] | i < m) ⟶ i:ℕm ⟶ X[i]
   ∀x:i:ℕm ⟶ X[i]. ∃i:ℕΠ(B[i] | i < m). (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.  N  :  \mBbbN{}
6.  (m  *  (k  +  1))  =  N
7.  \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(N  +  1)))
8.  B  :  i:\mBbbN{}m  {}\mrightarrow{}  \mBbbN{}\msupplus{}
9.  \mforall{}i:\mBbbN{}m.  \mexists{}xs:\mBbbN{}B  i  {}\mrightarrow{}  X[i].  \mforall{}x:X[i].  \mexists{}i1:\mBbbN{}B  i.  (mdist(d[i];x;xs  i1)  \mleq{}  (r1/r(N  +  1)))
10.  \mexists{}xs:(i:\mBbbN{}m  {}\mrightarrow{}  \mBbbN{}B  i)  {}\mrightarrow{}  i:\mBbbN{}m  {}\mrightarrow{}  X[i]
          \mforall{}x:i:\mBbbN{}m  {}\mrightarrow{}  X[i].  \mexists{}f:i:\mBbbN{}m  {}\mrightarrow{}  \mBbbN{}B  i.  \mforall{}i:\mBbbN{}m.  (mdist(d[i];x  i;xs  f  i)  \mleq{}  (r1/r(N  +  1)))
11.  i:\mBbbN{}m  {}\mrightarrow{}  \mBbbN{}B[i]  \msim{}  \mBbbN{}\mPi{}(B[i]  |  i  <  m)
\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:
((D  0  With  \mkleeneopen{}\mPi{}(B[i]  |  i  <  m)\mkleeneclose{}    THENA  Auto)  THEN  ExRepD)

---

Home Index