---

Step * of Lemma partition-sum-constant

∀I:Interval
  (icompact(I)
  ⇒ (∀c:ℝ. ∀p:partition(I). ∀y:partition-choice(full-partition(I;p)).  (S(λx.c;full-partition(I;p)) = (c * |I|))))
BY
{ (Auto THEN (GenConcl ⌜full-partition(I;p) = v ∈ (ℝ List)⌝⋅ THENA Auto) THEN Unfold `partition-sum` 0 THEN Reduce 0) }

1
1. I : Interval
2. icompact(I)
3. c : ℝ
4. p : partition(I)
5. y : partition-choice(full-partition(I;p))
6. v : ℝ List
7. full-partition(I;p) = v ∈ (ℝ List)
⊢ Σ{c * (v[i + 1] - v[i]) | 0≤i≤||v|| - 2} = (c * |I|)

---

Latex:

---

Latex:
\mforall{}I:Interval
    (icompact(I)
    {}\mRightarrow{}  (\mforall{}c:\mBbbR{}.  \mforall{}p:partition(I).  \mforall{}y:partition-choice(full-partition(I;p)).
                (S(\mlambda{}x.c;full-partition(I;p))  =  (c  *  |I|))))


By

---

Latex:
(Auto
  THEN  (GenConcl  \mkleeneopen{}full-partition(I;p)  =  v\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Unfold  `partition-sum`  0
  THEN  Reduce  0)

---

Home Index