---

Step * 1 of Lemma dot-product-split-last


1. n : ℕ+
2. x : ℝ^n
3. y : ℝ^n
4. x⋅y = (x⋅y + λi.(x ((n - 1) + i))⋅λi.(y ((n - 1) + i)))
⊢ x⋅y = (x⋅y + ((x (n - 1)) * (y (n - 1))))
BY
{ (RepUR ``dot-product`` -1 THEN (Subst' n - n - 1 - 1 ~ 0 -1 THENA Auto) THEN Fold `dot-product` (-1)) }

1
1. n : ℕ+
2. x : ℝ^n
3. y : ℝ^n
4. x⋅y = (x⋅y + Σ{(x ((n - 1) + i)) * (y ((n - 1) + i)) | 0≤i≤0})
⊢ x⋅y = (x⋅y + ((x (n - 1)) * (y (n - 1))))

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  x  :  \mBbbR{}\^{}n
3.  y  :  \mBbbR{}\^{}n
4.  x\mcdot{}y  =  (x\mcdot{}y  +  \mlambda{}i.(x  ((n  -  1)  +  i))\mcdot{}\mlambda{}i.(y  ((n  -  1)  +  i)))
\mvdash{}  x\mcdot{}y  =  (x\mcdot{}y  +  ((x  (n  -  1))  *  (y  (n  -  1))))


By

---

Latex:
(RepUR  ``dot-product``  -1
  THEN  (Subst'  n  -  n  -  1  -  1  \msim{}  0  -1  THENA  Auto)
  THEN  Fold  `dot-product`  (-1))

---

Home Index