---

Step * 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)))
⊢ ∃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 ∃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))) BY
         ((Skolemize (-1) `g' THENA Auto)
          THEN (D 0 With ⌜λf,i. (g i (f i))⌝  THEN Auto)
          THEN (Assert ∀i:ℕm. ∃i1:ℕB i. (mdist(d[i];x i;g i i1) ≤ (r1/r(N + 1))) BY
                      (ParallelOp -2 THEN Auto))
          THEN (Skolemize (-1) `f' THENA Auto)
          THEN D 0 With ⌜f⌝ 
          THEN 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)))
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)))
⊢ ∃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.  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)))
\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  \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)))  BY
              ((Skolemize  (-1)  `g'  THENA  Auto)
                THEN  (D  0  With  \mkleeneopen{}\mlambda{}f,i.  (g  i  (f  i))\mkleeneclose{}    THEN  Auto)
                THEN  (Assert  \mforall{}i:\mBbbN{}m.  \mexists{}i1:\mBbbN{}B  i.  (mdist(d[i];x  i;g  i  i1)  \mleq{}  (r1/r(N  +  1)))  BY
                                        (ParallelOp  -2  THEN  Auto))
                THEN  (Skolemize  (-1)  `f'  THENA  Auto)
                THEN  D  0  With  \mkleeneopen{}f\mkleeneclose{} 
                THEN  Auto))

---

Home Index