---

Step * of Lemma partition-sum-bound

∀I:Interval
  (icompact(I)
  ⇒ (∀f:I ⟶ℝ. ∀mc:f[x] continuous for x ∈ I. ∀p:partition(I). ∀y:partition-choice(full-partition(I;p)).
        (|S(f;full-partition(I;p))| ≤ (||f[x]||_I * |I|))))
BY
{ (SquashExtract THEN Auto THEN Unfold `partition-sum` 0 THEN GenConcl ⌜y = a ∈ (ℕ||p|| + 1 ⟶ {x:ℝ| x ∈ I} )⌝⋅) }

1
.....wf..... 
1. I : Interval
2. icompact(I)
3. f : I ⟶ℝ
4. mc : f[x] continuous for x ∈ I
5. p : partition(I)
6. y : partition-choice(full-partition(I;p))
⊢ y ∈ ℕ||p|| + 1 ⟶ {x:ℝ| x ∈ I} 

2
1. I : Interval
2. icompact(I)
3. f : I ⟶ℝ
4. mc : f[x] continuous for x ∈ I
5. p : partition(I)
6. y : partition-choice(full-partition(I;p))
7. a : ℕ||p|| + 1 ⟶ {x:ℝ| x ∈ I} 
8. y = a ∈ (ℕ||p|| + 1 ⟶ {x:ℝ| x ∈ I} )
⊢ |Σ{(f (a i)) * (full-partition(I;p)[i + 1] - full-partition(I;p)[i]) | 0≤i≤||full-partition(I;p)|| - 2}| ≤ (||f[x]||_I
* |I|)

---

Latex:

---

Latex:
\mforall{}I:Interval
    (icompact(I)
    {}\mRightarrow{}  (\mforall{}f:I  {}\mrightarrow{}\mBbbR{}.  \mforall{}mc:f[x]  continuous  for  x  \mmember{}  I.  \mforall{}p:partition(I).
            \mforall{}y:partition-choice(full-partition(I;p)).
                (|S(f;full-partition(I;p))|  \mleq{}  (||f[x]||\_I  *  |I|))))


By

---

Latex:
(SquashExtract  THEN  Auto  THEN  Unfold  `partition-sum`  0  THEN  GenConcl  \mkleeneopen{}y  =  a\mkleeneclose{}\mcdot{})

---

Home Index