---

Step * 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)))
⊢ ∃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
{ (InstLemma `equipollent-product` [⌜m⌝;⌜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)))
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)))

---

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)))
\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:
(InstLemma  `equipollent-product`  [\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index