---

Step * of Lemma prod-metric-meq

∀[k:ℕ]. ∀[X:ℕk ⟶ Type]. ∀[d:i:ℕk ⟶ metric(X[i])]. ∀[p,q:i:ℕk ⟶ X[i]].  uiff(p ≡ q;∀i:ℕk. p i ≡ q i)
BY
{ (Intros THEN (Unhide THENA Auto) THEN RepUR ``meq prod-metric`` 0 THEN Fold `mdist` 0) }

1
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]
⊢ uiff(Σ{mdist(d i;p i;q i) | 0≤i≤k - 1} = r0;∀i:ℕk. (mdist(d[i];p i;q i) = r0))

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[X:\mBbbN{}k  {}\mrightarrow{}  Type].  \mforall{}[d:i:\mBbbN{}k  {}\mrightarrow{}  metric(X[i])].  \mforall{}[p,q:i:\mBbbN{}k  {}\mrightarrow{}  X[i]].
    uiff(p  \mequiv{}  q;\mforall{}i:\mBbbN{}k.  p  i  \mequiv{}  q  i)


By

---

Latex:
(Intros  THEN  (Unhide  THENA  Auto)  THEN  RepUR  ``meq  prod-metric``  0  THEN  Fold  `mdist`  0)

---

Home Index