---

Step * of Lemma m-TB-product

∀m:ℕ. ∀[X:ℕm ⟶ Type]. ∀[d:i:ℕm ⟶ metric(X[i])].  ((∀i:ℕm. m-TB(X[i];d[i])) ⇒ m-TB(i:ℕm ⟶ X[i];prod-metric(m;d)))
BY
{ (Auto THEN (RWO "m-TB-iff" (-1) THENA Auto) THEN (RWO "m-TB-iff" 0 THENA Auto) THEN (D 0 THENA Auto)) }

1
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)))

---

Latex:

---

Latex:
\mforall{}m:\mBbbN{}
    \mforall{}[X:\mBbbN{}m  {}\mrightarrow{}  Type].  \mforall{}[d:i:\mBbbN{}m  {}\mrightarrow{}  metric(X[i])].
        ((\mforall{}i:\mBbbN{}m.  m-TB(X[i];d[i]))  {}\mRightarrow{}  m-TB(i:\mBbbN{}m  {}\mrightarrow{}  X[i];prod-metric(m;d)))


By

---

Latex:
(Auto
  THEN  (RWO  "m-TB-iff"  (-1)  THENA  Auto)
  THEN  (RWO  "m-TB-iff"  0  THENA  Auto)
  THEN  (D  0  THENA  Auto))

---

Home Index