---

Step * 1 1 of Lemma prod-metric-meq

.....antecedent..... 
1. k : ℕ
2. X : ℕk ⟶ Type
3. d : i:ℕk ⟶ metric(X[i])
4. p : i:ℕk ⟶ X[i]
5. q : i:ℕk ⟶ X[i]
⊢ ∀i:ℕk. (r0 ≤ mdist(d i;p i;q i))
BY
{ Auto }

---

Latex:

---

Latex:
.....antecedent..... 
1.  k  :  \mBbbN{}
2.  X  :  \mBbbN{}k  {}\mrightarrow{}  Type
3.  d  :  i:\mBbbN{}k  {}\mrightarrow{}  metric(X[i])
4.  p  :  i:\mBbbN{}k  {}\mrightarrow{}  X[i]
5.  q  :  i:\mBbbN{}k  {}\mrightarrow{}  X[i]
\mvdash{}  \mforall{}i:\mBbbN{}k.  (r0  \mleq{}  mdist(d  i;p  i;q  i))


By

---

Latex:
Auto

---

Home Index