---

Step * 2 1 1 of Lemma uniform-partition-point


1. I : Interval
2. icompact(I)
3. k : ℕ+
4. i : ℕk + 1
5. ¬(i = 0 ∈ ℤ)
6. r(k) ≠ r0
7. i = k ∈ ℤ
⊢ ([right-endpoint(I)][k - 1 - k - 1] * r(k)) = (((r(k) - r(k)) * left-endpoint(I)) + (r(k) * right-endpoint(I)))
BY
{ RepeatFor 2 ((RW IntNormC 0 THEN Auto THEN Reduce 0 THEN nRNorm 0 THEN Auto)⋅) }

---

Latex:

---

Latex:

1.  I  :  Interval
2.  icompact(I)
3.  k  :  \mBbbN{}\msupplus{}
4.  i  :  \mBbbN{}k  +  1
5.  \mneg{}(i  =  0)
6.  r(k)  \mneq{}  r0
7.  i  =  k
\mvdash{}  ([right-endpoint(I)][k  -  1  -  k  -  1]  *  r(k))
=  (((r(k)  -  r(k))  *  left-endpoint(I))  +  (r(k)  *  right-endpoint(I)))


By

---

Latex:
RepeatFor  2  ((RW  IntNormC  0  THEN  Auto  THEN  Reduce  0  THEN  nRNorm  0  THEN  Auto)\mcdot{})

---

Home Index