---

Step * 1 of Lemma prod-metric-meq


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))
BY
{ ((InstLemma `rsum-of-nonneg-zero-iff` [⌜0⌝;⌜k - 1⌝]⋅ THENA Auto)
   THEN (Subst' (k - 1) + 1 ~ k -1 THENA Auto)
   THEN (D -1 With ⌜λi.mdist(d i;p i;q i)⌝  THENA Auto)
   THEN RepUR ``so_apply`` -1
   THEN (D -1 THENM Trivial)) }

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

---

Latex:

---

Latex:

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{}  uiff(\mSigma{}\{mdist(d  i;p  i;q  i)  |  0\mleq{}i\mleq{}k  -  1\}  =  r0;\mforall{}i:\mBbbN{}k.  (mdist(d[i];p  i;q  i)  =  r0))


By

---

Latex:
((InstLemma  `rsum-of-nonneg-zero-iff`  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}k  -  1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Subst'  (k  -  1)  +  1  \msim{}  k  -1  THENA  Auto)
  THEN  (D  -1  With  \mkleeneopen{}\mlambda{}i.mdist(d  i;p  i;q  i)\mkleeneclose{}    THENA  Auto)
  THEN  RepUR  ``so\_apply``  -1
  THEN  (D  -1  THENM  Trivial))

---

Home Index