---

Step * of Lemma constant-partition-sum

∀I:Interval
  (icompact(I) ⇒ (∀p:partition(I). ∀f:I ⟶ℝ. ∀z:ℝ.  ((z ∈ I) ⇒ (S(f;full-partition(I;p)) = ((f z) * |I|)))))
BY
{ (Auto
   THEN RepUR ``partition-sum`` 0
   THEN RWO "rsum_linearity2" 0
   THEN Auto
   THEN BLemma `rmul_functionality`
   THEN Auto
   THEN RWO "rsum-telescopes" 0
   THEN Auto
   THEN RepUR ``full-partition`` 0
   THEN Auto') }

1
1. I : Interval
2. icompact(I)
3. p : partition(I)
4. f : I ⟶ℝ
5. z : ℝ
6. z ∈ I
⊢ ([left-endpoint(I) / (p @ [right-endpoint(I)])][((||p @ [right-endpoint(I)]|| + 1) - 2) + 1] - left-endpoint(I)) = |I|

---

Latex:

---

Latex:
\mforall{}I:Interval
    (icompact(I)
    {}\mRightarrow{}  (\mforall{}p:partition(I).  \mforall{}f:I  {}\mrightarrow{}\mBbbR{}.  \mforall{}z:\mBbbR{}.    ((z  \mmember{}  I)  {}\mRightarrow{}  (S(f;full-partition(I;p))  =  ((f  z)  *  |I|)))))


By

---

Latex:
(Auto
  THEN  RepUR  ``partition-sum``  0
  THEN  RWO  "rsum\_linearity2"  0
  THEN  Auto
  THEN  BLemma  `rmul\_functionality`
  THEN  Auto
  THEN  RWO  "rsum-telescopes"  0
  THEN  Auto
  THEN  RepUR  ``full-partition``  0
  THEN  Auto')

---

Home Index