---

Step * 1 of Lemma integral_wf


1. a : ℝ@i
2. b : ℝ@i
3. a ≤ b@i
4. f : [a, b] ⟶ℝ@i
5. mc : f x continuous for x ∈ [a, b]@i
⊢ TERMOF{alt-Riemann-sums-converge-ext:o, 1:l} a b (λx.(f x)) ∈ mc:λx.(f x)[x] continuous for x ∈ [a, b]
  ⟶ Riemann-sum-alt(λx.(f x);a;b;k + 1)↓ as k→∞
BY
{ GenConclAtAddr [2;1] }

1
1. a : ℝ@i
2. b : ℝ@i
3. a ≤ b@i
4. f : [a, b] ⟶ℝ@i
5. mc : f x continuous for x ∈ [a, b]@i
6. v : ∀f:[a, b] ⟶ℝ. ∀mc:f[x] continuous for x ∈ [a, b].  Riemann-sum-alt(f;a;b;k + 1)↓ as k→∞@i
7. (TERMOF{alt-Riemann-sums-converge-ext:o, 1:l} a b)
= v
∈ (∀f:[a, b] ⟶ℝ. ∀mc:f[x] continuous for x ∈ [a, b].  Riemann-sum-alt(f;a;b;k + 1)↓ as k→∞)@i
⊢ v (λx.(f x)) ∈ mc:λx.(f x)[x] continuous for x ∈ [a, b] ⟶ Riemann-sum-alt(λx.(f x);a;b;k + 1)↓ as k→∞

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}@i
2.  b  :  \mBbbR{}@i
3.  a  \mleq{}  b@i
4.  f  :  [a,  b]  {}\mrightarrow{}\mBbbR{}@i
5.  mc  :  f  x  continuous  for  x  \mmember{}  [a,  b]@i
\mvdash{}  TERMOF\{alt-Riemann-sums-converge-ext:o,  1:l\}  a  b  (\mlambda{}x.(f  x))
    \mmember{}  mc:\mlambda{}x.(f  x)[x]  continuous  for  x  \mmember{}  [a,  b]  {}\mrightarrow{}  Riemann-sum-alt(\mlambda{}x.(f  x);a;b;k  +  1)\mdownarrow{}  as  k\mrightarrow{}\minfty{}


By

---

Latex:
GenConclAtAddr  [2;1]

---

Home Index