---

Step * 1 of Lemma uniform-partition-point


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index