---

Step * of Lemma Riemann-sum-alt-req

∀[a:ℝ]. ∀[b:{b:ℝ| a ≤ b} ]. ∀[f:[a, b] ⟶ℝ].
  ((∀x,y:ℝ.  ((x ∈ [a, b]) ⇒ (x = y) ⇒ ((f y) = (f x))))
  ⇒ (∀[k:ℕ+]. (Riemann-sum-alt(f;a;b;k) = Riemann-sum(f;a;b;k))))
BY
{ (Auto
   THEN Try (Complete ((RepUR ``i-member`` -2 THEN MemTypeCD THEN Auto)))
   THEN (DVar `b'⋅ THEN (Unhide THENA Auto))
   THEN (Assert icompact([a, b]) BY
               EAuto 1)
   THEN Unfolds ``Riemann-sum-alt`` 0
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))) }

1
1. a : ℝ
2. b : ℝ
3. a ≤ b
4. f : [a, b] ⟶ℝ
5. ∀x,y:ℝ.  ((x ∈ [a, b]) ⇒ (x = y) ⇒ ((f y) = (f x)))@i
6. k : ℕ+
7. icompact([a, b])
⊢ (rsum'(0;k - 1;i.f ((r(k - i) * a) + (r(i) * b)/r(k))) * (b - a/r(k))) = Riemann-sum(f;a;b;k)

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  Try  (Complete  ((RepUR  ``i-member``  -2  THEN  MemTypeCD  THEN  Auto)))
  THEN  (DVar  `b'\mcdot{}  THEN  (Unhide  THENA  Auto))
  THEN  (Assert  icompact([a,  b])  BY
                          EAuto  1)
  THEN  Unfolds  ``Riemann-sum-alt``  0
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto)))

---

Home Index