---

Step * of Lemma rsum-single

∀[n:ℤ]. ∀[x:{i:ℤ| i = n ∈ ℤ}  ⟶ ℝ].  (Σ{x[i] | n≤i≤n} = x[n])
BY
{ ((UnivCD THENA Auto) THEN Unfold `rsum` 0 THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))) }

1
1. n : ℤ
2. x : {i:ℤ| i = n ∈ ℤ}  ⟶ ℝ
⊢ let xs ⟵ map(λi.x[i];[n, n + 1)) in radd-list(xs) = x[n]

---

Latex:

---

Latex:
\mforall{}[n:\mBbbZ{}].  \mforall{}[x:\{i:\mBbbZ{}|  i  =  n\}    {}\mrightarrow{}  \mBbbR{}].    (\mSigma{}\{x[i]  |  n\mleq{}i\mleq{}n\}  =  x[n])


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `rsum`  0  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto)))

---

Home Index