---

Step * of Lemma Riemann-sum-rsub

∀[a:ℝ]. ∀[b:{b:ℝ| a ≤ b} ]. ∀[f,g:[a, b] ⟶ℝ]. ∀[k:ℕ+].
  ((Riemann-sum(f;a;b;k) - Riemann-sum(g;a;b;k)) = Riemann-sum(λx.((f x) - g x);a;b;k))
BY
{ (Auto
   THEN DVar `b'⋅
   THEN (Unhide THENA Auto)
   THEN (Assert icompact([a, b]) BY
               EAuto 1)
   THEN (Unfold `Riemann-sum` 0 THEN (CallByValueReduce 0 THENA Auto))
   THEN (Assert ⌜full-partition([a, b];uniform-partition([a, b];k)) ∈ {x:ℝ| (a ≤ x) ∧ (x ≤ b)}  List⌝⋅
   THENM ((GenConclAtAddr [2;1] THENA Auto)
          THEN (CallByValueReduce 0 THENA Auto)
          THEN RepUR ``partition-sum default-partition-choice`` 0)
   )) }

1
.....assertion..... 
1. a : ℝ
2. b : ℝ
3. a ≤ b
4. f : [a, b] ⟶ℝ
5. g : [a, b] ⟶ℝ
6. k : ℕ+
7. icompact([a, b])
⊢ full-partition([a, b];uniform-partition([a, b];k)) ∈ {x:ℝ| (a ≤ x) ∧ (x ≤ b)}  List

2
1. a : ℝ
2. b : ℝ
3. a ≤ b
4. f : [a, b] ⟶ℝ
5. g : [a, b] ⟶ℝ
6. k : ℕ+
7. icompact([a, b])
8. full-partition([a, b];uniform-partition([a, b];k)) ∈ {x:ℝ| (a ≤ x) ∧ (x ≤ b)}  List
9. v : {x:ℝ| (a ≤ x) ∧ (x ≤ b)}  List@i
10. full-partition([a, b];uniform-partition([a, b];k)) = v ∈ ({x:ℝ| (a ≤ x) ∧ (x ≤ b)}  List)@i
⊢ (Σ{(f v[i]) * (v[i + 1] - v[i]) | 0≤i≤||v|| - 2} - Σ{(g v[i]) * (v[i + 1] - v[i]) | 0≤i≤||v|| - 2})
= Σ{((f v[i]) - g v[i]) * (v[i + 1] - v[i]) | 0≤i≤||v|| - 2}

---

Latex:

---

Latex:
\mforall{}[a:\mBbbR{}].  \mforall{}[b:\{b:\mBbbR{}|  a  \mleq{}  b\}  ].  \mforall{}[f,g:[a,  b]  {}\mrightarrow{}\mBbbR{}].  \mforall{}[k:\mBbbN{}\msupplus{}].
    ((Riemann-sum(f;a;b;k)  -  Riemann-sum(g;a;b;k))  =  Riemann-sum(\mlambda{}x.((f  x)  -  g  x);a;b;k))


By

---

Latex:
(Auto
  THEN  DVar  `b'\mcdot{}
  THEN  (Unhide  THENA  Auto)
  THEN  (Assert  icompact([a,  b])  BY
                          EAuto  1)
  THEN  (Unfold  `Riemann-sum`  0  THEN  (CallByValueReduce  0  THENA  Auto))
  THEN  (Assert  \mkleeneopen{}full-partition([a,  b];uniform-partition([a,  b];k))  \mmember{}  \{x:\mBbbR{}|  (a  \mleq{}  x)  \mwedge{}  (x  \mleq{}  b)\}    List\mkleeneclose{}\mcdot{}
  THENM  ((GenConclAtAddr  [2;1]  THENA  Auto)
                THEN  (CallByValueReduce  0  THENA  Auto)
                THEN  RepUR  ``partition-sum  default-partition-choice``  0)
  ))

---

Home Index