---

Step * of Lemma real-vec-sum-shift

∀[k,n,m:ℤ]. ∀[x:Top].  (Σ{x[i] | n≤i≤m} ~ Σ{x[i + k] | n - k≤i≤m - k})
BY
{ ((UnivCD THENA Auto) THEN Unfold `real-vec-sum` 0 THEN EqCD THEN BLemma `rsum-shift` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[k,n,m:\mBbbZ{}].  \mforall{}[x:Top].    (\mSigma{}\{x[i]  |  n\mleq{}i\mleq{}m\}  \msim{}  \mSigma{}\{x[i  +  k]  |  n  -  k\mleq{}i\mleq{}m  -  k\})


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `real-vec-sum`  0  THEN  EqCD  THEN  BLemma  `rsum-shift`  THEN  Auto)

---

Home Index