---

Step * 1 of Lemma alt-Riemann-sums-cauchy


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)
BY
{ ((InstLemma `continuous-implies-functional` [⌜[a, b]⌝]⋅ THEN Auto)
   THEN (Unfold `so_apply` -1 THEN BHyp -1 )
   THEN Auto
   THEN Thin (-1)) }

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
⊢ y ∈ {x:ℝ| (a ≤ x) ∧ (x ≤ b)} 

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}@i
2.  b  :  \{b:\mBbbR{}|  a  \mleq{}  b\}  @i
3.  f  :  [a,  b]  {}\mrightarrow{}\mBbbR{}@i
4.  mc  :  f[x]  continuous  for  x  \mmember{}  [a,  b]@i
5.  k@0  :  \mBbbN{}\msupplus{}@i
6.  N  :  \mBbbN{}
7.  k  :  \mBbbN{}@i
8.  m  :  \mBbbN{}@i
9.  N  \mleq{}  k@i
10.  N  \mleq{}  m@i
11.  |Riemann-sum(f;a;b;k  +  1)  -  Riemann-sum(f;a;b;m  +  1)|  \mleq{}  (r1/r(k@0))
12.  x  :  \mBbbR{}@i
13.  y  :  \mBbbR{}@i
14.  x  \mmember{}  [a,  b]@i
15.  x  =  y@i
\mvdash{}  (f  y)  =  (f  x)


By

---

Latex:
((InstLemma  `continuous-implies-functional`  [\mkleeneopen{}[a,  b]\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  (Unfold  `so\_apply`  -1  THEN  BHyp  -1  )
  THEN  Auto
  THEN  Thin  (-1))

---

Home Index