---

Step * of Lemma Riemann-sum-rleq

∀[a:ℝ]. ∀[b:{b:ℝ| a ≤ b} ]. ∀[f,g:[a, b] ⟶ℝ]. ∀[k:ℕ+].
  Riemann-sum(f;a;b;k) ≤ Riemann-sum(g;a;b;k) supposing ∀x:ℝ. ((x ∈ [a, b]) ⇒ ((f x) ≤ (g x)))
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. ∀x:ℝ. ((x ∈ [a, b]) ⇒ ((f x) ≤ (g x)))
8. 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. ∀x:ℝ. ((x ∈ [a, b]) ⇒ ((f x) ≤ (g x)))
8. icompact([a, b])
9. full-partition([a, b];uniform-partition([a, b];k)) ∈ {x:ℝ| (a ≤ x) ∧ (x ≤ b)}  List
10. v : {x:ℝ| (a ≤ x) ∧ (x ≤ b)}  List@i
11. 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}

---

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)  \mleq{}  Riemann-sum(g;a;b;k)  supposing  \mforall{}x:\mBbbR{}.  ((x  \mmember{}  [a,  b])  {}\mRightarrow{}  ((f  x)  \mleq{}  (g  x)))


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