---

Step * of Lemma alt-Riemann-sums-cauchy

∀a:ℝ. ∀b:{b:ℝ| a ≤ b} . ∀f:[a, b] ⟶ℝ. ∀mc:f[x] continuous for x ∈ [a, b].  cauchy(k.Riemann-sum-alt(f;a;b;k + 1))
BY
{ (InstLemma `Riemann-sums-cauchy` []
   THEN RepeatFor 10 (ParallelLast')
   THEN Auto
   THEN RWO "Riemann-sum-alt-req" 0
   THEN Auto) }

1
1. a : ℝ@i
2. b : {b:ℝ| a ≤ b} @i
3. f : [a, b] ⟶ℝ@i
4. mc : f[x] continuous for x ∈ [a, b]@i
5. k@0 : ℕ+@i
6. N : ℕ
7. k : ℕ@i
8. m : ℕ@i
9. N ≤ k@i
10. N ≤ m@i
11. |Riemann-sum(f;a;b;k + 1) - Riemann-sum(f;a;b;m + 1)| ≤ (r1/r(k@0))
12. x : ℝ@i
13. y : ℝ@i
14. x ∈ [a, b]@i
15. x = y@i
⊢ (f y) = (f x)

---

Latex:

---

Latex:
\mforall{}a:\mBbbR{}.  \mforall{}b:\{b:\mBbbR{}|  a  \mleq{}  b\}  .  \mforall{}f:[a,  b]  {}\mrightarrow{}\mBbbR{}.  \mforall{}mc:f[x]  continuous  for  x  \mmember{}  [a,  b].
    cauchy(k.Riemann-sum-alt(f;a;b;k  +  1))


By

---

Latex:
(InstLemma  `Riemann-sums-cauchy`  []
  THEN  RepeatFor  10  (ParallelLast')
  THEN  Auto
  THEN  RWO  "Riemann-sum-alt-req"  0
  THEN  Auto)

---

Home Index