---

Step * 2 1 of Lemma frs-non-dec-sum


1. u : ℝ
2. 1 < 1
3. frs-non-dec([u])
4. ¬1 < 0
⊢ Σ{[u][i + 1] - [u][i] | 0≤i≤-1} = (last([u]) - u)
BY
{ Auto' }

---

Latex:

---

Latex:

1.  u  :  \mBbbR{}
2.  1  <  1
3.  frs-non-dec([u])
4.  \mneg{}1  <  0
\mvdash{}  \mSigma{}\{[u][i  +  1]  -  [u][i]  |  0\mleq{}i\mleq{}-1\}  =  (last([u])  -  u)


By

---

Latex:
Auto'

---

Home Index